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
|
// program inspired by "Proving Copyless Message Passing" (Villard, Lozes and Calcagno, APLAS 2009)
// msg tag indicates what the type of the message
// channel is freed by Getter when it completes
// ack-channel instead of single channel with ack message channel
// using Owicki-Gries ghostfields can be used to remove the "assume false;" statements
// Conjecture: it is ok to send debit credit(d, -x) over a channel c as long as
// a) d.mu << c.mu
// b) leaking positive or negative debit is not allowed
channel AckChannel(ch: C) where ch != null && credit(ch, -1); // ack
channel C(msg: int, n: Node, ackC: AckChannel) where
(msg == 0 || msg == 1) &&
(msg == 0 ==> acc(this.mu, 50) && acc(ackC.mu, 50)) &&
(msg == 1 ==> n != null && acc(n.next) && acc(n.mu) && credit(ackC, -1)); // cell
class Node {
var next: Node;
function length(): int
requires this.list;
{
unfolding this.list in 1 + (next == null ? 0 : next.length())
}
predicate list {
acc(next) && acc(mu) && (next != null ==> next.list)
}
}
class Program {
method Putter(e: C, x0: Node, ackC: AckChannel)
requires e!= null && acc(e.mu, 50) && e.mu == maxlock && acc(ackC.mu, 50) && e.mu << ackC.mu && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));
{
var x: Node := x0;
var t: Node;
while(x != null)
invariant (x != null ==> x.list) && acc(e.mu, 50) && acc(ackC.mu, 50) && e.mu << ackC.mu && credit(e, - 1);
{
unfold x.list;
t := x.next;
send e(1, x, ackC);
x := t;
var ack;
assume maxlock << ackC.mu; // Chalice should be able to figure this out itself?
var ctmp: C;
receive ctmp := ackC;
if(ctmp != e) { assume false; /* abort */ }
}
send e(0, null, ackC);
}
method Getter(f: C, ackC: AckChannel)
requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.mu && ackC != null && acc(ackC.mu, 50) && f.mu << ackC.mu;
{
var x: Node := null;
var msg := 1;
while(msg != 0)
invariant acc(f.mu, 50) && maxlock << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50) && acc(ackC.mu, 50));
{
var ackC2: AckChannel;
receive msg, x, ackC2 := f;
if(ackC2 != ackC) { assume false; /* abort */ }
if(msg == 0) {
}
if(msg == 1) {
free x;
send ackC(f);
}
}
free f; // close the channel
}
method Main(x: Node)
requires x.list;
{
var e := new C;
var ackC := new AckChannel above e;
fork Putter(e, x, ackC);
fork Getter(e, ackC);
}
}
|
