blob: d26dedbbf5d25279a4b8e8411ef42c4dad9b6b58 (
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
|
class Cell
{
var inner: InnerCell;
predicate inv
{
acc(inner) && inner!=null && rd(inner.value,1) && rd*(inner.mu) && rd*(this.mu)
}
method CellConstructor()
requires acc(inner) && acc(this.mu)
ensures inv && get()==0;
{
inner := new InnerCell;
call inner.InnerCellConstructor(0)
share inner;
fold inv;
}
method CellConstructor2(other: Cell)
requires acc(inner) && acc(this.mu)
requires other != null && other.inv;
requires unfolding other.inv in waitlevel << other.inner.mu
ensures inv && other.inv && get()==other.get();
{
unfold other.inv;
inner := other.inner;
acquire inner;
inner.refCount := inner.refCount+1;
release inner;
fold other.inv;
fold inv;
}
function get():int
requires inv;
{ unfolding inv in inner.value }
method set(x:int)
requires inv;
requires unfolding inv in waitlevel << inner.mu
ensures inv && get()==x;
{
var old_in: InnerCell;
unfold inv;
old_in := inner;
acquire old_in;
if (inner.refCount==1) { inner.value:=x; }
else
{
inner.refCount := inner.refCount-1;
inner := new InnerCell;
call inner.InnerCellConstructor(x)
share inner;
}
release old_in;
fold inv;
}
}
class InnerCell
{
var value: int;
var refCount: int;
invariant acc(refCount) && refCount > 0 && acc(value,100-rd(refCount));
method InnerCellConstructor(val: int)
requires acc(refCount) && acc(value)
ensures acc(refCount) && acc(value) && refCount==1 && value == val;
{
refCount := 1;
value := val
}
}
|
