'Fork' is atomic

922a41c1 · Ralf Jung · 47d81be1 · 922a41c1
Commit 922a41c1 authored Jul 28, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

heap_lang/tactics.v heap_lang/tactics.v +1 -0

No files found.
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -179,6 +179,7 @@ Definition atomic (e : expr) :=
  | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
  | CAS e0 e1 e2 =>
     bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
+  | Fork _ => true
  (* Make "skip" atomic *)
  | App (Rec _ _ (Lit _)) (Lit _) => true
  | _ => false