Commit 33247d9f authored by Simon Friis Vindum's avatar Simon Friis Vindum

Implement new approach to proof of original variant

parent 553737c5
......@@ -88,7 +88,7 @@ Definition MS_enqueue :=
(* c = InjL ... Tail is nil, we can try to insert now *)
(If
(CAS (Var 2 (* c *)) (Var 1 (* t *)) (Var 5 (* n *)))
(* Insertion succeeded, we are done *)
(* Insertion succeeded *)
(Seq
(* Update the tail pointer *)
(Store (Var 8 (* tail *)) (Var 5 (* n *)))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment