blob: f466b58aed3c933d379cfde2c90f38c73a92b9f6 (
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
|
class OwickiGries {
var counter: int
ghost var c0: int
ghost var c1: int
invariant acc(counter) && acc(c0,50) && acc(c1,50) && counter == c0 + c1
method Main() {
var og := new OwickiGries{ counter := 0, c0 := 0, c1 := 0 }
share og
fork tk0 := og.Worker(false)
fork tk1 := og.Worker(true)
join tk0; join tk1
acquire og; unshare og
assert og.counter == 2
}
method Worker(b: bool)
requires rd(mu) && waitlevel << mu
requires (!b ==> acc(c0,50)) && (b ==> acc(c1,50))
ensures rd(mu)
ensures !b ==> acc(c0,50) && c0 == old(c0) + 1
ensures b ==> acc(c1,50) && c1 == old(c1) + 1
{
lock (this) {
counter := counter + 1
if (!b) {
c0 := c0 + 1
} else {
c1 := c1 + 1
}
}
}
}
|