Skip to content
Snippets Groups Projects
Select Git revision
  • 5db2a2e554aff67e2f08c36741637c1eff445fd5
  • master default protected
  • btypes-fixes
  • freetypes
  • embedded-codegen
  • rust-support
  • z3solver
7 results

README.md

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.

    Benchmarks

    Execution

    Executing benchmarks is done by executing make in each of the directories.

    Technical Data

    System A

    • Java: Java HotSpot(TM) 64-Bit Server VM (build 15+36-1562, mixed mode, sharing)
    • C++ Compiler: Apple clang version 13.0.0 (clang-1300.0.29.30) with -O1 and -O2
    • ProB: 1.9.0-nightly (b6d1b600dbf06b7984dd2a1dd7403206cfd9d394)
    • B2Program Commit: 4ba7747d
    • Device: MacBook Air with 8 GB of RAM and a 1.6 GHz Intel i5 processor with two cores

    System B

    • Java: OpenJDK 64-Bit Server VM AdoptOpenJDK (build 15.0.2+7, mixed mode, sharing)
    • C++ Compiler: clang version 7.0.1-8+deb10u2 (tags/RELEASE_701/final) with -O1 and -O2
    • Rust: rustc 1.58.1 (db9d1b20b 2022-01-20), cargo 1.58.0 (f01b232bc 2022-01-19)
    • ProB: 1.12.0-nightly (693d2769ec052b92f3b9f3cfc8e50b53bd41a0a7)
    • B2Programm Commit: 7e0bb37cf1b556bd7f7e8f8a1d63a26ebe16ad18 (branch: rust-support, will probably change on rebase)
    • Device: Debian 10 (buster) under wsl 2 (Windows 10), with Ryzen 7 1700 (8C/16T) and 32GB RAM

    Results

    Single-threaded

    System A

    Machines ProB OP ProB ST TLC Java C++ -O1 C++ -O2
    Counter Runtime 90.06 87.98 8.52 3.24 / 5.16 1.29 / 5.88 1.28 / 5.84
    Speed-up 1 1.02 10.67 27.84 / 17.47 70.08 / 15.33 70.63 / 15.42
    Memory 1151604 1151556 335420 421034 / 654880 217920 / 878754 217940 / 878780
    Cruise Controller Runtime 0.75 1.74 6.89 1.6 / 1.53 0.06 / 0.16 0.06 / 0.15
    Speed-up 1 0.11 0.15 0.47 / 0.49 12.5 / 4.69 12.5 / 5
    Memory 174954 174247 172016 121832 / 113110 2722 / 10912 2788 / 11040
    Landing Gear Runtime 36.85 188.87 25.68 18.23 / 17.22 15.1 / 34.38 14.98 / 33.36
    Speed-up 1 0.2 1.51 2.12 / 2.44 2.56 / 1.12 2.58 / 1.16
    Memory 476783 469995 681308 751508 / 985684 186736 / 1053604 186726 / 1053642
    CAN BUS Runtime 23.13 52.11 11.42 6.23 / 7.21 3.77 / 10.29 3.7 / 9.85
    Speed-up 1 0.44 2.03 3.71 / 3.2 6.14 / 2.25 6.26 / 2.35
    Memory 353338 352125 461096 450596 / 562440 196762 / 677544 196708 / 677734
    Train_6 Runtime 21.92 55.09 19.02 18.96 / 17.13 13.77 / 8.56 13.71 / 8.29
    Speed-up 1 0.4 1.15 1.16 / 1.28 1.59 / 2.56 1.6 / 2.64
    Memory 278126 204090 348272 479204 / 854666 43414 / 108370 43418 / 108410
    Train_10 Runtime 776.81 2564.03 2373.16 1004.45 / 799.37 940.32 / 533.78 924.577 / 520.63
    Speed-up 1 0.3 0.33 0.77 / 0.97 0.83 / 1.46 0.84 / 1.49
    Memory 2995244 1278929 896422 1267960 / 2317640 1228082 / 2995064 1228102 / 2995000
    nota Runtime 29.89 178.82 18.78 21.89 / 20.9 88.51 / 157.8 89.48 / 157.9
    Speed-up 1 0.17 1.59 1.37 / 1.43 0.34 / 0.19 0.33 / 0.19
    Memory 947413 946857 883470 974294 / 1063392 189306 / 993818 189344 / 993864
    sort_1000 Runtime 234.97 359.23 505.1 1365.79 / 146.72 3288.73 / 3468.77 3244.62 / 3473.78
    Speed-up 1 0.65 0.47 0.15 / 1.6 0.07 / 0.07 0.07 / 0.06
    Memory 833697 602163 374906 521224 / 1314720 303293 / 947840 303300 / 947864
    N Queens (N=4) Runtime 0.15 0.19 6.46 61.97 / 61.19 57.05 / 57.02 56.43 / 55.73
    Speed-up 1 0.79 0.02 0.002 / 0.002 0.003 / 0.003 0.003 / 0.003
    Memory 166608 166574 170972 351168 / 349608 48892 / 48886 48998 / 48996
    N Queens (N=8) Runtime 0.46 0.56 278 > 3600 / > 3600 > 3600 / > 3600 > 3600 / > 3600
    Speed-up 1 0.83 0.002 < 0.001 / < 0.001 < 0.001 / < 0.001 < 0.001 / < 0.001
    Memory 166907 166872 255230 - / - - / - - / -

    System B

    Machines ProB OP ProB ST Java C++ -O1 C++ -O2 Rust
    Lift_MC_Large Runtime 89.59 84.3 2.23 / 2.7 0.80 / 0.97 0.74 / 00.96 00.42 / 00.50
    Speed-up 1 1.06 40.17 / 33.18 111.99 / 92.36 121.07 / 93.32 213.31 / 179.18
    Memory 1.139.020 1.139.546 700.824 / 721.548 250.488 / 250.524 250.388 / 250.405 54.734 / 54.742
    Cruise Controller Runtime 2.7 3.56 1.73 / 2.28 0.14 / 0.14 0.11 / 00.12 00.07 / 00.18
    Speed-up 1 0.76 1.56 / 1.18 19.29 / 19.29 24.55 / 22.5 38.57 / 15
    Memory 186.172 186.408 159.292 / 161.860 6.296 / 6.580 6.310 / 6.489 5011 / 5226
    Landing Gear Runtime 45.35 185.56 11.16 / 13.52 10.95 / 10.58 8.79 / 9.59 09.84 / 19.23
    Speed-up 1 0.24 4.06 / 3.35 4.14 / 4.29 5.16 / 4.73 4.61 / 2.36
    Memory 487.388 481.932 1.063.784 / 1.352.408 329.680 / 333.076 329.672 / 332.976 734.749 / 854.914
    CAN BUS Runtime 27.78 52.99 3.79 / 4.47 1.99 / 2.1 1.71 / 2.02 02.3 / 02.45
    Speed-up 1 0.52 7.33 / 6.21 13.96 / 13.23 16.25 / 13.75 12.08 / 11.34
    Memory 366.300 365.156 542.680 / 1.080.708 316.888 / 326.688 316.873 / 326.791 1.012.179 / 1.049.515
    Train1_Lukas Runtime 21.59 54.19 13.0 / 12.25 5.29 / 2.39 4.93 / 2.31 07.08 / 07.14
    Speed-up 1 0.4 1.66 / 1.76 4.08 / 9.03 4.38 / 9.35 3.05 / 3.02
    Memory 289.692 217.156 701.600 / 1.044.600 59.408 / 62.912 59.299 / 62.798 187.201 / 255.626
    Train_1_beebook_v2 Runtime 570.51 1642.6 626.39 / 545.66 338.03 / 140.84 311.83 / 135.69 445.79 / 416.89
    Speed-up 1 0.35 0.91 / 1.05 1.69 / 4.05 1.83 / 4.2 1.28 / 1.37
    Memory 2.998.192 1.310.184 1.451.340 / 3.110.416 1.559.736 / 1.667.508 1.559.626 / 1.667.335 4.735.570 / 6.047.158
    nota Runtime 33.08 166.53 10.75 / 9.58 26.55 / 23.1 22.43 / 21.4 20.12 / 20.77
    Speed-up 1 0.2 3.08 / 3.45 1.25 / 1.43 1.47 / 1.55 1.64 / 1.59
    Memory 950.228 948.460 1.201.656 / 1.512.316 280.532 / 413.696 280.518 / 413.597 1.321.891 / 1.269.008
    sort_1000 Runtime 242.17 301.23 988.25 / 85.87 1650.41 / 1317.36 1424.95 / 1251.89 516 / 95.12
    Speed-up 1 0.8 0.25 / 2.82 0.15 / 0.18 0.17 / 0.19 0.47 / 2.55
    Memory 828.468 602.360 1.202.264 / 1.361.680 338.680 / 342.100 338.626 / 342.083 269.996 / 269.939
    N Queens (N=4) Runtime 2.15 2.18 34.41 / 35.73 28.81 / 32.6 27.79 / 27.16 22.34 / 22.74
    Speed-up 1 0.99 0.06 / 0.06 0.07 / 0.07 0.08 / 0.08 0.1 / 0.09
    Memory 178.152 177.208 511.568 / 503.032 61.684 / 61.980 61.762 / 61.814 345.376 / 345.386

    Multi-threaded (6 Threads)

    Note: Threadcount only includes worker threads (the ones that actually do the model-checking). Current implementation requires an additional coordinator thread.

    System A

    Machines TLC Java C++ -O1 C++ -O2
    Counter Runtime 11.79 22.98 / 26.34 17.55 / 24.47 17.62 / 24.47
    Speed-up to TLC 1 0.51 / 0.45 0.67 / 0.48 0.67 / 0.48
    Speed-up to 1 TH 0.73 0.15 / 0.2 0.07 / 0.24 0.07 / 0.24
    Memory 294664 398248 / 728514 218086 / 878910 218078 / 878928
    Cruise Controller Runtime 6.86 1.68 / 1.6 0.06 / 0.15 0.05 / 0.15
    Speed-up to TLC 1 4.1 / 4.3 114.33 / 45.73 137.2 / 45.73
    Speed-up to 1 TH 1 0.96 / 0.96 1 / 1.07 1.2 / 1
    Memory 172032 147498 / 142246 3048 / 10994 3086 / 11150
    Landing Gear Runtime 19.76 14.49 / 14.56 11.54 / 27.29 11.3 / 27.35
    Speed-up to TLC 1 1.36 / 1.36 1.71 / 0.72 1.75 / 0.72
    Speed-up to 1 TH 1.3 1.26 / 1.18 1.31 / 1.26 1.33 / 1.22
    Memory 808976 954956 / 1179980 195566 / 1056952 195590 / 1057498
    CAN BUS Runtime 13.4 6.78 / 7.53 3.61 / 11.03 3.53 / 10.89
    Speed-up to TLC 1 1.98 / 1.78 3.72 / 1.21 3.8 / 1.23
    Speed-up to 1 TH 0.85 0.92 / 0.96 1.04 / 0.93 1.05 / 0.9
    Memory 468646 498644 / 574292 204528 / 687058 204572 / 687424
    Train_6 Runtime 15.33 12.54 / 11.97 8.56 / 5.44 8.42 / 5.4
    Speed-up to TLC 1 1.22 / 1.28 1.79 / 2.82 1.82 / 2.84
    Speed-up to 1 TH 1.24 1.51 / 1.43 1.61 / 1.57 1.63 / 1.54
    Memory 468646 725776 / 1077684 204528 / 687058 204572 / 687424
    Train_10 Runtime 1482.03 459.81 / 421.8 536.21 / 318.4 532.94 / 316.53
    Speed-up to TLC 1 3.22 / 3.51 2.76 / 4.65 2.78 / 4.68
    Speed-up to 1 TH 1.6 2.18 / 1.9 1.75 / 1.68 1.73 / 1.64
    Memory 1077022 1456166 / 2340918 1261254 / 3164336 1261022 / 3164792
    nota Runtime 16.1 16.87 / 19.56 97.37 / 181.08 97 / 179.75
    Speed-up to TLC 1 0.95 / 0.82 0.17 / 0.09 0.17 / 0.09
    Speed-up to 1 TH 1.17 1.3 / 1.07 0.91 / 0.87 0.92 / 0.88
    Memory 898580 1100700 / 1138802 220748 / 1035806 218750 / 1035398
    sort_1000 Runtime 306.13 663.23 / 79.55 1504 / 1613.77 1496.86 / 1580.33
    Speed-up to TLC 1 0.46 / 3.84 0.2 / 0.19 0.2 / 0.19
    Speed-up to 1 TH 1.65 2.06 / 1.85 2.19 / 2.15 2.17 / 2.2
    Memory 503360 520850 / 1894494 304048 / 948392 304058 / 948402
    N Queens (N=4) Runtime 6.44 58.68 / 60.18 56.5 / 56.13 54.99 / 55.14
    Speed-up to TLC 1 0.11 / 0.11 0.11 / 0.11 0.12 / 0.12
    Speed-up to 1 TH 1.0 1.06 / 1.02 1.01 / 1.02 1.03 / 1.01
    Memory 170934 360534 / 350706 49026 / 48920 49012 / 49018
    N Queens (N=8) Runtime 190.72 > 3600 / > 3600 > 3600 / > 3600 > 3600 / > 3600
    Speed-up to TLC 1 < 0.01 / < 0.01 < 0.01 / < 0.01 < 0.01 / < 0.01
    Speed-up to 1 TH 1.46 - / - - / - - / -
    Memory 260730 - / - - / - - / -

    System B

    Machines Java C++ -O1 C++ -O2 Rust
    Lift_MC_Large Runtime 67.14 / 67.37 63.33 / 64.33 64.37 / 61.59 09.82 / 09.96
    Speed-up
    Memory 548.128 / 522.388 250.840 / 250.926 250.822 / 250.832 38.637 / 38.590
    Cruise Controller Runtime 1.76 / 1.78 0.06 / 0.06 0.05 / 00.06 00.04 / 00.06
    Speed-up
    Memory 171.916 / 180.132 6.544 / 7.112 6.697 / 7.018 6.978 / 6.959
    Landing Gear Runtime 6.42 / 6.69 7.28 / 7.59 7.03 / 6.76 03.41 / 04.56
    Speed-up
    Memory 1.405.280 / 2.043.336 340.408 / 345.720 341.353 / 345.930 727.461 / 847.765
    CAN BUS Runtime 3.52 / 4.29 3.92 / 4.51 4.12 / 4.35 01.64 / 01.64
    Speed-up
    Memory 550.004 / 1.159.472 317.140 / 326.652 317.437 / 326.536 1.047.918 / 1.050.520
    Train1_Lukas Runtime 5.96 / 5.44 4.46 / 2.02 4.36 / 1.91 01.61 / 01.46
    Speed-up
    Memory 1.468.360 / 1.772.524 60.412 / 65.012 60.320 / 64.956 189.500 / 250.548
    Train_1_beebook Runtime 174.56 / 147.29 257.59 / 115.41 250.92 / 111.71 89.65 / 76.61
    Speed-up
    Memory 2.555.344 / 3.094.376 1.573.868 / 1.812.972 1.572.735 / 1.814.287 4.998.943 / 5.484.696
    nota Runtime 5.12 / 4.74 25.91 / 25.63 26.12 / 21.58 05.02 / 05.24
    Speed-up
    Memory 2.185.468 / 2.464.928 300.208 / 438.692 299.167 / 433.206 1.390.200 / 1.369.317
    sort_1000 Runtime 208.82 / 37.32 327.81 / 279.46 336.3 / 273.14 110.91 / 27.47
    Speed-up
    Memory 2.359.820 / 2.420.428 323.472 / 341.740 323.596 / 341.784 243.784 / 243.330
    N Queens (N=4) Runtime 32.87 / 32.2 30.02 / 28.66 30.88 / 25.98 21.34 / 22.46
    Speed-up
    Memory 508.736 / 499.924 62696 / 62.832 62.630 / 62.742 345.888 / 345.855

    Runtime in Seconds

    Memory Usage in KB

    OP = Operation Reuse

    ST = Standard

    TH = Thread

    Entries as v1/v2 for without/with caching

    Overhead

    Machines ProB TLC Java C++
    Counter Parsing/Translation 2.52 2.95 1.32 1.35
    Compiling - - 2.15 6.22 / 7.31
    Cruise Controller Parsing/Translation 3.05 3.97 2.34 2.52
    Compiling - - 3.33 20.84 / 37.48
    Landing Gear Parsing/Translation 3.04 3.91 2.53 2.74
    Compiling - - 3.61 16.17 / 23.45
    CAN BUS Parsing/Translation 2.85 3.45 1.87 2.05
    Compiling - - 3.05 16.4 / 20.64
    Train_6 Parsing/Translation 2.83 3.5 2.1 2.19
    Compiling - - 2.8 15.52 / 20.05
    Train_10 Parsing/Translation 2.9 3.59 2.07 2.21
    Compiling - - 2.84 15.52 / 20.05
    nota Parsing/Translation 2.94 3.65 2.14 2.32
    Compiling - - 3.03 29.23 / 39.76
    sort_1000 Parsing/Translation 2.61 3.1 1.53 1.58
    Compiling - - 2.26 8.51 / 10.37
    N Queens (N=4) Parsing/Translation 2.61 3.07 1.45 1.5
    Compiling - - 2.2 9.11 / 11.33
    N Queens (N=8) Parsing/Translation 2.59 3.08 1.46 1.53
    Compiling - - 2.1 9.14 / 11.35

    Time in Seconds