- fixed a positioning bug in Parser.scala

- CopyLessMessagePassing-with-ack2.chalice verifies (i.e. separate channel for acknowledgements)

3 files changed, 92 insertions, 3 deletions

diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice
index 1c21e8f4..842e3d7d 100644
--- a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice
+++ b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice
@@ -4,7 +4,8 @@
 // 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.

+// Conjecture: it is ok to send debit for yourself over yourself.

+// Why: Suppose a channel that allows self-debt is involved in a deadlock. The either that channel is empty, which means there's no difference between the situation with or with self-debt. Or the channel is non-empty. This means that we can make progress by receiving the message stored in the channel! Does this make any sense?

 

 channel C(msg: int, n: Node) where 

   (msg == 0 ==> credit(this, -1)) && // ack

@@ -41,7 +42,7 @@ class Program {
       send e(1, x);

       x := t;

       var ack;

-      assume maxlock << e.mu;

+      assume maxlock << e.mu; // Chalice should be able to figure this out itself

       receive ack, t := e;

       if(ack != 2) { assume false; /* abort */ }

     }

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);

+  }  

+}

+

+

+

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 4667f0e7..f9d21f76 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -204,7 +204,7 @@ class Parser extends StandardTokenParsers {
         case FunctionApplication(obj, name, args) => Semi ^^^ Send(MemberAccess(obj,name), args)

         case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})

     | ("send" ~> atom into { e => e match {

-        case FunctionApplication(ImplicitThisExpr(), name, args) => Semi ^^^ Send(VariableExpr(name), args)

+        case fa@FunctionApplication(ImplicitThisExpr(), name, args) => Semi ^^^ {val va = VariableExpr(name); va.pos = fa.pos; Send(va, args)}

         case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})

     | "receive" ~> (identList <~ ":=" ?) ~ expression <~ Semi ^^ {

         case outs ~ e => Receive(e, ExtractList(outs)) }