From 42dfffc981c1d606c64186b36d13824d2840e969 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 29 Oct 2017 12:10:04 +0100
Subject: [PATCH] add a strong form of atomicity, for weak forms of weakest-pre

---
 theories/program_logic/language.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 88c82f8eb..ab23fe814 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -52,9 +52,15 @@ Section language.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬prim_step e σ e' σ' efs.
 
+  (* This (weak) form of atomicity is enough to open invariants when WP is safe,
+     i.e., programs never can get stuck. *)
   Definition atomic (e : expr Λ) : Prop :=
     ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'.
 
+  (* To open invariants with unsafe WP, we need a stronger form of atomicity. *)
+  Definition strongly_atomic (e : expr Λ) : Prop :=
+    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → is_Some (to_val e').
+
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
@@ -74,6 +80,10 @@ Section language.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
+  Lemma strongly_atomic_atomic e :
+    strongly_atomic e → atomic e.
+  Proof. unfold strongly_atomic, atomic. eauto using val_irreducible. Qed.
+
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
   Proof.
-- 
GitLab