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
|
type X;
const nil: X;
type lmap;
function {:linear "mem"} dom(lmap): [int]bool;
function map(lmap): [int]int;
function cons([int]bool, [int]int) : lmap;
axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);
var {:qed} {:linear "mem"} g: lmap;
const p: int;
procedure {:yields} TransferToGlobal({:cnst "tid"} tid: X, {:linear "mem"} l: lmap);
ensures {:both 1} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;
procedure {:yields} TransferFromGlobal({:cnst "tid"} tid: X) returns ({:linear "mem"} l: lmap);
ensures {:both 1} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;
procedure {:yields} Load({:cnst "tid"} tid: X, {:cnst "mem"} l: lmap, a: int) returns (v: int);
ensures {:both 1} |{ A: assert tid != nil && lock == tid; v := map(l)[a]; return true; }|;
procedure {:yields} Store({:cnst "tid"} tid: X, {:linear "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);
ensures {:both 1} |{ A: assert tid != nil && lock == tid; assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;
procedure {:yields} P({:cnst "tid"} tid: X)
requires {:phase 2} tid != nil && Inv(g);
ensures {:phase 2} Inv(g);
{
var t: int;
var {:linear "mem"} l: lmap;
par Yield();
call Acquire(tid);
call l := TransferFromGlobal(tid);
call t := Load(tid, l, p);
call l := Store(tid, l, p, t+1);
call t := Load(tid, l, p+4);
call l := Store(tid, l, p+4, t+1);
call TransferToGlobal(tid, l);
call Release(tid);
par Yield();
}
procedure {:yields} {:stable} Yield()
requires {:phase 2} Inv(g);
ensures {:phase 2} Inv(g);
{
yield;
assert {:phase 2} Inv(g);
}
function {:inline} Inv(g: lmap) : bool
{
dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]
}
var {:qed} b: bool;
var {:qed} lock: X;
procedure {:yields} Acquire({:cnst "tid"} tid: X)
free requires {:phase 1} InvLock(lock, b);
ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; b := true; lock := tid; return true; }|;
{
var status: bool;
var tmp: X;
par YieldLock();
L:
assert {:phase 1} InvLock(lock, b);
call status := CAS(tid, false, true);
par YieldLock();
goto A, B;
A:
assume status;
return;
B:
assume !status;
goto L;
}
procedure {:yields} CAS(tid: X, prev: bool, next: bool) returns (status: bool);
ensures {:atomic 0} |{
A: goto B, C;
B: assume b == prev; b := next; status := true; lock := tid; return true;
C: status := false; return true;
}|;
procedure {:yields} Release({:cnst "tid"} tid: X);
ensures {:left 1} |{ A: assert lock == tid && tid != nil; b := false; lock := nil; return true; }|;
procedure {:yields} {:stable} YieldLock()
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
{
yield;
assert {:phase 1} InvLock(lock, b);
}
function {:inline} InvLock(lock: X, b: bool) : bool
{
lock != nil <==> b
}
|
