blob: 828cf0056250719cf8a4bf651eb46e62fcbaeb0a (
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
143
144
145
146
147
148
149
150
151
152
|
class Counter {
var value: int;
invariant acc(value) && old(value)<=value;
}
class Program {
method main1(){
var counter := new Counter;
counter.value := 0;
share counter;
acquire counter;
var tmp1 := counter.value;
release counter;
acquire counter;
var tmp2 := counter.value;
release counter;
assert tmp1 <= tmp2;
}
method main2(){
var counter := new Counter;
counter.value := 0;
share counter;
acquire counter;
release counter;
call bar(counter);
}
method bar(c: Counter)
requires c!=null && acc(c.mu) && waitlevel << c.mu;
requires eval(c.release, acc(c.value) && 0<=c.value);
{
lock (c) {
assert 0 <= c.value; // ok, because of the lastSeen conjunct in the precondition
}
}
method main3() returns (counter: Counter)
lockchange counter;
{
counter := new Counter;
counter.value := 0;
share counter;
acquire counter;
call doRelease(counter, counter.value);
}
method doRelease(c: Counter, i: int)
requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && i<=c.value);
lockchange c;
{
release c; // ok, because of atAcquire conjunct in the precondition
}
method main4(){
var counter := new Counter;
counter.value := 0;
share counter;
acquire counter;
counter.value := counter.value - 1;
release counter; // error: should fail
}
method main5(){
var counter := new Counter;
counter.value := 10;
share counter;
call foo(counter);
unshare counter;
assert 10<=counter.value; // error: should fail
}
method foo(c: Counter)
requires c!=null && acc(c.mu) && waitlevel << c.mu && eval(c.release, acc(c.value) && 10<=c.value);
ensures c!=null && holds(c) && acc(c.mu) && acc(c.value);
lockchange c;
{
acquire c;
unshare c;
c.value := 5;
share c;
acquire c;
}
method nestedGood0(c: Counter)
requires c != null && acc(c.mu) && waitlevel << c.mu;
{
lock (c) {
release c
acquire c
}
}
method nestedGood1(c: Counter)
requires c != null && acc(c.mu) && waitlevel << c.mu;
{
var t: Counter := c
lock (t) {
t := new Counter
share t
acquire t
} // this line releases the original value for t
release t
}
method nestedBad0(c: Counter)
requires c != null && acc(c.mu) && waitlevel << c.mu;
{
lock (c) {
release c
} // error: no longer holds c
}
method nestedBad1(c: Counter)
requires c != null && acc(c.mu) && waitlevel << c.mu;
{
lock (c) {
acquire c // error: already holds c
}
}
method nestedBad2(c: Counter)
requires c != null && acc(c.mu) && waitlevel << c.mu;
{
lock (c) {
lock (c) { // error: already holds c
}
}
}
method nestedBad3(c: Counter)
requires c != null && acc(c.mu) && waitlevel << c.mu;
{
var t: Counter := c
lock (t) {
release t
t := new Counter
share t
acquire t
} // error: this line attempts to release the original t
}
}
|
