1 files changed, 88 insertions, 0 deletions
diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice b/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice
new file mode 100644
index 00000000..51fd469c
--- /dev/null
+++ b/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice
@@ -0,0 +1,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);
+  }  
+}
+
+
+