blob: 5ccce089006ea0448f22832125f24c0e36d41fb1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
class LoopLockChange {
method Test0()
requires rd(mu) && waitlevel << mu
lockchange this;
{
acquire this;
var b := true;
while(b) // error: lockchange clause of loop must include all lock changes that happened before the loop
{
b := false;
}
}
method Test1()
requires rd(mu) && waitlevel << mu
lockchange this;
{
acquire this;
var b := true;
while(b)
lockchange this;
{
b := false;
}
}
method Test2()
requires rd(mu) && waitlevel << mu
lockchange this;
{
var b := true;
while(b) // error: insufficient lockchange clause
invariant rd(mu);
invariant b ==> waitlevel << mu
{
acquire this;
b := false;
}
}
method Test3()
requires rd(mu) && waitlevel << mu
lockchange this;
{
var b := true;
while(b)
invariant rd(mu);
invariant b ==> waitlevel << mu
lockchange this;
{
acquire this;
b := false;
}
}
method Test4(p: LoopLockChange)
requires rd(p.mu) && waitlevel << p.mu
requires rd(mu) && waitlevel << mu
{
var current: LoopLockChange := this;
var b := true;
while(b)
invariant rd(current.mu)
invariant b ==> rd(p.mu);
invariant b ==> waitlevel << current.mu
lockchange current; // error: after the loop body, current does no longer point to the object whose lock was acquired
{
acquire current;
current := p;
b := false;
}
assume false; // to prevent complaint about method's lockchange clause
}
method Test5(p: LoopLockChange)
requires rd(p.mu) && waitlevel << p.mu
requires rd(mu) && waitlevel << mu
lockchange this;
{
var current: LoopLockChange := this;
var b := true;
while(b)
invariant rd(current.mu)
invariant b ==> rd(p.mu);
invariant b ==> current == this;
invariant b ==> waitlevel << current.mu
lockchange this;
{
acquire current;
current := p;
b := false;
}
}
method Test6()
requires rd(mu) && waitlevel << mu
{
var b := true;
while(b)
invariant rd(mu);
invariant b ==> waitlevel << mu
invariant b ==> !(rd holds(this))
invariant !b ==> holds(this)
lockchange this;
{
acquire this;
b := false;
}
release this;
}
method Test7()
requires rd(mu) && waitlevel << mu
{
acquire this;
release this;
}
// The following test requires a better treatment of allocation, which we don't have yet
/* method Test8()
{
var tmp : LoopLockChange := this;
var b := false;
while(b)
{
tmp := new LoopLockChange;
share tmp;
acquire tmp;
b := false;
}
assert !holds(tmp);
}
*/
}
|
