MCMT: Experiments
Timings have been obtained on a Pentium Intel 1.73 GHz with 1 Gb
Sdram running MCMT v.1.0 on Gentoo Linux. Further documentation on single examples is available in the distribution.
In the first table, statistics are relative to the default configuration of the tool, whereas the second table refers to the best
setting we found for each example (thus, in the second table, various heuristics for invariant synthesis, signature abstraction
and acceleration can have been applied). We are far from having explored all possible settings,
we just tried few of them, hence the real 'best setting' has sometimes still to be found.
Timeouts are mostly due to
trivial divergence reasons that the default setting is not able to capture. A couple of lines
of the Default Setting Table are empty:
this is because a non-default setting has been adopted in order
to manually suggest the tool invariants to be checked (these are the only two cases where
invariants are not generated automatically).
- Mutual exclusion algorithms
Default Setting
|
  |
depth |
#nodes |
#deleted nodes |
#SMT calls |
time (sec) |
Bakery |
2 |
1 |
0 |
6 |
0.00 |
Bakery_bogus |
8 |
90 |
14 |
1413 |
0.81 |
Bakery_e |
12 |
48 |
17 |
439 |
0.20 |
Bakery_Lamport   |
12 |
56 |
15 |
595 |
0.27 |
Bakery_t |
9 |
28 |
5 |
251 |
0.11 |
Burns |
14 |
56 |
7 |
373 |
0.14 |
Dijkstra |
14 |
122 |
37 |
2920 |
2.11 |
Dijkstra1 |
13 |
38 |
11 |
222 |
0.10 |
Distrib_Lamport |
23 |
913 |
242 |
47574 |
120.62 |
Java M-lock |
9 |
23 |
2 |
289 |
0.10 |
Mux_Sem |
7 |
8 |
2 |
57 |
0.02 |
Rickart_Agrawala |
13 |
458 |
119 |
35355 |
187.04 |
Sz_fp |
22 |
277 |
3 |
7703 |
5.12 |
Sz_fp_ver |
30 |
284 |
38 |
10611 |
6.66 |
Szymanski |
17 |
136 |
10 |
2529 |
1.60 |
Szymanski_at |
23 |
1745 |
311 |
424630 |
540.19 |
Ticket |
9 |
18 |
0 |
284 |
0.17 |
|
Best Setting
|
  |
depth |
#nodes |
#deleted nodes |
#SMT calls |
#invar. found |
time (sec) |
Bakery |
2 |
1 |
0 |
6 |
0 |
0.00 |
Bakery_bogus |
8 |
53 |
4 |
1400 |
7 |
0.68 |
Bakery_e |
7 |
8 |
1 |
213 |
16 |
0.10 |
Bakery_Lamport   |
4 |
7 |
1 |
209 |
7 |
0.08 |
Bakery_t |
7 |
8 |
1 |
134 |
5 |
0.06 |
Burns |
2 |
2 |
1 |
53 |
3 |
0.02 |
Dijkstra |
2 |
1 |
1 |
215 |
12 |
0.08 |
Dijkstra1 |
2 |
1 |
1 |
35 |
2 |
0.02 |
Distrib_Lamport |
23 |
248 |
42 |
19254 |
7 |
32.84 |
Java M-lock |
9 |
23 |
2 |
289 |
0 |
0.10 |
Mux_Sem |
2 |
1 |
1 |
65 |
6 |
0.02 |
Rickart_Agrawala |
13 |
458 |
119 |
35355 |
0 |
187.04 |
Sz_fp |
22 |
277 |
3 |
7703 |
0 |
5.12 |
Sz_fp_ver |
30 |
284 |
38 |
10611 |
0 |
6.66 |
Szymanski |
9 |
14 |
5 |
882 |
12 |
0.30 |
Szymanski_at |
9 |
22 |
10 |
2987 |
42 |
1.25 |
Ticket |
9 |
18 |
0 |
284 |
0 |
0.17 |
|
- Cache coherence protocols
Default Setting
|
  |
depth |
#nodes |
#deleted nodes |
#SMT calls |
time (sec) |
Berkeley |
2 |
1 |
0 |
16 |
0.00 |
Futurebus |
8 |
37 |
3 |
998 |
0.96 |
German07 |
26 |
2442 |
576 |
121388 |
145.68 |
German_buggy |
16 |
1631 |
203 |
41497 |
49.70 |
German_ca |
9 |
13 |
0 |
62 |
0.03 |
German_pfs |
33 |
11605 |
2755 |
858184 |
31m 01s |
Illinois |
4 |
8 |
0 |
144 |
0.08 |
Illinois_ca |
3 |
3 |
1 |
48 |
0.02 |
Mesi |
3 |
2 |
0 |
9 |
0.00 |
Mesi_ca |
3 |
2 |
0 |
13 |
0.00 |
Moesi |
3 |
2 |
0 |
10 |
0.01 |
Moesi_ca |
3 |
2 |
0 |
13 |
0.00 |
Synapse |
2 |
1 |
0 |
16 |
0.01 |
Xerox P.D. |
7 |
13 |
0 |
388 |
0.23 |
|
Best Setting
|
  |
depth |
#nodes |
#deleted nodes |
#SMT calls |
#invar. found |
time (sec) |
Berkeley |
2 |
1 |
0 |
16 |
0 |
0.00 |
Futurebus |
8 |
37 |
3 |
998 |
0 |
0.96 |
German07 |
26 |
2442 |
576 |
121388 |
0 |
145.68 |
German_buggy |
16 |
1631 |
203 |
41497 |
0 |
49.70 |
German_ca |
9 |
13 |
0 |
62 |
0 |
0.03 |
German_pfs |
33 |
11141 |
2673 |
784168 |
149 |
30m 27s |
Illinois |
4 |
8 |
0 |
144 |
0 |
0.08 |
Illinois_ca |
3 |
3 |
1 |
48 |
0 |
0.02 |
Mesi |
3 |
2 |
0 |
9 |
0 |
0.00 |
Mesi_ca |
3 |
2 |
0 |
13 |
0 |
0.00 |
Moesi |
3 |
2 |
0 |
10 |
0 |
0.01 |
Moesi_ca |
3 |
2 |
0 |
13 |
0 |
0.00 |
Synapse |
2 |
1 |
0 |
16 |
0 |
0.01 |
Xerox P.D. |
7 |
13 |
0 |
388 |
0 |
0.23 |
|
- Imperative Programs
Default Setting
|
  |
depth |
#nodes |
#deleted nodes |
#SMT calls |
time (sec) |
Find |
4 |
27 |
7 |
691 |
0.90 |
Max_in_Array |
- |
- |
- |
- |
timeout |
Strcat |
- |
- |
- |
- |
timeout |
Strcmp |
- |
- |
- |
- |
timeout |
Strcopy |
3 |
3 |
1 |
694 |
1.22 |
|
Best Setting
|
  |
depth |
#nodes |
#deleted nodes |
#calls |
#invar. found |
time (sec) |
Find |
4 |
27 |
7 |
691 |
0 |
0.90 |
Max_in_Array |
2 |
1 |
1 |
46 |
5 |
0.03 |
Strcat |
2 |
2 |
2 |
80 |
2 |
0.07 |
Strcmp |
2 |
1 |
1 |
21 |
3 |
0.01 |
Strcopy |
3 |
3 |
2 |
564 |
4 |
0.38 |
|
- Miscellanea
Default Setting
|
  |
depth |
#nodes |
#deleted nodes |
#SMT calls |
time (sec) |
Alternating_bit |
  |
  |
  |
  |
  |
Bakery |
6 |
12 |
0 |
86 |
0.04 |
Bakery2 |
6 |
22 |
1 |
247 |
0.07 |
Controller |
6 |
8 |
0 |
95 |
0.03 |
Csm |
- |
- |
- |
- |
timeout |
Filter_simple |
59 |
132 |
0 |
1363 |
2.53 |
Fischer |
10 |
16 |
2 |
336 |
0.16 |
Fischer_U |
8 |
13 |
3 |
198 |
0.08 |
German |
26 |
2642 |
678 |
157870 |
191.39 |
Ins_sort |
- |
- |
- |
- |
timeout |
MIS |
  |
  |
  |
  |
  |
Mux_Sem |
7 |
15 |
0 |
174 |
0.04 |
Mux_Sem_param |
4 |
5 |
0 |
85 |
0.04 |
Order |
3 |
3 |
0 |
18 |
0.01 |
Simple |
2 |
1 |
0 |
10 |
0.00 |
Swimming_Pool |
3 |
81 |
0 |
1300 |
0.67 |
Szymanski+ |
21 |
685 |
102 |
43236 |
47.00 |
Ticket_o |
- |
- |
- |
- |
timeout |
Token_Ring |
3 |
2 |
0 |
30 |
0.02 |
Tricky |
8 |
7 |
0 |
22 |
0.02 |
Two_Semaphores |
4 |
5 |
1 |
48 |
0.02 |
|
Best Setting
|
  |
depth |
#nodes |
#deleted nodes |
#SMT calls |
#invar. found |
time (sec) |
Alternating_bit |
21 |
1008 |
156 |
41894 |
1 |
44.48 |
Bakery |
6 |
12 |
0 |
86 |
0 |
0.04 |
Bakery2 |
6 |
22 |
1 |
247 |
0 |
0.07 |
Controller |
6 |
8 |
0 |
95 |
0 |
0.03 |
Csm |
2 |
2 |
2 |
76 |
1 |
0.02 |
Filter_simple |
59 |
132 |
0 |
1363 |
0 |
2.53 |
Fischer |
10 |
16 |
2 |
336 |
0 |
0.16 |
Fischer_U |
8 |
13 |
3 |
198 |
0 |
0.08 |
German |
26 |
2642 |
678 |
157870 |
0 |
191.39 |
Ins_sort |
2 |
2 |
1 |
40 |
1 |
0.04 |
MIS |
1 |
0 |
0 |
1261 |
95 |
0.85 |
Mux_Sem |
7 |
15 |
0 |
174 |
0 |
0.04 |
Mux_Sem_param |
2 |
3 |
1 |
57 |
4 |
0.02 |
Order |
2 |
2 |
2 |
16 |
2 |
0.01 |
Simple |
2 |
1 |
0 |
10 |
0 |
0.00 |
Swimming_Pool |
3 |
62 |
3 |
927 |
0 |
0.73 |
Szymanski+ |
2 |
1 |
1 |
90 |
2 |
0.04 |
Ticket_o |
3 |
4 |
2 |
201 |
10 |
0.06 |
Token_Ring |
3 |
2 |
0 |
30 |
0 |
0.02 |
Tricky |
2 |
1 |
1 |
13 |
1 |
0.00 |
Two_Semaphores |
4 |
5 |
1 |
48 |
0 |
0.02 |
|