From 922a41c1f73ddcdb106c2d00ae00ad8c7c2b8698 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 28 Jul 2016 15:05:48 +0200
Subject: [PATCH] 'Fork' is atomic
---
heap_lang/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index da060db51..5d847b133 100644
--- 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
--
GitLab