Commit 78b3986b authored by Simon Hudon's avatar Simon Hudon
Browse files

little fixes

parent 254e94b2
......@@ -207,36 +207,40 @@ Qed.
Lemma twp_xchg_offset s E l off vs v v' :
vs !! off = Some v
val_is_unboxed v ->
val_is_unboxed 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Φ".
iIntros (Hlookup Hunboxed 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 ->
vs !! off = Some v
val_is_unboxed 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Φ").
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) ->
val_is_unboxed (vs !!! off)
val_is_unboxed v
[[{ 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 => //.
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) ->
val_is_unboxed (vs !!! off)
val_is_unboxed 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Φ").
iIntros (? ? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_xchg_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
......
......@@ -334,10 +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]
| 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]
| 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
......@@ -371,10 +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 21 [e0; e1] => Xchg (go e0) (go e1)
| 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 :=
......@@ -685,6 +685,7 @@ Inductive head_step : expr → state → list observation → expr → state →
| XchgS l v1 v2 σ :
σ.(heap) !! l = Some $ Some v1
val_is_unboxed v1
val_is_unboxed v2
head_step (Xchg (Val $ LitV $ LitLoc l) (Val v2)) σ
[]
(Val v1) (state_upd_heap <[l:=Some v2]> σ)
......
......@@ -313,11 +313,12 @@ Proof.
Qed.
Lemma twp_xchg s E l v' v :
val_is_unboxed v' ->
val_is_unboxed 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 (Hv Hv' Φ) "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.
......@@ -326,11 +327,12 @@ Proof.
Qed.
Lemma wp_xchg s E l v' v :
val_is_unboxed v' ->
val_is_unboxed 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Φ").
iIntros (Hv Hv' Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_xchg with "H"); [by auto..|]. iIntros "H HΦ". by iApply "HΦ".
Qed.
......
......@@ -373,14 +373,15 @@ 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 ->
val_is_unboxed v'
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=> ????.
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.
......@@ -389,7 +390,8 @@ Proof.
Qed.
Lemma tac_twp_xchg Δ s E i K l v v' Φ :
envs_lookup i Δ = Some (false, l v)%I
val_is_unboxed v ->
val_is_unboxed v'
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
......
......@@ -279,17 +279,18 @@ Proof.
eexists _, _, _, _; simpl; split; first econstructor; eauto.
Qed.
Lemma erased_head_step_head_step_Xchg l v w σ :
val_is_unboxed v ->
val_is_unboxed v
val_is_unboxed 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.
intros Hv Hw Hl.
rewrite lookup_erase_heap in Hl.
destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
rewrite val_is_unboxed_erased in Hv * => //; intros Hv.
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 //.
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)
......@@ -358,6 +359,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,
......@@ -722,13 +725,14 @@ Proof.
Qed.
Lemma head_step_erased_prim_step_xchg σ l v w :
val_is_unboxed v ->
val_is_unboxed v
val_is_unboxed w
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.
intros Hv Hw Hl. do 3 eexists; apply head_prim_step; econstructor.
1: rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl; eauto.
1,2: by rewrite val_is_unboxed_erased.
Qed.
Lemma head_step_erased_prim_step_store σ l v w :
......
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