Add some more atomic-branch examples.

Examples/Fail/spinLockBrokenCAS.cvf

@@ -0,0 +1,40 @@
+/*
+ * Herlihy/Shavit-style compare and swap lock,
+ * with an intentionally broken compare and swap.
+ */
+
+shared bool lock;  // True iff the lock is taken.
+thread bool test;  // Used when trying to take the lock.
+
+/*
+ * Locks the CAS lock.
+ */
+method lock() {
+  {| emp |}
+    do {
+      {| emp |}
+        test = false;
+      {| if test == false then emp else False() |}
+        <| if (lock == test) { lock = true; } /* test = lock; */ |>
+      {| if test == false then holdLock() else emp |}
+    } while (test == true);
+  {| holdLock() |}
+}
+
+/*
+ * Unlocks the CAS lock.
+ */
+method unlock() {
+  {| holdLock() |}
+    <| lock = false; |>
+  {| emp |}
+}
+
+
+// False is a hack to implement local variable reasoning.
+view False();
+constraint False() -> false;
+
+view holdLock();
+constraint holdLock() -> lock == true;  // Identity of lock.
+constraint holdLock() * holdLock() -> false;  // Mutual exclusion

Examples/PassGH/spinLock.cvf

@@ -25,7 +25,11 @@ method lock(Lock x) {
       {| isLock(x) |}
         test = false;
       {| if test == false then isLock(x) else False() |}
-        <| test = %{ CAS_to_true([|x|]) }; |>
+        <| test = %{ [|x|].lock };
+           if (%{ [|x|].lock } == false) {
+               %{ [|x|].lock := true };
+           } |>
+        test = !test;
       {| if test == false then isLock(x) else holdLock(x) |}
     } while (test == false);
   {| holdLock(x) |}

Examples/PassGH/spinLockAtomicBranch.cvf

@@ -0,0 +1,62 @@
+// Allocatable version of Examples/Pass/spinLock.cvf.
+
+typedef int Lock;
+
+pragma grasshopper_include {./grasshopper/spinlock-module.spl};
+pragma grasshopper_footprint {LockFoot};
+pragma grasshopper_footprint_sort {Set<Lock>};
+
+thread Lock x, ret;
+thread bool test;  // Used when trying to take the lock.
+
+view newLock(Lock x), holdLock(Lock x), isLock(Lock x);
+
+method newLock() {
+  {| emp |}
+    <| ret = %{new Lock}; |>
+  {| newLock(ret) |}
+    <| %{[|ret|].lock := false}; |>
+  {| isLock(ret) |}
+}
+
+method lock(Lock x) {
+  {| isLock(x) |}
+    do {
+      {| isLock(x) |}
+        test = false;
+      {| if test == false then isLock(x) else False() |}
+        <| test = %{ [|x|].lock };
+           if (%{ [|x|].lock } == false) {
+               %{ [|x|].lock := true };
+           } |>
+        test = !test;
+      {| if test == false then isLock(x) else holdLock(x) |}
+    } while (test == false);
+  {| holdLock(x) |}
+}
+
+method unlock(Lock x) {
+  {| holdLock(x) |}
+    <| %{[|x|].lock := false}; |>
+  {| isLock(x) |}
+}
+
+method split(Lock x) {
+  {| isLock(x) |}
+    ;
+  {| isLock(x) * isLock(x) |}
+}
+
+// False is a hack to implement local variable reasoning.
+view False();
+constraint False() -> false;
+
+constraint holdLock(x)  ->  %{ [|x|] in LockFoot && [|x|].lock };
+constraint isLock(x)    ->  %{ [|x|] in LockFoot };
+constraint newLock(x)   ->  %{ [|x|] in LockFoot };
+
+constraint isLock(x)   * newLock(y)   ->  x != y;
+constraint holdLock(x) * newLock(y)   ->  x != y;
+constraint newLock(x)  * newLock(y)   ->  x != y;
+
+constraint holdLock(x) * holdLock(y)  ->  x != y;

Grasshopper.fs

@@ -55,6 +55,11 @@ module Types =
           Assign of lvalue : ShadowVar * prim : GrassPrim
         | /// <summary>A pure assumption.</summary>
           PureAssume of assumption : BoolExpr<Sym<GrassVar>>
+        | /// <summary>A branch.</summary>
+          Branch of
+            cond : BoolExpr<Sym<GrassVar>>
+            * trueBranch : GrassCommand list
+            * falseBranch : GrassCommand list
 
     /// <summary>A Grasshopper formula.</summary>
     type Formula =
@@ -292,17 +297,26 @@ module Pretty =
     /// <returns>
     ///     A <see cref="Doc"/> representing <paramref name="cmd"/>.
     /// </returns>
-    let printCommand (cmd : GrassCommand) : Doc =
-        let c =
-            match cmd with
-            | VarDecl var -> String "var" <+> printTypedGrass printShadowVar var
-            | NoAssign prim -> printPrim prim
-            | Assign (lvalue, prim) ->
-                printShadowVar lvalue <+> String ":=" <+> printPrim prim
-            | PureAssume assumption ->
-                String "pure assume"
-                    <+> printBoolExprG (printSymGrass printGrassVar) assumption
-        withSemi c
+    let rec printCommand (cmd : GrassCommand) : Doc =
+        let printBlock c = 
+            braced (ivsep (List.map (printCommand >> Indent) c))
+
+        match cmd with
+        | VarDecl var ->
+            withSemi (String "var" <+> printTypedGrass printShadowVar var)
+        | NoAssign prim ->
+            withSemi (printPrim prim)
+        | Assign (lvalue, prim) ->
+            withSemi (printShadowVar lvalue <+> String ":=" <+> printPrim prim)
+        | PureAssume assumption ->
+            withSemi
+                (String "pure assume"
+                    <+> printBoolExprG (printSymGrass printGrassVar) assumption)
+        | Branch (cond = c; trueBranch = t; falseBranch = f) ->
+            String "if"
+            <+> parened (printBoolExprG (printSymGrass printGrassVar) c)
+            <+> printBlock t
+            <+> (if f.IsEmpty then Nop else (String "else" <+> printBlock f))
 
     /// Print a single Grasshopper query.
     let printGrassTerm (name : string) (term : GrassTerm) : Doc =
@@ -404,18 +418,25 @@ let findTermVars (term : Backends.Z3.Types.ZTerm)
 /// <returns>
 ///     A Chessie result, containing a list of Grasshopper commands.
 /// </returns>
-let grassMicrocode (routine : Microcode<CTyped<MarkedVar>, Sym<MarkedVar>> list)
+let rec grassMicrocode (routine : Microcode<CTyped<MarkedVar>, Sym<MarkedVar>> list)
   : Result<GrassCommand list, Error> =
     let translateAssign (x, y) =
         maybe BTrue (mkEq (mkVarExp (mapCTyped Reg x))) y
 
+    let grassBool x =
+        mapMessages Traversal
+            (liftWithoutContext
+                (Starling >> ok)
+                (tliftOverSym >> tliftOverCTyped >> tliftToExprDest >> tliftToBoolSrc)
+                (normalBool x))
+
     let grassMicrocodeInstruction ent =
         match ent with
-        | Branch _ ->
-            fail
-                (CommandNotImplemented
-                    (cmd = ent,
-                     why = "Cannot encode commands with inner conditionals."))
+        | Microcode.Branch (c, t, f) ->
+            lift3 (fun c' t' f' -> [ Branch (c', t', f') ])
+                (grassBool c)
+                (grassMicrocode t)
+                (grassMicrocode f)
         | Symbol cmd ->
             // These translate directly into Grasshopper primitive commands.
             ok [ NoAssign cmd ]
@@ -463,12 +484,7 @@ let grassMicrocode (routine : Microcode<CTyped<MarkedVar>, Sym<MarkedVar>> list)
                      why = "Assignments cannot mix symbols and pure expressions."))
         | Assume x ->
             // Pure assumption.
-            let grassifyR =
-                liftWithoutContext
-                    (Starling >> ok)
-                    (tliftOverSym >> tliftOverCTyped >> tliftToExprDest >> tliftToBoolSrc)
-                    (normalBool x)
-            lift (fun x -> [ PureAssume x ]) (mapMessages Traversal grassifyR)
+            lift (fun x -> [ PureAssume x ]) (grassBool x)
 
     lift List.concat (collect (List.map grassMicrocodeInstruction routine))
 

testresults

@@ -2,6 +2,7 @@
 ./Examples/Fail/badInc2.cvf: badInc_C000_000
 ./Examples/Fail/petersonArrayBadTurns.cvf: lock_C001_005
 ./Examples/Fail/petersonBadTurns.cvf: lockA_C001_019 lockB_C001_018
+./Examples/Fail/spinLockBrokenCAS.cvf: lock_C001__lock_C003_002
 ./Examples/Fail/ticketLockBad.cvf: unlock_C000_002 unlock_C000_003
 ./Examples/Fail/ticketLockBad2.cvf: lock_C000_000 lock_C000_002 unlock_C000_000
 ./Examples/Fail/ticketLockFlippedLoop.cvf: lock_C002_001 lock_C002_004 lock_C003_002 lock_C003_003 lock_C003_005
@@ -30,4 +31,5 @@
 ./Examples/PassGH/clhLock.cvf:
 ./Examples/PassGH/lclist.cvf:
 ./Examples/PassGH/spinLock.cvf:
+./Examples/PassGH/spinLockAtomicBranch.cvf:
 ./Examples/PassGH/ticketLock.cvf: