Binary operations are atomic

78a89b31 · Dan Frumin · 671be1fc · 78a89b31
Commit 78a89b31 authored Oct 23, 2017 by Dan Frumin
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

theories/F_mu_ref_conc/lang.v theories/F_mu_ref_conc/lang.v +1 -0

No files found.
--- a/theories/F_mu_ref_conc/lang.v
+++ b/theories/F_mu_ref_conc/lang.v
@@ -419,6 +419,7 @@ Module lang.
    | Load e =>  is_Some (to_val e)
    | Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
    | CAS e0 e1 e2 => is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
+    | BinOp _ e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
    | Fork _ => True
    | _ => False
    end.