From 8be808243e6c93c37440e97553ec869826d9e585 Mon Sep 17 00:00:00 2001 From: Matt Windsor Date: Thu, 16 Feb 2017 13:06:05 +0000 Subject: [PATCH] Add some more atomic-branch examples. --- Examples/Fail/spinLockBrokenCAS.cvf | 40 +++++++++++++++ Examples/PassGH/spinLock.cvf | 6 ++- Examples/PassGH/spinLockAtomicBranch.cvf | 62 ++++++++++++++++++++++++ Grasshopper.fs | 62 +++++++++++++++--------- testresults | 2 + 5 files changed, 148 insertions(+), 24 deletions(-) create mode 100644 Examples/Fail/spinLockBrokenCAS.cvf create mode 100644 Examples/PassGH/spinLockAtomicBranch.cvf diff --git a/Examples/Fail/spinLockBrokenCAS.cvf b/Examples/Fail/spinLockBrokenCAS.cvf new file mode 100644 index 0000000..5b0082b --- /dev/null +++ b/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 diff --git a/Examples/PassGH/spinLock.cvf b/Examples/PassGH/spinLock.cvf index 32f5d3e..26e5fe3 100644 --- a/Examples/PassGH/spinLock.cvf +++ b/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) |} diff --git a/Examples/PassGH/spinLockAtomicBranch.cvf b/Examples/PassGH/spinLockAtomicBranch.cvf new file mode 100644 index 0000000..26e5fe3 --- /dev/null +++ b/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}; + +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; diff --git a/Grasshopper.fs b/Grasshopper.fs index 97e85af..07ad958 100644 --- a/Grasshopper.fs +++ b/Grasshopper.fs @@ -55,6 +55,11 @@ module Types = Assign of lvalue : ShadowVar * prim : GrassPrim | /// A pure assumption. PureAssume of assumption : BoolExpr> + | /// A branch. + Branch of + cond : BoolExpr> + * trueBranch : GrassCommand list + * falseBranch : GrassCommand list /// A Grasshopper formula. type Formula = @@ -292,17 +297,26 @@ module Pretty = /// /// A representing . /// - 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) /// /// A Chessie result, containing a list of Grasshopper commands. /// -let grassMicrocode (routine : Microcode, Sym> list) +let rec grassMicrocode (routine : Microcode, Sym> list) : Result = 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, Sym> 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)) diff --git a/testresults b/testresults index 0cb1c22..8573810 100644 --- a/testresults +++ b/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: