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: 4ba7747dacda81e57d44830b45e768785a7be4d8
• 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