blob: 7f2f9c44525f2de47f9cd1e83f5ba243b45f5d77 (
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
|
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type Tid;
var {:layer 0,1} a:[Tid]int;
procedure {:yields} {:layer 1} main() {
var {:linear "tid"} tid:Tid;
yield;
while (true) {
call tid := Allocate();
async call P(tid);
yield;
}
yield;
}
procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid)
ensures {:layer 1} a[tid] == old(a)[tid] + 1;
{
var t:int;
yield;
assert {:layer 1} a[tid] == old(a)[tid];
call t := Read(tid);
yield;
assert {:layer 1} a[tid] == t;
call Write(tid, t + 1);
yield;
assert {:layer 1} a[tid] == t + 1;
}
procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
{
yield;
call tid := AllocateLow();
yield;
}
procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
ensures {:atomic}
|{A:
val := a[tid]; return true;
}|;
procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);
ensures {:atomic}
|{A:
a[tid] := val; return true;
}|;
procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
ensures {:atomic} |{ A: return true; }|;
function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
{
MapConstBool(false)[x := true]
}
function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
{
x
}
|
