blob: e8ab1a6025efb045262b5520751a2beeaf6ffd54 (
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
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) && maxlock << ch.mu
requires credit(ch)
ensures rd(ch.mu)
{
var c: Cell
receive c := ch
while (c != null)
invariant rd(ch.mu) && maxlock << ch.mu
invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
{
var i := c.val
receive c := ch
}
}
// variations
method Main0() { // error: debt remains after body
var ch := new Ch
fork tk0 := Producer(ch)
fork tk1 := Consumer(ch)
// join tk0
join tk1
}
method Main1() {
var ch := new Ch
fork tk0 := Producer(ch)
fork tk1 := Consumer(ch)
join tk0
// join tk1
} // no problem
method Producer0(ch: Ch) // error: debt remains after body
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 Producer1(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 + c.val // error: can no longer read c.val
}
send ch(null)
}
method Consumer0(ch: Ch)
requires rd(ch.mu) && maxlock << ch.mu
requires credit(ch)
ensures rd(ch.mu)
{
var c: Cell
receive c := ch
while (c != null && c.val == 7) // this consumer may end early, but that's allowed
invariant rd(ch.mu) && maxlock << ch.mu
invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
{
var i := c.val
receive c := ch
}
}
method Consumer1(ch: Ch)
requires rd(ch.mu) && maxlock << ch.mu
requires credit(ch)
ensures rd(ch.mu)
{
var c: Cell
receive c := ch
if (c != null) {
assert 0 <= c.val // follows from where clause
}
}
method Consumer2(ch: Ch)
requires rd(ch.mu) && maxlock << ch.mu
requires credit(ch)
ensures rd(ch.mu)
{
var c: Cell
receive c := ch
if (c != null) {
assert c.val < 2 // error: does not follow from where clause
}
}
}
|
