Structural Invariants for Parameterized Architectures
243
Benchmark
size
#st. / #cls.
Properties
time
(s.)
trap
#st. / #tr.
trap-inv
#st. / #tr.
flow
#st. / #tr.
flow-inv
#st. / #tr.
Berkeley
4 / 8
deadlock-freedom
consistency properties
0.37 18 / 95
18 / 78
12 / 50
7 / 18
Dragon
5 / 24
deadlock-freedom
consistency properties
1.63 39 / 433
32 / 159
54 / 537
11 / 57
Firefly
5 / 13
deadlock-freedom
consistency properties
0.53 55 / 409
36 / 200
38 / 309
11 / 44
Illinois
4 / 13
deadlock-freedom
consistency properties
0.46 14 / 83
11 / 32
16 / 95
9 / 38
MESI
4 / 8
deadlock-freedom
consistency properties
0.36 12 / 62
11 / 32
12 / 49
7 / 18
MOESI
5 / 10
deadlock-freedom
consistency properties
0.56 20 / 150
16 / 64
12 / 57
7 / 20
Synapse
3 / 6
deadlock-freedom
consistency properties
0.32 12 / 44
11 / 30
12 / 42
7 / 16
DijkstraScholten
4 / 6
deadlock-freedom
0.25 13 / 48
11 / 31
10 / 35
9 / 31
Bakery
3 / 4
deadlock-freedom
mutual exclusion
0.26 10 / 27
10 / 24
8 / 23
7 / 20
Burns
6 / 12
deadlock-freedom
mutual exclusion
0.30 10 / 64
9 / 30
8 / 35
7 / 32
Dijkstra
12 / 14
deadlock-freedom
mutual exclusion
11.86 375 / 11840 106 / 2887 13 / 148 10 / 110
Broadcast
MutEx
2 / 2
deadlock-freedom
mutual exclusion
0.23
9 / 22
9 / 21
8 / 19
7 / 16
Preemptive
(high)
5 / 4
deadlock-freedom
mutual exclusion
0.26 41 / 279
17 / 71
16 / 88
10 / 46
Preemptive
5 / 4
deadlock-freedom
mutual exclusion
0.25 28 / 173
22 / 97
20 / 113
12 / 62
Preemptive
(uninitialized)
3 / 3
deadlock-freedom
mutual exclusion
×
0.25 20 / 80
11 / 37
8 / 23
7 / 20
Semaphore
4 / 2
deadlock-freedom
mutual exclusion
0.23 14 / 39
9 / 32
10 / 36
8 / 30
Szymanski
15 / 31
deadlock-freedom
n.a.
mutual exclusion
n.a.
19.35 495 / 34990
n.a.
8 / 84
7 / 66
Dijkstra (ring)
10 / 9
deadlock-freedom
mutual exclusion
75.63 703 / 10160 1149 / 23195 20 / 247 20 / 387
Dining Cryptographers
7 / 15
deadlock-freedom
×
correctness
1.54 250 / 3232 288 / 2484
10 / 72
9 / 60
Dining
Philosophers
(global)
5 / 3
deadlock-freedom
0.23 32 / 145
19 / 98
15 / 77
11 / 56
Herman (linear)
3 / 3
deadlock-freedom
×
no token loss
0.25 19 / 70
14 / 42
10 / 33
9 / 27
Herman (ring)
3 / 4
deadlock-freedom
no token loss
0.26 19 / 71
14 / 42
10 / 33
9 / 27
Israeli-Jalfon
3 / 5
deadlock-freedom
no token loss
0.25 43 / 187
14 / 42
8 / 23
7 / 20
Dining
Philosophers
(lefty)
5 / 5
deadlock-freedom
0.25 37 / 219
27 / 167
12 / 63
11 / 57
Dining
Philosophers (lefty,
rem. forks)
6 / 5
deadlock-freedom
0.26 37 / 270
21 / 119
14 / 101
11 / 66
LehmannRabin
6 / 7
deadlock-freedom
0.26 39 / 361
23 / 211
11 / 67
11 / 73
Table 1: Experimental results of ostrich.