blob: abac4f5c30abd63357c0e3cee218ebd8dc56ce4c (
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
|
class Cell {
var val: int
}
channel Ch(c: Cell) where
c != null ==> acc(c.val) && 0 <= c.val && credit(this)
class Program {
method Main() {
var ch := new Ch
fork tk0 := Producer(ch)
fork tk1 := Consumer(ch)
join tk0
join tk1
}
method Producer(ch: Ch)
requires ch != null
ensures credit(ch)
{
var i := 0
while (i < 25)
{
var x := i*i
var c := new Cell { val := x }
send ch(c)
i := i + 1
}
send ch(null)
}
method Consumer(ch: Ch)
requires rd(ch.mu) && waitlevel << ch.mu
requires credit(ch)
ensures rd(ch.mu)
{
var c: Cell
receive c := ch
while (c != null)
invariant rd(ch.mu) && waitlevel << ch.mu
invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
{
var i := c.val
receive c := ch
}
}
}
|
