From f6c342c3a0237c31e77e8548972de825a2eac19c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 May 2017 16:35:36 +0200
Subject: [PATCH] Do not allow na reads and CAS to race on the same location.

We do this by requiring Rst 0 for failed CASes. This avoid reduces the
need for the stuck_term hack.
---
 theories/lang/lang.v    | 29 ++-------------
 theories/lang/lifting.v | 18 +++++-----
 theories/lang/races.v   | 78 ++++++-----------------------------------
 theories/lang/tactics.v |  3 +-
 4 files changed, 22 insertions(+), 106 deletions(-)

diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 1dbd8ee6..ab255f38 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -236,8 +236,6 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
 | BinOpOffset l z :
     bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ shift_loc l z).
 
-Definition stuck_term := App (Lit $ LitInt 0) [].
-
 Inductive head_step : expr → state → expr → state → list expr → Prop :=
 | BinOpS op l1 l2 l' σ :
     bin_op_eval σ op l1 l2 l' →
@@ -278,9 +276,9 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
     head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
               (Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
               []
-| CasFailS l n e1 lit1 e2 lit2 litl σ :
+| CasFailS l e1 lit1 e2 lit2 litl σ :
     to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
-    σ !! l = Some (RSt n, LitV litl) →
+    σ !! l = Some (RSt 0, LitV litl) →
     lit_neq σ lit1 litl →
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ lit_of_bool false) σ  []
 | CasSucS l e1 lit1 e2 lit2 litl σ :
@@ -290,13 +288,6 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ
               (Lit $ lit_of_bool true) (<[l:=(RSt 0, LitV lit2)]>σ)
               []
-| CasStuckS l n e1 lit1 e2 lit2 litl σ :
-    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
-    σ !! l = Some (RSt n, LitV litl) → 0 < n →
-    lit_eq σ lit1 litl →
-    head_step (CAS (Lit $ LitLoc l) e1 e2) σ
-              stuck_term σ
-              []
 | AllocS n l init σ :
     0 < n →
     (∀ m, σ !! shift_loc l m = None) →
@@ -528,11 +519,6 @@ Proof.
   intros Heq. inversion 1; econstructor; eauto using lit_eq_state, lit_neq_state.
 Qed.
 
-(* Misc *)
-Lemma stuck_not_head_step σ e' σ' ef :
-  ¬head_step stuck_term σ e' σ' ef.
-Proof. inversion 1. Qed.
-
 (** Equality and other typeclass stuff *)
 Instance base_lit_dec_eq : EqDecision base_lit.
 Proof. solve_decision. Defined.
@@ -607,19 +593,8 @@ Program Instance lrust_ectxi_lang : EctxiLanguage expr val ectx_item state :=
      ectxi_language.head_step := head_step |}.
 Solve Obligations with eauto using to_of_val, of_to_val,
   val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
-
 Canonical Structure lrust_lang := ectx_lang expr.
 
-(* Lemmas about the language. *)
-Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
-Proof.
-  apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
-  apply prim_head_irreducible; unfold stuck_term.
-  - inversion 1.
-  - apply ectxi_language_sub_values.
-    intros [] ??; simplify_eq/=; eauto; discriminate_list.
-Qed.
-
 (* Define some derived forms *)
 Notation Lam xl e := (Rec BAnon xl e).
 Notation Let x e1 e2 := (App (Lam [x] e2) [e1]).
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index bea9a136..1b1fee34 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -130,15 +130,15 @@ Proof.
   iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
+Lemma wp_cas_int_fail E l z1 e2 lit2 zl :
   to_val e2 = Some (LitV lit2) → z1 ≠ zl →
-  {{{ ▷ l ↦{q} LitV (LitInt zl) }}}
+  {{{ ▷ l ↦ LitV (LitInt zl) }}}
     CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
-  {{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
+  {{{ RET LitV $ LitInt 0; l ↦ LitV (LitInt zl) }}}.
 Proof.
   iIntros (<-%of_to_val ? Φ) ">Hv HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+  iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -173,16 +173,16 @@ Lemma wp_cas_loc_suc E l l1 e2 lit2 :
   {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
 Proof. intros ?. by apply wp_cas_suc. Qed.
 
-Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
+Lemma wp_cas_loc_fail E l q' q1 l1 v1' e2 lit2 l' vl' :
   to_val e2 = Some (LitV lit2) → l1 ≠ l' →
-  {{{ ▷ l ↦{q} LitV (LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
+  {{{ ▷ l ↦ LitV (LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
     CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
   {{{ RET LitV (LitInt 0);
-      l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
+      l ↦ LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
 Proof.
   iIntros (<-%of_to_val ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
+  iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hl") as %?.
   iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
   iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
   iModIntro; iSplit; first by eauto.
@@ -202,7 +202,7 @@ Proof.
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
   iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
-  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   - inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
     iApply "HΦ"; simpl; auto.
   - iMod (heap_write with "Hσ Hv") as "[$ Hv]".
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 3321b135..d7e27444 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -79,12 +79,8 @@ Proof.
   - apply ectxi_language_sub_values. intros [] ? ->; inversion Hhead; eauto.
 Qed.
 
-Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
-  ∀ e' σ' efs, ectx_language.head_step e σ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
-
 Lemma next_access_head_reducible_state e σ a l :
   next_access_head e σ a l → head_reducible e σ →
-  head_reduce_not_to_stuck e σ →
   match a with
   | (ReadAcc, ScOrd | Na1Ord) => ∃ v n, σ !! l = Some (RSt n, v)
   | (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
@@ -93,12 +89,8 @@ Lemma next_access_head_reducible_state e σ a l :
   | (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
   end.
 Proof.
-  intros Ha (e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
-  - destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
-    eapply CasStuckS; done.
-  - exfalso. eapply Hrednonstuck; last done.
-    eapply CasStuckS; done.
-  - match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
+  intros Ha (e'&σ'&ef&Hstep). destruct Ha; inv_head_step; eauto.
+  match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
 Qed.
 
 Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 a l :
@@ -155,38 +147,6 @@ Proof.
   eapply (@is_Some_None (lock_state * val)). rewrite -FREE'. naive_solver.
 Qed.
 
-Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef :
-  (∀ el' σ' e', rtc step (el, σ) (el', σ') →
-                e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → head_step e σ e' σ' ef → head_reduce_not_to_stuck e' σ'.
-Proof.
-  intros Hsafe Hi Hstep e1 σ1 ? Hstep1 Hstuck.
-  cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?). by eapply stuck_irreducible. }
-  destruct (elem_of_list_split _ _ Hi) as (?&?&->).
-  eapply Hsafe; last by (apply: fill_not_val; subst).
-  - eapply rtc_l, rtc_l, rtc_refl.
-    + econstructor. done. done. econstructor; done.
-    + econstructor. done. done. econstructor; done.
-  - subst. set_solver+.
-Qed.
-
-(* TODO: Unify this and the above. *)
-Lemma safe_not_reduce_to_stuck el σ K e :
-  (∀ el' σ' e', rtc step (el, σ) (el', σ') →
-                e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → head_reduce_not_to_stuck e σ.
-Proof.
-  intros Hsafe Hi e1 σ1 ? Hstep1 Hstuck.
-  cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?). by eapply stuck_irreducible. }
-  destruct (elem_of_list_split _ _ Hi) as (?&?&->).
-  eapply Hsafe; last by (apply: fill_not_val; subst).
-  - eapply rtc_l, rtc_refl.
-    + econstructor. done. done. econstructor; done.
-  - subst. set_solver+.
-Qed.
-
 Theorem safe_nonracing el σ :
   (∀ el' σ' e', rtc step (el, σ) (el', σ') →
                 e' ∈ el' → to_val e' = None → reducible e' σ') →
@@ -199,10 +159,8 @@ Proof.
   assert (Hrede1:head_reducible e1 σ).
   { eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse1:head_reduce_not_to_stuck e1 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
-  assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
-  destruct Hrede1 as (e1'&σ1'&ef1&Hstep1). clear Hnse1.
+  assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1).
+  destruct Hrede1 as (e1'&σ1'&ef1&Hstep1).
   assert (Ha1' : a1.2 = Na1Ord → next_access_head e1' σ1' (a1.1, Na2Ord) l).
   { intros. eapply next_access_head_Na1Ord_step, Hstep1.
     by destruct a1; simpl in *; subst. }
@@ -216,16 +174,11 @@ Proof.
     eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
            fill_not_val=>//.
     by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
-  assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
-
   assert (to_val e2 = None). by destruct Ha2.
   assert (Hrede2:head_reducible e2 σ).
   { eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse2:head_reduce_not_to_stuck e2 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
-  assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
+  assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2).
   destruct Hrede2 as (e2'&σ2'&ef2&Hstep2).
   assert (Ha2' : a2.2 = Na1Ord → next_access_head e2' σ2' (a2.1, Na2Ord) l).
   { intros. eapply next_access_head_Na1Ord_step, Hstep2.
@@ -240,23 +193,16 @@ Proof.
     eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
            fill_not_val=>//.
     by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
-  assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K2); first done; last done. set_solver+. }
-
   assert (Ha1'2 : a1.2 = Na1Ord → next_access_head e2 σ1' a2 l).
   { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
     by rewrite <-HNa, <-surjective_pairing. }
   assert (Hrede1_2: head_reducible e2 σ1').
   { intros. eapply (next_access_head_reductible_ctx e2 σ1' σ  a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
-  { eapply safe_not_reduce_to_stuck with (K:=K2).
-    - intros. eapply Hsafe. etrans; last done. done. done. done.
-    - set_solver+. }
   assert (Hσe1'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord)).
   assert (Hσe1'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2).
 
   assert (Ha2'1 : a2.2 = Na1Ord → next_access_head e1 σ2' a1 l).
   { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
@@ -264,14 +210,10 @@ Proof.
   assert (Hrede2_1: head_reducible e1 σ2').
   { intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
-  { eapply safe_not_reduce_to_stuck with (K:=K1).
-    - intros. eapply Hsafe. etrans; last done. done. done. done.
-    - set_solver+. }
   assert (Hσe2'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1).
   assert (Hσe2'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord)).
 
   assert (a1.1 = FreeAcc → False).
   { destruct a1 as [[]?]; inversion 1.
@@ -288,7 +230,7 @@ Proof.
     end;
     try congruence.
 
-  clear e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1. destruct Hrede1_2 as (e2'&σ'&ef&?).
+  clear e2' Hstep2 σ2' Hrtc_step2 Hrede2_1. destruct Hrede1_2 as (e2'&σ'&ef&?).
   inv_head_step.
   match goal with
   | H : <[l:=_]> σ !! l = _ |- _ => by rewrite lookup_insert in H
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 58955702..92917a7e 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -155,8 +155,7 @@ Proof.
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef.
     destruct e; simpl; try done; repeat (case_match; try done);
-    inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
-    rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
+    inversion 1; apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto.
   - apply ectxi_language_sub_values=> /= Ki e' Hfill.
     revert He. destruct e; simpl; try done; repeat (case_match; try done);
     rewrite ?bool_decide_spec;
-- 
GitLab