From 4e15875ab1372784cd6ea25a7873c8e8f5c0e69d Mon Sep 17 00:00:00 2001
From: Simon Hudon <simonhudon@google.com>
Date: Sun, 28 Feb 2021 00:01:46 -0500
Subject: [PATCH] add atomic exchange operation

---
 iris_heap_lang/class_instances.v |  2 ++
 iris_heap_lang/derived_laws.v    | 35 ++++++++++++++++++++
 iris_heap_lang/lang.v            | 20 +++++++++++-
 iris_heap_lang/metatheory.v      |  4 ++-
 iris_heap_lang/primitive_laws.v  | 22 +++++++++++++
 iris_heap_lang/proofmode.v       | 55 ++++++++++++++++++++++++++++++++
 iris_heap_lang/proph_erasure.v   | 28 ++++++++++++++++
 iris_heap_lang/tactics.v         |  2 ++
 8 files changed, 166 insertions(+), 2 deletions(-)

diff --git a/iris_heap_lang/class_instances.v b/iris_heap_lang/class_instances.v
index 0e1f94c5a..6d3dac76d 100644
--- a/iris_heap_lang/class_instances.v
+++ b/iris_heap_lang/class_instances.v
@@ -50,6 +50,8 @@ Section atomic.
   Proof. solve_atomic. Qed.
   Global Instance load_atomic s v : Atomic s (Load (Val v)).
   Proof. solve_atomic. Qed.
+  Global Instance xchg_atomic s v1 v2 : Atomic s (Xchg (Val v1) (Val v2)).
+  Proof. solve_atomic. Qed.
   Global Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
   Proof. solve_atomic. Qed.
   Global Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 72ce1856a..94c3bcc69 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -205,6 +205,41 @@ Proof.
   iApply (twp_store_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
+Lemma twp_xchg_offset s E l off vs v v' :
+  (vs !! off) = Some v →
+  val_is_unboxed v ->
+  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
+Proof.
+  iIntros (Hlookup Hunboxed Φ) "Hl HΦ".
+  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
+  iApply (twp_xchg with "Hl1") => //. iIntros "Hl1".
+  iApply "HΦ". iApply "Hl2". iApply "Hl1".
+Qed.
+Lemma wp_xchg_offset s E l off vs v v' :
+  (vs !! off) = Some v →
+  val_is_unboxed v ->
+  {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
+Proof.
+  iIntros (? ? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
+  iApply (twp_xchg_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
+Qed.
+
+Lemma twp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
+   val_is_unboxed (vs !!! off) ->
+  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
+Proof.
+  intros ?. setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
+  by apply vlookup_lookup.
+Qed.
+
+Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
+   val_is_unboxed (vs !!! off) ->
+  {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
+Proof.
+  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
+  iApply (twp_xchg_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
+Qed.
+
 Lemma twp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
   vs !! off = Some v' →
   v' = v1 →
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index bb686c72b..5a58f32b4 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -112,6 +112,7 @@ Inductive expr :=
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
+  | Xchg (e0 : expr) (e1 : expr) (* exchange *)
   | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
   (* Prophecy *)
   | NewProph
@@ -249,6 +250,8 @@ Proof.
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
      | CmpXchg e0 e1 e2, CmpXchg e0' e1' e2' =>
         cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
+     | Xchg e0 e1, Xchg e0' e1' =>
+        cast_if_and (decide (e0 = e0')) (decide (e1 = e1'))
      | FAA e1 e2, FAA e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
      | NewProph, NewProph => left _
@@ -331,6 +334,7 @@ Proof.
      | Load e => GenNode 15 [go e]
      | Store e1 e2 => GenNode 16 [go e1; go e2]
      | CmpXchg e0 e1 e2 => GenNode 17 [go e0; go e1; go e2]
+     | Xchg e0 e1 => GenNode 21 [go e0; go e1]
      | FAA e1 e2 => GenNode 18 [go e1; go e2]
      | NewProph => GenNode 19 []
      | Resolve e0 e1 e2 => GenNode 20 [go e0; go e1; go e2]
@@ -370,6 +374,7 @@ Proof.
      | GenNode 18 [e1; e2] => FAA (go e1) (go e2)
      | GenNode 19 [] => NewProph
      | GenNode 20 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
+     | GenNode 21 [e0; e1] => Xchg (go e0) (go e1)
      | _ => Val $ LitV LitUnit (* dummy *)
      end
    with gov v :=
@@ -384,7 +389,7 @@ Proof.
    for go).
  refine (inj_countable' enc dec _).
  refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
- - destruct e as [v| | | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
+ - destruct e as [v| | | | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
      [exact (gov v)|done..].
  - destruct v; by f_equal.
 Qed.
@@ -422,6 +427,8 @@ Inductive ectx_item :=
   | LoadCtx
   | StoreLCtx (v2 : val)
   | StoreRCtx (e1 : expr)
+  | XchgLCtx (v2 : val)
+  | XchgRCtx (e1 : expr)
   | CmpXchgLCtx (v1 : val) (v2 : val)
   | CmpXchgMCtx (e0 : expr) (v2 : val)
   | CmpXchgRCtx (e0 : expr) (e1 : expr)
@@ -459,6 +466,8 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
   | LoadCtx => Load e
   | StoreLCtx v2 => Store e (Val v2)
   | StoreRCtx e1 => Store e1 e
+  | XchgLCtx v2 => Xchg e (Val v2)
+  | XchgRCtx e1 => Xchg e1 e
   | CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
   | CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
   | CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
@@ -490,6 +499,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
   | Free e => Free (subst x v e)
   | Load e => Load (subst x v e)
+  | Xchg e1 e2 => Xchg (subst x v e1) (subst x v e2)
   | Store e1 e2 => Store (subst x v e1) (subst x v e2)
   | CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
   | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
@@ -672,6 +682,14 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV LitUnit) (state_upd_heap <[l:=Some w]> σ)
                []
+  | XchgS l v1 v2 σ :
+     σ.(heap) !! l = Some $ Some v1 →
+     val_is_unboxed v1 →
+     head_step (Xchg (Val $ LitV $ LitLoc l) (Val v2)) σ
+               []
+               (Val v1) (state_upd_heap <[l:=Some v2]> σ)
+               []
+
   | CmpXchgS l v1 v2 vl σ b :
      σ.(heap) !! l = Some $ Some vl →
      (* Crucially, this compares the same way as [EqOp]! *)
diff --git a/iris_heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
index 54619aa4a..2bc59de5b 100644
--- a/iris_heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -13,7 +13,7 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
   | Rec f x e => is_closed_expr (f :b: x :b: X) e
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
      is_closed_expr X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | Xchg e1 e2 | FAA e1 e2 =>
      is_closed_expr X e1 && is_closed_expr X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2 =>
      is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
@@ -137,6 +137,7 @@ Proof.
   - by apply heap_closed_alloc.
   - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
   - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
+  - select (_ !! _ = Some _) ltac:(fun H => by specialize (Clσ1 _ _ H)).
   - case_match; try apply map_Forall_insert_2; by naive_solver.
 Qed.
 
@@ -160,6 +161,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
   | Free e => Free (subst_map vs e)
   | Load e => Load (subst_map vs e)
   | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
+  | Xchg e1 e2 => Xchg (subst_map vs e1) (subst_map vs e2)
   | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
   | NewProph => NewProph
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 32a2d6f25..eb0cd29af 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -312,6 +312,28 @@ Proof.
   iApply (twp_store with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
+Lemma twp_xchg s E l v' v :
+  val_is_unboxed v' ->
+  [[{ l ↦ v' }]] Xchg (Val $ LitV $ LitLoc l) (Val v) @ s; E
+  [[{ RET v'; l ↦ v }]].
+Proof.
+  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
+  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto with head_step.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_xchg s E l v' v :
+  val_is_unboxed v' ->
+  {{{ ▷ l ↦ v' }}} Xchg (Val $ LitV (LitLoc l)) (Val v) @ s; E
+  {{{ RET v'; l ↦ v }}}.
+Proof.
+  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
+  iApply (twp_xchg with "H"); [by auto..|]. iIntros "H HΦ". by iApply "HΦ".
+Qed.
+
 Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
   v' ≠ v1 → vals_compare_safe v' v1 →
   [[{ l ↦{dq} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 55314fede..031de179b 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -370,6 +370,39 @@ Proof.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
 
+Lemma tac_wp_xchg Δ Δ' s E i K l v v' Φ :
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I →
+  val_is_unboxed v ->
+  match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' with
+  | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ v) @ s; E {{ Φ }})
+  | None => False
+  end →
+  envs_entails Δ (WP fill K (Xchg (LitV l) (Val v')) @ s; E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq=> ????.
+  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+  rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
+  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite right_id.
+    by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+Lemma tac_twp_xchg Δ s E i K l v v' Φ :
+  envs_lookup i Δ = Some (false, l ↦ v)%I →
+  val_is_unboxed v ->
+  match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ with
+  | Some Δ' => envs_entails Δ' (WP fill K (Val $ v) @ s; E [{ Φ }])
+  | None => False
+  end →
+  envs_entails Δ (WP fill K (Xchg (LitV l) v') @ s; E [{ Φ }]).
+Proof.
+  rewrite envs_entails_eq. intros.
+  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
+  rewrite -twp_bind. eapply wand_apply; first by eapply twp_xchg.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
+
 Lemma tac_wp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
@@ -686,6 +719,28 @@ Tactic Notation "wp_store" :=
   | _ => fail "wp_store: not a 'wp'"
   end.
 
+Tactic Notation "wp_xchg" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_xchg: cannot find" l "↦ ?" in
+  wp_pures;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_xchg _ _ _ _ _ K))
+      |fail 1 "wp_xchg: cannot find 'Xchg' in" e];
+    [iSolveTC
+    |solve_mapsto ()
+    |pm_reduce; first [wp_seq|wp_finish]]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_xchg _ _ _ _ K))
+      |fail 1 "wp_xchg: cannot find 'Xchg' in" e];
+    [solve_mapsto ()
+    |pm_reduce; first [wp_seq|wp_finish]]
+  | _ => fail "wp_xchg: not a 'wp'"
+  end.
+
 Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 704a56c57..202b61c4a 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -43,6 +43,7 @@ Fixpoint erase_expr (e : expr) : expr :=
   | AllocN e1 e2 => AllocN (erase_expr e1) (erase_expr e2)
   | Free e => Free (erase_expr e)
   | Load e => Load (erase_expr e)
+  | Xchg e1 e2 => Xchg (erase_expr e1) (erase_expr e2)
   | Store e1 e2 => Store (erase_expr e1) (erase_expr e2)
   | CmpXchg e0 e1 e2 => CmpXchg (erase_expr e0) (erase_expr e1) (erase_expr e2)
   | FAA e1 e2 => FAA (erase_expr e1) (erase_expr e2)
@@ -97,6 +98,8 @@ Fixpoint erase_ectx_item (Ki : ectx_item) : list ectx_item :=
   | AllocNRCtx e1 => [AllocNRCtx (erase_expr e1)]
   | FreeCtx => [FreeCtx]
   | LoadCtx => [LoadCtx]
+  | XchgLCtx v2 => [XchgLCtx (erase_val v2)]
+  | XchgRCtx e1 => [XchgRCtx (erase_expr e1)]
   | StoreLCtx v2 => [StoreLCtx (erase_val v2)]
   | StoreRCtx e1 => [StoreRCtx (erase_expr e1)]
   | CmpXchgLCtx v1 v2 => [CmpXchgLCtx (erase_val v1) (erase_val v2)]
@@ -275,6 +278,19 @@ Proof.
   destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
   eexists _, _, _, _; simpl; split; first econstructor; eauto.
 Qed.
+Lemma erased_head_step_head_step_Xchg l v w σ :
+  val_is_unboxed v ->
+  erase_heap (heap σ) !! l = Some (Some v) →
+  head_steps_to_erasure_of (Xchg #l w) σ v
+   {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
+Proof.
+  intros ? Hl.
+  rewrite lookup_erase_heap in Hl.
+  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
+  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
+  - rewrite val_is_unboxed_erased in H * => //.
+  - rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
+Qed.
 Lemma erased_head_step_head_step_Store l v w σ :
   erase_heap (heap σ) !! l = Some (Some v) →
   head_steps_to_erasure_of (#l <- w) σ #()
@@ -349,6 +365,7 @@ Proof.
     erased_head_step_head_step_AllocN,
     erased_head_step_head_step_Free,
     erased_head_step_head_step_Load,
+    erased_head_step_head_step_Xchg,
     erased_head_step_head_step_Store,
     erased_head_step_head_step_CmpXchg,
     erased_head_step_head_step_FAA.
@@ -704,6 +721,16 @@ Proof.
   by destruct lookup; simplify_eq.
 Qed.
 
+Lemma head_step_erased_prim_step_xchg σ l v w :
+  val_is_unboxed v ->
+  heap σ !! l = Some (Some v) →
+  ∃ e2' σ2' ef', prim_step (Xchg #l (erase_val w)) (erase_state σ) [] e2' σ2' ef'.
+Proof.
+  intros ? Hw. do 3 eexists; apply head_prim_step; econstructor.
+  - rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
+  - by rewrite val_is_unboxed_erased.
+Qed.
+
 Lemma head_step_erased_prim_step_store σ l v w :
   heap σ !! l = Some (Some v) →
   ∃ e2' σ2' ef', prim_step (#l <- erase_val w) (erase_state σ) [] e2' σ2' ef'.
@@ -739,6 +766,7 @@ Proof.
                 head_step_erased_prim_step_free,
                 head_step_erased_prim_step_load,
                 head_step_erased_prim_step_store,
+                head_step_erased_prim_step_xchg,
                 head_step_erased_prim_step_FAA;
     by do 3 eexists; apply head_prim_step; econstructor.
 Qed.
diff --git a/iris_heap_lang/tactics.v b/iris_heap_lang/tactics.v
index 87484570c..2415618e0 100644
--- a/iris_heap_lang/tactics.v
+++ b/iris_heap_lang/tactics.v
@@ -37,6 +37,8 @@ Ltac reshape_expr e tac :=
     | Load ?e                         => add_item LoadCtx vs K e
     | Store ?e (Val ?v)               => add_item (StoreLCtx v) vs K e
     | Store ?e1 ?e2                   => add_item (StoreRCtx e1) vs K e2
+    | Xchg ?e (Val ?v)                => add_item (XchgLCtx v) vs K e
+    | Xchg ?e1 ?e2                    => add_item (XchgRCtx e1) vs K e2
     | CmpXchg ?e0 (Val ?v1) (Val ?v2) => add_item (CmpXchgLCtx v1 v2) vs K e0
     | CmpXchg ?e0 ?e1 (Val ?v2)       => add_item (CmpXchgMCtx e0 v2) vs K e1
     | CmpXchg ?e0 ?e1 ?e2             => add_item (CmpXchgRCtx e0 e1) vs K e2
-- 
GitLab