Chalice/tests/examples/OwickiGries.chalice


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
      }
    }
  }
}