Commit 4e15875a authored by Simon Hudon's avatar Simon Hudon
Browse files

add atomic exchange operation

parent 6ce8b332
......@@ -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)).
......
......@@ -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
......
......@@ -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]! *)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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.
......
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment