split lclist grasshopper stuff

septract · Aug 4, 2016 · 8535461 · 8535461
1 parent 99e3763
commit 8535461
Show file tree

Hide file tree

Showing 2 changed files with 100 additions and 102 deletions.
diff --git a/grasshopper/lclist-module.spl b/grasshopper/lclist-module.spl
@@ -0,0 +1,99 @@
+// Node data-structure 
+
+struct Node {
+  var next: Node;
+  var lock: Bool; 
+  var val: Int; 
+}
+
+
+// List segment definitions
+
+predicate lseg(x: Node, y: Node) {
+  acc({ z: Node :: Btwn(next, x, z, y) && z != y }) &*& Reach(next, x, y)
+}
+
+predicate lseg_upperbound(ub: Int, FP: Set<Node>)
+  requires acc(FP)
+{
+  forall z: Node :: (z in FP && z.next != null) ==> z.val <= ub
+}
+
+predicate lseg_sentinel (head: Node, ub: Int, FP: Set<Node>) 
+  requires acc(FP) 
+{ 
+  exists z: Node :: 
+    z in FP && z.next == null && z.val == ub && z != head 
+} 
+
+predicate llseg(h: Node, y: Node, ub: Int) {
+  lseg(h, y) && 
+  (exists X: Set<Node> :: 
+    acc(X) &*& lseg_upperbound(ub, X) &*& lseg_sentinel(h,ub,X)) 
+}
+
+predicate nodeUnlocked(x: Node, y: Node) { 
+  x.next == y &*& x.lock == false
+} 
+
+predicate nodeLocked(x: Node, y: Node) { 
+  x.next == y &*& x.lock == true  
+} 
+
+
+// Calls to helper procedures
+
+procedure takeLock(x: Node)
+  requires acc(x); 
+  ensures acc(x) &*& nodeLocked(x,x.next); 
+{ 
+  while (x.lock == true) {} 
+  x.lock := true; 
+}  
+
+procedure releaseLock(x: Node)
+  requires acc(x) &*& nodeLocked(x,x.next); 
+  ensures acc(x) &*& nodeUnlocked(x,x.next); 
+{ 
+  x.lock := false; 
+}  
+
+predicate endNode(x: Node, ub: Int) { 
+  acc(x) &*& x.next == null &*& x.val == ub
+} 
+
+procedure disposeNode(x: Node) 
+  requires acc(x); 
+  ensures emp; 
+{ 
+  free(x); 
+} 
+
+
+// Equivalents to Starling predicates. 
+
+predicate isListG (head: Node, ub: Int, v: Int) { 
+  llseg(head, null, ub) &*& head != null &*& v < ub 
+} 
+
+predicate has1LockG(head: Node, a: Node, b: Node) 
+{ 
+  exists X: Set<Node> :: acc(X) &*& a in X &*& nodeLocked(a, b)
+} 
+
+predicate has2LockG(head: Node, a: Node, b: Node) { 
+  exists X: Set<Node>, c: Node :: 
+    acc(X) &*& a in X &*& b in X &*& nodeLocked(a, b) &*& nodeLocked(b,c)
+} 
+
+predicate dangleNodeG(x: Node) 
+{ 
+  acc(x)
+} 
+
+predicate isValG(head: Node, n: Node, v: Int) 
+  requires acc(n) 
+{ 
+  exists X: Set<Node> :: acc(X) &*& n.val == v
+} 
+
diff --git a/grasshopper/lclist-seq.spl b/grasshopper/lclist-seq.spl
@@ -1,108 +1,7 @@
 // A Starling-style proof of the lclist delete operation 
 // Sequential only, but the predicates should be similar to the concurrent case. 
 
-// This proof is derived in part from the GRASShopper examples in 
-// https://github.com/wies/grasshopper/tree/master/tests/spl
-
-// Node data-structure 
-
-struct Node {
-  var next: Node;
-  var lock: Bool; 
-  var val: Int; 
-}
-
-
-// List segment definitions
-
-predicate lseg(x: Node, y: Node) {
-  acc({ z: Node :: Btwn(next, x, z, y) && z != y }) &*& Reach(next, x, y)
-}
-
-predicate lseg_upperbound(ub: Int, FP: Set<Node>)
-  requires acc(FP)
-{
-  forall z: Node :: (z in FP && z.next != null) ==> z.val <= ub
-}
-
-predicate lseg_sentinel (head: Node, ub: Int, FP: Set<Node>) 
-  requires acc(FP) 
-{ 
-  exists z: Node :: 
-    z in FP && z.next == null && z.val == ub && z != head 
-} 
-
-predicate llseg(h: Node, y: Node, ub: Int) {
-  lseg(h, y) && 
-  (exists X: Set<Node> :: 
-    acc(X) &*& lseg_upperbound(ub, X) &*& lseg_sentinel(h,ub,X)) 
-}
-
-predicate nodeUnlocked(x: Node, y: Node) { 
-  x.next == y &*& x.lock == false
-} 
-
-predicate nodeLocked(x: Node, y: Node) { 
-  x.next == y &*& x.lock == true  
-} 
-
-
-// Calls to helper procedures
-
-procedure takeLock(x: Node)
-  requires acc(x); 
-  ensures acc(x) &*& nodeLocked(x,x.next); 
-{ 
-  while (x.lock == true) {} 
-  x.lock := true; 
-}  
-
-procedure releaseLock(x: Node)
-  requires acc(x) &*& nodeLocked(x,x.next); 
-  ensures acc(x) &*& nodeUnlocked(x,x.next); 
-{ 
-  x.lock := false; 
-}  
-
-predicate endNode(x: Node, ub: Int) { 
-  acc(x) &*& x.next == null &*& x.val == ub
-} 
-
-procedure disposeNode(x: Node) 
-  requires acc(x); 
-  ensures emp; 
-{ 
-  free(x); 
-} 
-
-
-// Equivalents to Starling predicates. 
-
-predicate isListG (head: Node, ub: Int, v: Int) { 
-  llseg(head, null, ub) &*& head != null &*& v < ub 
-} 
-
-predicate has1LockG(head: Node, a: Node, b: Node) 
-{ 
-  exists X: Set<Node> :: acc(X) &*& a in X &*& nodeLocked(a, b)
-} 
-
-predicate has2LockG(head: Node, a: Node, b: Node) { 
-  exists X: Set<Node>, c: Node :: 
-    acc(X) &*& a in X &*& b in X &*& nodeLocked(a, b) &*& nodeLocked(b,c)
-} 
-
-predicate dangleNodeG(x: Node) 
-{ 
-  acc(x)
-} 
-
-predicate isValG(head: Node, n: Node, v: Int) 
-  requires acc(n) 
-{ 
-  exists X: Set<Node> :: acc(X) &*& n.val == v
-} 
-
+include "./lclist-module.spl"; 
 
 // Proof of deleteVal in a pseudo-Starling style