update coh axiom

hernanponcedeleon · Sep 27, 2024 · bd48d29 · bd48d29
1 parent 2ec066e
commit bd48d29
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/cat/c11.cat b/cat/c11.cat
@@ -59,7 +59,8 @@ acyclic hb as Hb
 (* coherent_memory_use *)
 let hbl = hb & loc
 
-irreflexive ((rf^-1)? ; mo ; rf? ; hb) as Coh
+// To support reads from uninitialized memory
+irreflexive ((fr | mo); rf?; hb) as Coh
 
 (* visible_side_effect_set *)
 let vis = ([W] ; hbl ; [R]) & ~(hbl; [W]; hbl)