Comparative Performance of XMC (with and without compilation) and Murphi

Table 1-2: the RETHER protocol

Program		Time (second)			Space (MB)
		Compile	Verify	Total
retherA	XMC	0.07	0.19	0.26	0.78
	Compiled	0.15	0.22	0.37	0.58
	Murphi	6.72	0.42	7.14	0.03
retherB	XMC	0.07	0.38	0.45	0.87
	Compiled	0.15	0.47	0.62	0.64
	Murphi	6.72	1.35	9.07	0.10

Table 1-3: sieve with property ae_finish

Program		Time (second)			Space (MB)
		Compile	Verify	Total
sieve3	XMC	0.09	1.54	1.63	6.07
	Compiled	0.11	0.19	0.30	1.07
	Murphi	4.21	0.45	4.66	0.02
sieve4	XMC	0.09	4.41	4.50	16.61
	Compiled	0.11	0.40	0.51	2.49
	Murphi	4.18	1.13	5.31	0.05
sieve5	XMC	0.09	15.57	15.66	55.07
	Compiled	0.11	1.20	1.31	7.42
	Murphi	4.24	4.05	8.29	0.17
sieve6	XMC	0.09	68.67	68.76	227.53
	Compiled	0.11	5.02	5.13	28.35
	Murphi	4.33	18.51	22.84	0.67
sieve7	XMC	0.09	130.12	130.21	437.88
	Compiled	0.11	8.71	8.82	61.32
	Murphi	4.35	32.12	36.47	1.03

Table 1-4: sieve with property ee_fail

Program		Time (second)			Space (MB)
		Compile	Verify	Total
sieve3	XMC	0.09	1.04	1.13	1.11
	Compiled	0.11	0.11	0.22	0.59
	Murphi	3.28	0.14	3.42	0.01
sieve4	XMC	0.09	3.12	3.21	2.39
	Compiled	0.11	0.31	0.42	0.85
	Murphi	3.30	0.37	3.67	0.02
sieve5	XMC	0.09	11.52	11.92	6.58
	Compiled	0.11	0.99	1.10	1.63
	Murphi	3.32	1.13	4.44	0.08
sieve6	XMC	0.09	52.22	52.31	24.00
	Compiled	0.11	4.22	4.33	4.63
	Murphi	3.36	5.41	8.77	0.35
sieve7	XMC	0.09	101.21	101.30	37.20
	Compiled	0.11	7.50	7.61	8.28
	Murphi	3.37	9.51	12.88	0.53

Table 1-5: leader with property ae_leader

Program		Time (second)			Space (MB)
		Compile	Verify	Total
leader3	XMC	0.11	0.12	0.23	0.84
	Compiled	0.13	0.03	0.16	0.48
	Murphi	4.21	0.15	4.36	0.01
leader4	XMC	0.11	0.67	0.78	2.81
	Compiled	0.14	0.12	0.26	0.88
	Murphi	4.34	0.69	5.03	0.02
leader5	XMC	0.11	3.41	3.52	12.73
	Compiled	0.14	0.60	0.74	2.64
	Murphi	4.42	4.69	9.11	0.10
leader6	XMC	0.11	17.08	17.19	60.82
	Compiled	0.16	2.71	2.87	10.74
	Murphi	4.52	29.51	34.03	0.52
leader7	XMC	0.11	83.08	83.19	287.97
	Compiled	0.17	12.42	12.59	47.80
	Murphi	4.50	184.06	184.56	2.41

Table 1-6: leader with property one_leader

Program		Time (second)			Space (MB)
		Compile	Verify	Total
leader3	XMC	0.11	0.13	0.24	0.85
	Compiled	0.14	0.04	0.18	0.47
	Murphi	3.28	0.05	3.33	0.01
leader4	XMC	0.11	0.59	0.70	2.97
	Compiled	0.14	0.12	0.26	0.83
	Murphi	3.41	0.23	3.64	0.01
leader5	XMC	0.11	2.82	2.93	13.27
	Compiled	0.15	0.59	0.74	2.44
	Murphi	3.53	1.52	5.05	0.06
leader6	XMC	0.11	14.18	14.29	62.71
	Compiled	0.16	2.90	3.06	9.94
	Murphi	3.51	8.98	12.49	0.37
leader7	XMC	0.11	68.66	68.77	294.47
	Compiled	0.17	12.90	13.07	44.56
	Murphi	3.64	58.56	64.20	1.87

NOTE:

1. CPU time is used.
2. Compilation time for the original XMC is the time needed to preprocess and load an XL specification; for XMC with compilation, it is the time needed to compile XL specifications into rules and load the rules; for Murphi it is the time needed to generate C++ code from Murphi specification and compile it using g++.
3. For the i-protocol and rether, both versions of XMC compiled only once for all the configurations.
4. Space for Murphi represents only the estimated minimum hash table size. Auxiliary space usage is assumed to be small. Actual space usage is larger.

Table 2: Size of Compiled Programs

Program	processes	local transitions	global transitions
sieve3	5	13	19
sieve4	6	13	23
sieve5	7	13	27
sieve6	8	13	31
sieve7	9	13	35
leader3	6	15	36
leader4	8	15	48
leader5	10	15	60
leader6	12	15	72
leader7	14	15	84
rether	5	20	376
iproto	4	53	59