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
|
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
{
MapConstBool(false)[x := true]
}
type X;
const nil: X;
var {:layer 0,2} b: bool;
var {:layer 1,3} lock: X;
procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X)
requires {:layer 2} tid != nil;
requires {:layer 2} InvLock(lock, b);
ensures {:layer 2} InvLock(lock, b);
{
yield;
assert {:layer 2} InvLock(lock, b);
while (*)
invariant {:layer 2} InvLock(lock, b);
{
call Enter(tid);
call Leave(tid);
yield;
assert {:layer 2} InvLock(lock, b);
}
yield;
assert {:layer 2} InvLock(lock, b);
}
function {:inline} InvLock(lock: X, b: bool) : bool
{
lock != nil <==> b
}
procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X)
requires {:layer 2} tid != nil;
requires {:layer 2} InvLock(lock, b);
ensures {:layer 2} InvLock(lock, b);
ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|;
{
yield;
assert {:layer 2} InvLock(lock, b);
call LowerEnter(tid);
yield;
assert {:layer 2} InvLock(lock, b);
}
procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X)
requires {:layer 2} InvLock(lock, b);
ensures {:layer 2} InvLock(lock, b);
ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;
{
yield;
assert {:layer 2} InvLock(lock, b);
call LowerLeave();
yield;
assert {:layer 2} InvLock(lock, b);
}
procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X)
ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
{
var status: bool;
yield;
L:
call status := CAS(false, true);
if (status) {
call SetLock(tid);
}
yield;
goto A, B;
A:
assume status;
yield;
return;
B:
assume !status;
goto L;
}
procedure {:yields} {:layer 1,2} LowerLeave()
ensures {:atomic} |{ A: b := false; lock := nil; return true; }|;
{
yield;
call SET(false);
call SetLock(nil);
yield;
}
procedure {:layer 1} {:inline 1} SetLock(v: X)
modifies lock;
{
lock := v;
}
procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool);
ensures {:atomic} |{
A: goto B, C;
B: assume b == prev; b := next; status := true; return true;
C: status := false; return true;
}|;
procedure {:yields} {:layer 0,1} SET(next: bool);
ensures {:atomic} |{ A: b := next; return true; }|;
|
