diff options
| author |  jansmans <unknown> | 2009-10-07 13:20:53 +0000 |
|---|---|---|
| committer | jansmans <unknown> | 2009-10-07 13:20:53 +0000 |
| commit | 0cb04ae067f2b44681516b2cb62fa1b64fc8bd71 (patch) | |
| tree | c06f46715142f82d42eb46333be415aa6c1139c0 | |
| parent | 11ea282f2404169e93c8c9de58ed684b2903910a (diff) | |
- extended to example to use acknowledgements (but uses sending debit)
| -rw-r--r-- | Chalice/examples/CopyLessMessagePassing-with-ack.chalice | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice new file mode 100644 index 00000000..1c21e8f4 --- /dev/null +++ b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice @@ -0,0 +1,81 @@ +// 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 works, but an assume is needed and negative credits are sent over channels!
+
+// Conjecture: it is ok to send debit for yourself over yourself if we check that neither positive nor negative credits are leaked.
+
+channel C(msg: int, n: Node) where
+ (msg == 0 ==> credit(this, -1)) && // ack
+ (msg == 1 ==> n != null && acc(n.next) && acc(n.mu) && credit(this, -1)) && // cell
+ (msg == 2 ==> acc(this.mu, 50)); // done
+
+
+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)
+ requires e!= null && acc(e.mu, 50) && e.mu == maxlock && (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) && credit(e, - 1);
+ {
+ unfold x.list;
+ t := x.next;
+ send e(1, x);
+ x := t;
+ var ack;
+ assume maxlock << e.mu;
+ receive ack, t := e;
+ if(ack != 2) { assume false; /* abort */ }
+ }
+ send e(2, null);
+ }
+
+ method Getter(f: C)
+ requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.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));
+ {
+ receive msg, x := f;
+ if(msg == 0) {
+ }
+ if(msg == 1) {
+ free x;
+ send f(2, null);
+ }
+ if(msg != 0 || msg != 1) { assume false; /* abort */ }
+ }
+ free f; // close the channel
+ }
+
+ method Main(x: Node)
+ requires x.list;
+ {
+ var e := new C;
+ fork Putter(e, x);
+ fork Getter(e);
+ }
+}
+
+
+
|