From 0523bbf315ab040f3650c0ff3d804c216e19f063 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Dec 2017 18:27:09 +0100
Subject: [PATCH] add dedicated type for atomicity

---
 theories/heap_lang/tactics.v           |  2 +-
 theories/program_logic/ectx_language.v |  8 +++---
 theories/program_logic/hoare.v         |  4 +--
 theories/program_logic/language.v      | 39 +++++++++-----------------
 theories/program_logic/weakestpre.v    | 24 ++++++++++++----
 theories/tests/ipm_paper.v             |  2 +-
 6 files changed, 41 insertions(+), 38 deletions(-)

diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index c4268b60c..fc056d5ba 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -189,7 +189,7 @@ Definition is_atomic (e : expr) :=
   end.
 Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
 Proof.
-  enough (is_atomic e → Atomic maybe_stuck (to_expr e)).
+  enough (is_atomic e → Atomic strongly_atomic (to_expr e)).
   { destruct s; auto using strongly_atomic_atomic. }
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 1e2054682..275c98cf4 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -129,10 +129,10 @@ Section ectx_language.
 
   Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
 
-  Definition HeadAtomic (s : stuckness) (e : expr Λ) : Prop :=
+  Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
     ∀ σ e' σ' efs,
       head_step e σ e' σ' efs →
-      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
+      if a is weakly_atomic then irreducible e' σ' else is_Some (to_val e').
 
   (* Some lemmas about this language *)
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
@@ -173,8 +173,8 @@ Section ectx_language.
     apply (Hirr empty_ectx). by rewrite fill_empty.
   Qed.
 
-  Lemma ectx_language_atomic s e :
-    HeadAtomic s e → sub_redexes_are_values e → Atomic s e.
+  Lemma ectx_language_atomic a e :
+    head_atomic a e → sub_redexes_are_values e → Atomic a e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 0f2136dee..aa371d768 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -58,7 +58,7 @@ Lemma ht_mono s E P P' Φ Φ' e :
   (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
 Lemma ht_stuck_mono s1 s2 E P Φ e :
-  (s1 ≤ s2)%stuckness → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
+  stuckness_le s1 s2 → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed.
 Global Instance ht_mono' s E :
   Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
@@ -79,7 +79,7 @@ Proof.
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic s e} :
+Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity s) e} :
   (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ s; E1 {{ Φ }}.
 Proof.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 7b3cd414f..28d47f037 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -53,19 +53,7 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
 Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
-Variant stuckness := not_stuck | maybe_stuck.
-Definition stuckness_le (s1 s2 : stuckness) : bool :=
-  match s1, s2 with
-  | maybe_stuck, not_stuck => false
-  | _, _ => true
-  end.
-Instance: @PreOrder stuckness stuckness_le.
-Proof.
-  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
-Qed.
-Bind Scope stuckness_scope with stuckness.
-Delimit Scope stuckness_scope with stuckness.
-Infix "≤" := stuckness_le : stuckness_scope.
+Inductive atomicity := strongly_atomic | weakly_atomic.
 
 Section language.
   Context {Λ : language}.
@@ -86,21 +74,21 @@ Section language.
   Definition stuck (e : expr Λ) (σ : state Λ) :=
     to_val e = None ∧ irreducible e σ.
 
-  (* [Atomic not_stuck]: This (weak) form of atomicity is enough to open invariants when WP ensures
-     safety, i.e., programs never can get stuck.  We have an example in
-     lambdaRust of an expression that is atomic in this sense, but not in the
-     stronger sense defined below, and we have to be able to open invariants
-     around that expression.  See `CasStuckS` in
+  (* [Atomic weakly_atomic]: This (weak) form of atomicity is enough to open
+     invariants when WP ensures safety, i.e., programs never can get stuck.  We
+     have an example in lambdaRust of an expression that is atomic in this
+     sense, but not in the stronger sense defined below, and we have to be able
+     to open invariants around that expression.  See `CasStuckS` in
      [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
 
-     [Atomic maybe_stuck]: To open invariants with a WP that does not ensure safety, we need a
-     stronger form of atomicity.  With the above definition, in case `e` reduces
-     to a stuck non-value, there is no proof that the invariants have been
-     established again. *)
-  Class Atomic (s : stuckness) (e : expr Λ) : Prop :=
+     [Atomic strongly_atomic]: To open invariants with a WP that does not ensure
+     safety, we need a stronger form of atomicity.  With the above definition,
+     in case `e` reduces to a stuck non-value, there is no proof that the
+     invariants have been established again. *)
+  Class Atomic (a : atomicity) (e : expr Λ) : Prop :=
     atomic σ e' σ' efs :
       prim_step e σ e' σ' efs →
-      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
+      if a is weakly_atomic then irreducible e' σ' else is_Some (to_val e').
 
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
@@ -121,7 +109,8 @@ 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 : Atomic maybe_stuck e → Atomic not_stuck e.
+  Lemma strongly_atomic_atomic e :
+    Atomic strongly_atomic e → Atomic weakly_atomic e.
   Proof. unfold Atomic. eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 68f006ce4..1642987af 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -11,6 +11,17 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
+Inductive stuckness := not_stuck | maybe_stuck.
+Definition stuckness_le (s1 s2 : stuckness) : bool :=
+  match s1, s2 with
+  | maybe_stuck, not_stuck => false
+  | _, _ => true
+  end.
+Instance: PreOrder stuckness_le.
+Proof.
+  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
+Qed.
+
 Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
@@ -233,7 +244,10 @@ Qed.
 Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
 Proof. iIntros "H". iApply (wp_strong_mono s E); try iFrame; auto. Qed.
 
-Lemma wp_atomic s E1 E2 e Φ `{Hatomic : !Atomic s e} :
+Definition stuckness_to_atomicity s :=
+  if s is maybe_stuck then strongly_atomic else weakly_atomic.
+
+Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
 Proof.
   iIntros "H". rewrite !wp_unfold /wp_pre.
@@ -245,8 +259,8 @@ Proof.
     rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
     + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
-      by edestruct (Hatomic _ _ _ _ Hstep).
-  - destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
+      by edestruct (atomic _ _ _ _ Hstep).
+  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
     iMod ("H" with "[#]") as "($ & H & $)"; first done.
     iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
 Qed.
@@ -300,7 +314,7 @@ Proof.
   iIntros "{$H}" (v) "?". by iApply HΦ.
 Qed.
 Lemma wp_stuck_mono s1 s2 E e Φ :
-  (s1 ≤ s2)%stuckness → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
+  stuckness_le s1 s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
 Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed.
 Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
 Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed.
@@ -379,7 +393,7 @@ Section proofmode_classes.
 
   (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
-    Atomic s e →
+    Atomic (stuckness_to_atomicity s) e →
     ElimModal (|={E1,E2}=> P) P
             (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index b6189d309..c9d41b148 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
 Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
-  nclose N ⊆ E → Atomic not_stuck e →
+  nclose N ⊆ E → Atomic weakly_atomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".
-- 
GitLab