Select Git revision
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
README.md 7.57 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 12.0.1+12,mixed mode, sharing)
- C++ Compiler: Apple LLVM version 10.0.1 (clang-1001.0.46.4) with -O1 and -O2
- ProB: 1.9.0-nightly (c5a6e9d31022d0bfe40cbcdf68e910041665ec41)
- B2Program Commit: edce3cc7
- Device: MacBook Air with 8 GBof RAM and a 1.6 GHz Intel i5 processor with two cores
Results
| Machines | ProB | Java BI | Java PI | C++ PI -O1 | C++ PI -O2 | |
|---|---|---|---|---|---|---|
| Lift | Runtime | > 1800 | 156.63 | 27.43 | 78.42 | 0.00 |
| Speedup | 1 | > 11.49 | > 65.62 | > 22.95 | > 180 000 | |
| Memory | - | 735 188 | 785 628 | 756 | 736 | |
| TrafficLight | Runtime | > 1800 | 47.04 | 9.05 | 69.09 | 0.00 |
| Speedup | 1 | > 38.27 | > 198.9 | > 26.05 | > 180 000 | |
| Memory | - | 855 112 | 447 828 | 756 | 736 | |
| Sieve | Runtime | 76.31 | 7.71 | 6.49 | 14.63 | 8.94 |
| Speedup | 1 | 9.9 | 11.76 | 5.22 | 8.54 | |
| Memory | 398 980 | 1 415 428 | 1 096 284 | 32 472 | 35 732 | |
| Scheduler | Runtime | 786.74 | 10.62 | 10.49 | 21.57 | 10.32 |
| Speedup | 1 | 74.08 | 74.99 | 36.47 | 76.23 | |
| Memory | 5 341 316 | 414 772 | 398 924 | 816 | 820 | |
| sort_m2_data1000 | Runtime | 17.27 | 3.27 | 2.10 | 0.2 | 0.03 |
| Speedup | 1 | 5.28 | 8.22 | 86.35 | 575.67 | |
| Memory | 577 808 | 191 280 | 143 864 | 1192 | 1104 | |
| CAN Bus | Runtime | 273.58 | 7.23 | 6.81 | 7.23 | 2.91 |
| Speedup | 1 | 37.84 | 40.17 | 37.84 | 94.01 | |
| Memory | 167 284 | 428 084 | 402 432 | 968 | 952 | |
| Train | Runtime | 241.16 | 13.31 | 12.83 | 18.55 | 8.10 |
| Speedup | 1 | 18.11 | 18.8 | 13 | 29.77 | |
| Memory | 163 476 | 377 292 | 376 540 | 984 | 1016 | |
| Cruise Controller | Runtime | > 1800 | 21.26 | 15.26 | 11.90 | 0.30 |
| Speedup | 1 | > 84.67 | > 117.96 | > 151.26 | > 6000 | |
| Memory | - | 750 816 | 484 948 | 864 | 820 |
Results (Rust)
Rust development was done on a different system, therefore benchmarks are not comparable to the old table. These benchmarks where run on a Ryzen 7 1700 under Debian via wsl (Win 10) (Memory values seem pretty high. GNU time had a bug for reporting 4x the RSS, but I'm using version 1.9 here, which apparently has it fixed...)
| Machines | ProB | Java PI | Java BI | C++ PI -O1 | C++ PI -O2 | Rust PI O1 | Rust PI O2 | Rust PI O3 | Rust BI O2 | Rust BI O3 | |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Lift | Runtime | > 1200 | 11.85 | 102.67 | 51.05 | 00.00 | 20.55 | 18.43 | 18.49 | 685.03 | 705.46 |
| Speedup | |||||||||||
| Memory | - | 2 220 976 | 2 247 676 | 3120 | 3060 | 2160 | 2276 | 2168 | 2572 | 2584 | |
| TrafficLight | Runtime | > 1200 | 05.21 | 17.40 | 51.35 | 00.00 | 21.31 | 10.87 | 10.78 | 78.33 | 80.27 |
| Speedup | |||||||||||
| Memory | - | 1 400 352 | 2 202 788 | 3188 | 3188 | 2312 | 2256 | 2312 | 2496 | 2664 | |
| Sieve | Runtime | 83.76 | 07.41 | 08.04 | 26.15 | 06.86 | 53.04 | 09.03 | 09.06 | 39.27 | 39.54 |
| Speedup | 1 | 11.3 | 10.42 | 3.2 | 12.2 | 1.58 | 9.28 | 9.25 | 2.13 | 2.12 | |
| Memory | 414 232 | 2 094 128 | 2 079 056 | 165 528 | 165 548 | 104 764 | 104 608 | 104 604 | 450 804 | 450 688 | |
| Scheduler | Runtime | 429.98 | 06.39 | 06.39 | 14.25 | 01.98 | 34.97 | 06.14 | 06.04 | 06.28 | 06.00 |
| Speedup | 1 | 67.29 | 67.29 | 30.17 | 217.16 | 12.3 | 70.03 | 71.19 | 68.47 | 71.66 | |
| Memory | 14 738 152 | 1 422 120 | 1 415 844 | 3080 | 3136 | 2384 | 2228 | 2324 | 2528 | 2584 | |
| sort_m2_data1000 | Runtime | 18.99 | 02.02 | 02.15 | 00.20 | 00.03 | 02.77 | 00.50 | 00.51 | 01.11 | 01.15 |
| Speedup | 1 | 9.4 | 8.83 | 94.95 | 633 | 6.86 | 37.98 | 37.24 | 17.11 | 16.51 | |
| Memory | 594 428 | 204 220 | 206 676 | 3412 | 3420 | 5312 | 5216 | 5328 | 10072 | 9872 | |
| CAN Bus | Runtime | 310.92 | 05.17 | 05.15 | 05.80 | 00.59 | 19.83 | 03.16 | 03.18 | 06.36 | 06.47 |
| Speedup | 1 | 60.14 | 60.37 | 53.61 | 526.98 | 15.68 | 98.39 | 97.77 | 48.89 | 48.06 | |
| Memory | 184 356 | 930 816 | 917 552 | 3364 | 3208 | 2668 | 2540 | 2508 | 2912 | 2928 | |
| Train | Runtime | 66.66 | 07.40 | 07.57 | 13.19 | 01.64 | 31.52 | 04.76 | 04.71 | 02.78 | 02.77 |
| Speedup | 1 | 9.01 | 8.81 | 5.05 | 40.65 | 2.11 | 14 | 14.15 | 23.98 | 24.06 | |
| Memory | 179 880 | 1 420 528 | 1419832 | 3224 | 3372 | 2740 | 2636 | 2612 | 2856 | 2812 | |
| Cruise Controller | Runtime | > 1200 | 13.91 | 14.66 | 08.34 | 00.04 | 05.15 | 05.43 | 05.33 | 14.20 | 14.64 |
| Speedup | |||||||||||
| Memory | - | 1 401 192 | 1 400 232 | 3160 | 3092 | 2376 | 2540 | 2352 | 2668 | 2668 |
Runtime in Seconds
Memory Usage in KB
BI = Big Integer
PI = Primitive Integer