diff options
| author |  jansmans <unknown> | 2009-10-07 12:58:55 +0000 |
|---|---|---|
| committer | jansmans <unknown> | 2009-10-07 12:58:55 +0000 |
| commit | 11ea282f2404169e93c8c9de58ed684b2903910a (patch) | |
| tree | b302a0df10663fd1c9b5866b213f43adb7e036fb | |
| parent | f0df4f110687974508a4c96e4ebb58a9cd7270c8 (diff) | |
- verified a program inpsired by "Copyless Message Passing" in Chalice
(todo: we should really support sending debit over channel to allow sending with acknowledgements)
| -rw-r--r-- | Chalice/examples/CopyLessMessagePassing.chalice | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/Chalice/examples/CopyLessMessagePassing.chalice b/Chalice/examples/CopyLessMessagePassing.chalice new file mode 100644 index 00000000..1363bb2a --- /dev/null +++ b/Chalice/examples/CopyLessMessagePassing.chalice @@ -0,0 +1,71 @@ +// 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
+
+// todo: accept ack message before sending the next one (requires sending negative credit!)
+
+channel C(msg: int, n: Node) where n!= null && acc(n.next) && acc(n.mu) && (msg == 1 ==> credit(this, 1)) && (msg == 0 ==> acc(this.mu, 50));
+
+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) && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));
+ {
+ var x: Node := x0;
+ var t: Node;
+
+ while(x != null)
+ invariant (x != null ==> x.list) && (x!=null ==> acc(e.mu, 50)) && (x != null ==> credit(e, - 1));
+ {
+ unfold x.list;
+ t := x.next;
+ if(t != null) {
+ send e(1, x);
+ } else {
+ send e(0, x);
+ }
+ x := t;
+ }
+ }
+
+ 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 == 1) {
+ free x;
+ }
+ }
+ free f; // close the channel
+ }
+
+ method Main(x: Node)
+ requires x.list;
+ {
+ var e := new C;
+ fork Putter(e, x);
+ fork Getter(e);
+ }
+}
+
+
+
|