blob: c52bb10af9b9fdb89e1d66fe8a9ce6d8fbe50628 (
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
|
class C {
var f: int;
method main(n: int)
requires n > 0 && acc(this.f)
ensures acc(this.f)
{
// fork all threads, and join them afterwards
call work(n);
this.f := 100; // we want a full permission in the end
}
method work(n: int)
requires rd(this.f,n)
ensures rd(this.f,n)
{
var tks:seq<token<C.m>> := nil<token<C.m>>;
// first loop; fork all threads
var i := 0;
while (i < n)
invariant i <= n && |tks| == i;
invariant i < n ==> rd(this.f,n-i);
invariant acc(tks[*].joinable);
invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
{
fork tk := m();
tks := tks ++ [tk];
i := i+1;
}
// second loop; join all threads
i := n;
while (i > 0)
invariant i >= 0 && |tks| == i;
invariant i < n ==> rd(this.f,n-i); // BUG: the eval construct inside the quantification does not give us the information needed to proof this invariant, see http://boogie.codeplex.com/workitem/10187
invariant acc(tks[*].joinable);
invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
{
var tk: token<C.m>;
tk := tks[i-1];
join tk;
i := i-1;
tks := tks[0..i];
}
}
method m()
requires rd(this.f,1);
ensures rd(this.f,1);
{ /* do some computation */ }
}
|
