Select Git revision
Fabian Vu authored and
GitHub
committed
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
README.md 11.02 KiB
Benchmarks
Execution
Executing benchmarks is done by executing make in each of the directories.
Technical Data
- 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
Results
Single-threaded
| 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 | - / - | - / - | - / - |
Multi-threaded (6 Threads)
| 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 | - / - | - / - | - / - |
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
Entries as v1/v2 for -O1/-O2