Merge branch 'atomic-exchange' into 'master'

add atomic exchange operation

See merge request iris/iris!675

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)).

iris_heap_lang/derived_laws.v

@@ -205,6 +205,37 @@ 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 →
+  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
+Proof.
+  iIntros (Hlookup Φ) "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 →
+  {{{ ▷ 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 :
+  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
+Proof.
+  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 :
+   {{{ ▷ 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 →

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,9 +334,10 @@ 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]
-     | FAA e1 e2 => GenNode 18 [go e1; go e2]
-     | NewProph => GenNode 19 []
-     | Resolve e0 e1 e2 => GenNode 20 [go e0; go e1; go e2]
+     | Xchg e0 e1 => GenNode 18 [go e0; go e1]
+     | FAA e1 e2 => GenNode 19 [go e1; go e2]
+     | NewProph => GenNode 20 []
+     | Resolve e0 e1 e2 => GenNode 21 [go e0; go e1; go e2]
      end
    with gov v :=
      match v with
@@ -367,9 +371,10 @@ Proof.
      | GenNode 15 [e] => Load (go e)
      | GenNode 16 [e1; e2] => Store (go e1) (go e2)
      | GenNode 17 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
-     | 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 18 [e0; e1] => Xchg (go e0) (go e1)
+     | GenNode 19 [e1; e2] => FAA (go e1) (go e2)
+     | GenNode 20 [] => NewProph
+     | GenNode 21 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
      | _ => 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,13 @@ 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 →
+     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]! *)

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

iris_heap_lang/primitive_laws.v

@@ -312,6 +312,26 @@ Proof.
   iApply (twp_store with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
+Lemma twp_xchg s E l v' 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 ns κs nt) "[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 :
+  {{{ ▷ 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

iris_heap_lang/proofmode.v

@@ -370,6 +370,37 @@ 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 →
+  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 →
+  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 +717,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

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,17 @@ 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 σ :
+  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 /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) σ #()
@@ -342,6 +356,8 @@ Proof.
              apply un_op_eval_erase in H as [? [? ?]]
            | H : bin_op_eval _ (erase_val _) (erase_val _) = Some _ |- _ =>
              apply bin_op_eval_erase in H as [? [? ?]]
+           | H : val_is_unboxed (erase_val _) |- _ =>
+             apply -> val_is_unboxed_erased in H
            end; simplify_eq/=;
     try (by repeat econstructor);
   eauto using erased_head_step_head_step_rec,
@@ -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,14 @@ Proof.
   by destruct lookup; simplify_eq.
 Qed.
 
+Lemma head_step_erased_prim_step_xchg σ l v w :
+  heap σ !! l = Some (Some v) →
+  ∃ e2' σ2' ef', prim_step (Xchg #l (erase_val w)) (erase_state σ) [] e2' σ2' ef'.
+Proof.
+  intros Hl. do 3 eexists; apply head_prim_step; econstructor.
+  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl; eauto.
+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 +764,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.

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

iris_staging/heap_lang/interpreter.v

@@ -535,6 +535,13 @@ Section interpreter.
       let '(l, _) := l_v0 in
       _ ← interp_modify_state (state_upd_heap <[l:=Some w]>);
       mret (LitV LitUnit)
+    | Xchg el e =>
+      w ← interp e;
+      vl ← interp el;
+      l_v0 ← read_loc "xchg" vl;
+      let '(l, v0) := l_v0 in
+      _ ← interp_modify_state (state_upd_heap <[l:=Some w]>);
+      mret v0
     | CmpXchg e e1 e2 =>
       v2 ← interp e2;
       v1 ← interp e1;

tests/heap_lang.v

@@ -199,6 +199,37 @@ Section tests.
     iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
   Qed.
 
+  Lemma wp_xchg l (v₁ v₂ : val) :
+    {{{ l ↦ v₁ }}}
+      Xchg #l v₂
+    {{{ RET v₁; l ↦ v₂ }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ".
+    wp_xchg.
+    iApply "HΦ" => //.
+  Qed.
+
+   Lemma twp_xchg l (v₁ v₂ : val) :
+     l ↦ v₁ -∗
+       WP  Xchg #l v₂ [{ v₁, l ↦ v₂ }].
+  Proof.
+    iIntros "Hl".
+    wp_xchg => //.
+  Qed.
+
+  Lemma wp_xchg_inv N l (v : val) :
+    {{{ inv N (∃ v, l ↦ v) }}}
+      Xchg #l v
+    {{{ v', RET v'; True }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ".
+    iInv "Hl" as (v') "Hl" "Hclose".
+    wp_xchg.
+    iApply "HΦ".
+    iApply "Hclose".
+    iExists _ => //.
+  Qed.
+
   Lemma wp_alloc_split :
     ⊢ WP Alloc #0 {{ _, True }}.
   Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
@@ -333,7 +364,7 @@ Section mapsto_tests.
   (* Loading from the general mapsto for any [dfrac]. *)
   Lemma general_mapsto dq l v :
     [[{ l ↦{dq} v }]] ! #l [[{ RET v; True }]].
-  Proof. 
+  Proof.
     iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
   Qed.
 
@@ -382,6 +413,7 @@ Section atomic.
     (* Test if a side-condition for [Atomic] is generated *)
     iIntros (?) "H". iInv "H" as "H". Show.
   Abort.
+
 End atomic.
 
 Section printing_tests.