Incorporate the `Xchg` operation

theories/logic/compatibility.v

@@ -93,6 +93,25 @@ Section compatibility.
     value_case.
   Qed.
 
+  Lemma refines_xchg e1 e2 e1' e2' A :
+    (REL e1 << e1' : ref A) -∗
+    (REL e2 << e2' : A) -∗
+    REL Xchg e1 e2 << Xchg e1' e2' : A.
+  Proof.
+    iIntros "IH1 IH2".
+    rel_bind_ap e2 e2' "IH2" w w' "IH2".
+    rel_bind_ap e1 e1' "IH1" v v' "IH1".
+    iDestruct "IH1" as (l l') "(% & % & Hinv)"; simplify_eq/=.
+    rel_xchg_l_atomic.
+    iInv (relocN .@ "ref" .@ (l,l')) as (v v') "[Hv1 [>Hv2 #Hv]]" "Hclose".
+    iModIntro. iExists _; iFrame "Hv1".
+    iNext. iIntros "Hw1".
+    rel_xchg_r.
+    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
+    { iNext; iExists _, _; simpl; iFrame. }
+    value_case.
+  Qed.
+
   Lemma refines_load e e' A :
     (REL e << e' : ref A) -∗
     REL !e << !e' : A.

theories/logic/proofmode/spec_tactics.v

@@ -190,6 +190,51 @@ Tactic Notation "tp_store" constr(j) :=
   |iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
   |pm_reduce (* new goal *)].
 
+
+Lemma tac_tp_xchg `{relocG Σ} k Δ1 Δ2 E1 i1 i2 K' e (l : loc) e' e2 v' v Q :
+  (∀ P, ElimModal True false false (|={E1}=> P) P Q Q) →
+  nclose specN ⊆ E1 →
+  envs_lookup_delete false i1 Δ1 = Some (false, refines_right k e, Δ2)%I →
+  e = fill K' (Xchg (# l) e') →
+  IntoVal e' v →
+  (* re-compose the expression and the evaluation context *)
+  envs_lookup i2 Δ2 = Some (false, l ↦ₛ v')%I →
+  e2 = fill K' (of_val v') →
+  match envs_simple_replace i2 false
+     (Esnoc (Esnoc Enil i1 (refines_right k e2)) i2 (l ↦ₛ v)) Δ2 with
+  | None => False
+  | Some Δ3 => envs_entails Δ3 Q
+  end →
+  envs_entails Δ1 Q.
+Proof.
+  rewrite /IntoVal.
+  rewrite envs_entails_eq. intros ??? -> <- ? -> HQ.
+  rewrite envs_lookup_delete_sound //; simpl.
+  destruct (envs_simple_replace _ _ _ _) as [Δ3|] eqn:HΔ3; last done.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id.
+  rewrite !assoc -(assoc _ spec_ctx).
+  rewrite -fill_app step_xchg // fill_app.
+  rewrite -[Q]elim_modal //.
+  apply bi.sep_mono_r.
+  apply bi.wand_intro_l.
+  rewrite (comm _ _ (l ↦ₛ v)%I). simpl.
+  rewrite assoc. rewrite (comm _ spec_ctx (l ↦ₛ _)%I).
+  by rewrite bi.wand_elim_r.
+Qed.
+
+Tactic Notation "tp_xchg" constr(j) :=
+  iStartProof;
+  eapply (tac_tp_store j);
+  [iSolveTC || fail "tp_store: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_store: cannot prove 'nclose specN ⊆ ?'"
+  |iAssumptionCore || fail "tp_store: cannot find '" j " ' RHS"
+  |tp_bind_helper
+  |iSolveTC || fail "tp_store: cannot convert the argument to a value"
+  |iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
+  |simpl; reflexivity || fail "tp_store: this should not happen"
+  |pm_reduce (* new goal *)].
+
 (* *)
 (* DF: *)
 (* If [envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)] and *)

theories/logic/proofmode/tactics.v

@@ -348,6 +348,86 @@ Tactic Notation "rel_store_r" :=
   |reflexivity
   |rel_finish  (** new goal *)].
 
+(** Xchg *)
+Lemma tac_rel_xchg_l_simpl `{!relocG Σ} K ℶ1 ℶ2 ℶ3 i1 (l : loc) v e' v' e t eres A :
+  e = fill K (Xchg (# l) e') →
+  IntoVal e' v' →
+  MaybeIntoLaterNEnvs 1 ℶ1 ℶ2 →
+  envs_lookup i1 ℶ2 = Some (false, l ↦ v)%I →
+  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ v')) ℶ2 = Some ℶ3 →
+  eres = fill K (of_val v) →
+  envs_entails ℶ3 (refines ⊤ eres t A) →
+  envs_entails ℶ1 (refines ⊤ e t A).
+Proof.
+  rewrite envs_entails_eq. intros ?????? Hg.
+  subst e eres.
+  rewrite into_laterN_env_sound envs_simple_replace_sound //; simpl.
+  rewrite bi.later_sep.
+  rewrite right_id.
+  rewrite -(refines_xchg_l K ⊤ l).
+  rewrite -fupd_intro.
+  rewrite -(bi.exist_intro v).
+  by rewrite Hg.
+Qed.
+
+Lemma tac_rel_xchg_r `{!relocG Σ} K ℶ1 ℶ2 i1 E (l : loc) v e' v' e t eres A :
+  e = fill K (Xchg (# l) e') →
+  IntoVal e' v' →
+  nclose specN ⊆ E →
+  envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
+  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) ℶ1 = Some ℶ2 →
+  eres = fill K (of_val v) →
+  envs_entails ℶ2 (refines E t eres A) →
+  envs_entails ℶ1 (refines E t e A).
+Proof.
+  rewrite envs_entails_eq. intros ?????? Hg.
+  subst e eres.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id.
+  rewrite (refines_xchg_r E K) //.
+  rewrite Hg.
+  apply bi.wand_elim_l.
+Qed.
+
+Tactic Notation "rel_xchg_l" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦ _)%I) => l end in
+    iAssumptionCore || fail "rel_xchg_l: cannot find" l "↦ₛ ?" in
+  rel_pures_l;
+  first
+    [rel_reshape_cont_l ltac:(fun K e' =>
+       eapply (tac_rel_xchg_l_simpl K);
+       [reflexivity (** e = fill K (#l <- e') *)
+       |iSolveTC    (** e' is a value *)
+       |idtac..])
+    |fail 1 "rel_xchg_l: cannot find 'Xchg'"];
+  (* the remaining goals are from tac_rel_xchg_l (except for the first one, which has already been solved by this point) *)
+  [iSolveTC        (** IntoLaters *)
+  |solve_mapsto ()
+  |pm_reflexivity || fail "rel_xchg_l: this should not happen O-:"
+  |reflexivity
+  |rel_finish  (** new goal *)].
+
+Tactic Notation "rel_xchg_l_atomic" := rel_apply_l refines_xchg_l.
+
+Tactic Notation "rel_xchg_r" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
+    iAssumptionCore || fail "rel_xchg_r: cannot find" l "↦ₛ ?" in
+  rel_pures_r;
+  first
+    [rel_reshape_cont_r ltac:(fun K e' =>
+       eapply (tac_rel_xchg_r K);
+       [reflexivity|iSolveTC|idtac..])
+    |fail 1 "rel_xchg_r: cannot find 'Xchg'"];
+  (* the remaining goals are from tac_rel_xchg_r (except for the first one, which has already been solved by this point) *)
+  [solve_ndisj || fail "rel_xchg_r: cannot prove 'nclose specN ⊆ ?'"
+  |solve_mapsto ()
+  |pm_reflexivity || fail "rel_xchg_r: this should not happen O-:"
+  |reflexivity
+  |rel_finish  (** new goal *)].
+
+
 (** Alloc *)
 Tactic Notation "rel_alloc_l_atomic" := rel_apply_l refines_alloc_l.
 

theories/logic/rules.v

@@ -183,6 +183,20 @@ Section rules.
     iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
+  Lemma refines_xchg_r E K l e1 v1 v t A :
+    nclose specN ⊆ E →
+    IntoVal e1 v1 →
+    l ↦ₛ v -∗
+    (l ↦ₛ v1 -∗ REL t << fill K (of_val v) @ E : A)
+    -∗ REL t << fill K (Xchg #l e1) @ E : A.
+  Proof.
+    rewrite /IntoVal. iIntros (?<-) "Hl Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    admit.
+  Admitted.
+
+
   Lemma refines_cmpxchg_fail_r E K l e1 e2 v1 v2 v t A :
     nclose specN ⊆ E →
     IntoVal e1 v1 →
@@ -369,6 +383,18 @@ Section rules.
     iApply (wp_store _ _ _ _ v' with "Hl"); auto.
   Qed.
 
+  Lemma refines_xchg_l K E l e v' t A :
+    IntoVal e v' →
+    (|={⊤,E}=> ∃ v, ▷ l ↦ v ∗
+      ▷(l ↦ v' -∗ REL fill K (of_val v) << t @ E : A))
+    -∗ REL fill K (Xchg #l e) << t : A.
+  Proof.
+    iIntros (<-) "Hlog".
+    iApply refines_atomic_l; auto.
+    iMod "Hlog" as (v) "[Hl Hlog]". iModIntro.
+    iApply (wp_xchg _ _ _ _ v' with "Hl"); auto.
+  Qed.
+
   Lemma refines_cmpxchg_l K E l e1 e2 v1 v2 t A :
     IntoVal e1 v1 →
     IntoVal e2 v2 →

theories/logic/spec_rules.v

@@ -211,6 +211,37 @@ Section rules.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
+  Lemma step_xchg E j K l e (v v' : val) :
+    IntoVal e v →
+    nclose specN ⊆ E →
+    spec_ctx ∗ j ⤇ fill K (Xchg #l e) ∗ l ↦ₛ v'
+    ={E}=∗ spec_ctx ∗ j ⤇ fill K (of_val v') ∗ l ↦ₛ v.
+  Proof.
+    iIntros (<-?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    iDestruct "Hinv" as (ρ) "Hinv".
+    rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
+    iInv specN as (tp σ) ">[Hown %]" "Hclose".
+    iDestruct (own_valid_2 with "Hown Hj")
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
+    iDestruct (own_valid_2 with "Hown Hl")
+      as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
+    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+    { by eapply auth_update, prod_local_update_1, singleton_local_update,
+        (exclusive_local_update _ (Excl (fill K (of_val v')))). }
+    iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
+    { eapply auth_update, prod_local_update_2.
+      apply: singleton_local_update.
+      { by rewrite /to_heap lookup_fmap Hl. }
+      apply: (exclusive_local_update _
+        (1%Qp, to_agree (Some v : leibnizO (option val)))).
+      apply: pair_exclusive_l. done. }
+    iFrame "Hj Hl". iApply "Hclose". iNext.
+    iExists (<[j:=fill K (of_val v')]> tp), (state_upd_heap <[l:=Some v]> σ).
+    rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+  Qed.
+
   (** CmpXchg & FAA *)
   Lemma step_cmpxchg_fail E j K l q v' e1 v1 e2 v2 :
     IntoVal e1 v1 →

theories/tests/proofmode_tests.v

@@ -91,5 +91,29 @@ Proof.
   rel_values.
 Qed.
 
+
+Lemma test_xchg_1 l1 l2 (v1 v2 : val) (A : lrel Σ) :
+  l1 ↦ v1 -∗
+  l2 ↦ₛ v2 -∗
+  (l1 ↦ #3 -∗ l2 ↦ₛ #3 -∗ A v1 v2) -∗
+  REL Xchg #l1 #3 << Xchg #l2 #3 : A.
+Proof.
+  iIntros "Hl1 Hl2 H".
+  rel_xchg_l. rel_xchg_r. rel_values.
+  iModIntro. iApply ("H" with "Hl1 Hl2").
+Qed.
+
+Lemma test_xchg_2 l1 l2 (v1 v2 : val) (A : lrel Σ) :
+  l1 ↦ v1 -∗
+  l2 ↦ₛ v2 -∗
+  (l1 ↦ #3 -∗ l2 ↦ₛ #3 -∗ A v1 v2) -∗
+  REL Xchg #l1 #3 << (let: "x" := !#l2 in #l2 <- #3;; "x") : A.
+Proof.
+  iIntros "Hl1 Hl2 H".
+  rel_xchg_l. rel_load_r. rel_pures_r.
+  rel_store_r. rel_pures_r. rel_values.
+  iModIntro. iApply ("H" with "Hl1 Hl2").
+Qed.
+
 End test.
 

theories/typing/fundamental.v

@@ -264,6 +264,18 @@ Section fundamental.
     - by iApply "IH2".
   Qed.
 
+  Lemma bin_log_related_xchg Δ Γ e1 e2 e1' e2' τ :
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef τ) -∗
+    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
+    {Δ;Γ} ⊨ Xchg e1 e2 ≤log≤ Xchg e1' e2' : τ.
+  Proof.
+    iIntros "IH1 IH2".
+    intro_clause.
+    iApply (refines_xchg with "[IH1] [IH2]").
+    - by iApply "IH1".
+    - by iApply "IH2".
+  Qed.
+
   Lemma bin_log_related_FAA Δ Γ e1 e2 e1' e2' :
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TRef TNat) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : TNat) -∗
@@ -574,6 +586,7 @@ Section fundamental.
       + iApply bin_log_related_alloc; by iApply fundamental.
       + iApply bin_log_related_load; by iApply fundamental.
       + iApply bin_log_related_store; by iApply fundamental.
+      + iApply bin_log_related_xchg; by iApply fundamental.
       + iApply bin_log_related_FAA; eauto;
           by iApply fundamental.
       + iApply bin_log_related_CmpXchg; eauto;

theories/typing/types.v

@@ -199,6 +199,7 @@ Inductive typed : stringmap type → expr → type → Prop :=
   | TAlloc Γ e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : ref τ
   | TLoad Γ e τ : Γ ⊢ₜ e : ref τ → Γ ⊢ₜ Load e : τ
   | TStore Γ e e' τ : Γ ⊢ₜ e : ref τ → Γ ⊢ₜ e' : τ → Γ ⊢ₜ Store e e' : ()
+  | TXchg Γ e e' τ : Γ ⊢ₜ e : ref τ → Γ ⊢ₜ e' : τ → Γ ⊢ₜ Xchg e e' : τ
   | TFAA Γ e1 e2 :
      Γ ⊢ₜ e1 : ref TNat →
      Γ ⊢ₜ e2 : TNat →