blob: 5107fd38884e130ba8cc6cc39aab18f77e871322 (
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
|
class Cell {
var x: int;
// use starred read permission
invariant rd*(x);
method a1(c: Cell)
requires c != null && rd(c.mu) && waitlevel << c;
{
acquire c;
assert(rd*(c.x));
release c;
assert(rd*(c.x));
}
method a2(c: Cell)
requires c != null && rd(c.mu) && waitlevel << c;
{
acquire c;
assert(rd(c.x)); // ERROR: should fail
release c;
assert(rd(c.x)); // ERROR: should fail
}
method a3()
{
var c: Cell := new Cell;
share c;
assert(rd*(c.x));
acquire c;
unshare c;
assert(rd*(c.x));
}
method a4()
{
var c: Cell := new Cell;
share c;
assert(rd(c.x)); // ERROR: should fail
}
method a5()
{
var c: Cell := new Cell;
share c;
acquire c;
unshare c;
assert(rd(c.x)); // ERROR: should fail
}
}
class Cell2 {
var x: int;
// use normal fractional permission
invariant rd(x);
method a1(c: Cell2)
requires c != null && rd(c.mu) && waitlevel << c;
{
acquire c;
assert(rd*(c.x));
release c;
assert(rd*(c.x)); // ERROR: we gave away all permission
}
method a2(c: Cell2)
requires c != null && rd(c.mu) && waitlevel << c;
{
acquire c;
assert(rd(c.x)); // ERROR: should fail
release c;
assert(rd(c.x)); // ERROR: should fail
}
method a3()
{
var c: Cell2 := new Cell2;
share c;
assert(rd*(c.x));
call void(c);
assert(rd*(c.x));
call dispose(c);
assert(rd*(c.x));
acquire c;
unshare c;
assert(rd*(c.x));
assert(acc(c.x)); // ERROR: should fail
}
method a4(c: Cell2)
requires c != null && acc(c.mu) && holds(c);
requires rd(c.x);
lockchange c
{
release c; // ERROR: should fail, we don't have enough permission
}
method a5()
{
var c: Cell2 := new Cell2;
share c;
acquire c;
assert(acc(c.x));
unshare c;
assert(acc(c.x));
}
method a6(c: Cell2)
requires acc(c.x,rd(c)) && acc(c.mu) && c.mu == lockbottom
{
var n: int;
share c;
rd acquire c;
n := c.x
rd release c;
n := c.x // ERROR: no read access possible
acquire c;
unshare c;
}
method void(c: Cell2) requires rd(c.x); ensures rd(c.x); {}
method dispose(c: Cell2) requires rd(c.x); {}
}
|
