diff --git a/benchmarks/execution/README.md b/benchmarks/execution/README.md index 07953459cd8af355f492941a1f3fa64f5d1d7017..ee8b5d5e445c7955d6b720e7ceaff9cb8438aabb 100644 --- a/benchmarks/execution/README.md +++ b/benchmarks/execution/README.md @@ -46,32 +46,32 @@ 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 | | 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** | 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** | 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** | 07.41 | 08.04 | 26.15 | 06.86 | 53.04 | 09.03 | 09.06 | 39.27 | 39.54 | -| | **Speedup** | | | | | | | | | | -| | **Memory** | 2 094 128 | 2 079 056 | 165 528 | 165 548 | 104 764 | 104 608 | 104 604 | 450 804 | 450 688 | -| Scheduler | **Runtime** | 06.39 | 06.39 | 14.25 | 01.98 | 34.97 | 06.14 | 06.04 | 06.28 | 06.00 | -| | **Speedup** | | | | | | | | | | -| | **Memory** | 1 422 120 | 1 415 844 | 3080 | 3136 | 2384 | 2228 | 2324 | 2528 | 2584 | -| sort_m2_data1000 | **Runtime** | 02.02 | 02.15 | 00.20 | 00.03 | 02.77 | 00.50 | 00.51 | 01.11 | 01.15 | -| | **Speedup** | | | | | | | | | | -| | **Memory** | 204 220 | 206 676 | 3412 | 3420 | 5312 | 5216 | 5328 | 10072 | 9872 | -| CAN Bus | **Runtime** | 05.17 | 05.15 | 05.80 | 00.59 | 19.83 | 03.16 | 03.18 | 06.36 | 06.47 | -| | **Speedup** | | | | | | | | | | -| | **Memory** | 930 816 | 917 552 | 3364 | 3208 | 2668 | 2540 | 2508 | 2912 | 2928 | -| Train | **Runtime** | 07.40 | 07.57 | 13.19 | 01.64 | 31.52 | 04.76 | 04.71 | 02.78 | 02.77 | -| | **Speedup** | | | | | | | | | | -| | **Memory** | 1 420 528 | 1419832 | 3224 | 3372 | 2740 | 2636 | 2612 | 2856 | 2812 | -| Cruise Controller | **Runtime** | 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 | +| 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