Commit d89c0111 authored by Marianna Rapoport's avatar Marianna Rapoport

Pass over Ralf's comments on Commit 851f05c2

parent b2c331e6
......@@ -425,11 +425,14 @@ Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cas_compare_safe !_ !_ /.
Local Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
Local Notation SOMEV x := (InjRV x) (only parsing).
(** We extend CAS to support atomic resolution of prophecy variables as follows:
[CAS p e1 e1 pv1 pv2]
where [pv1] and [pv2] are values of type [option (proph * val)].
If [CAS p e1 e2] succeeds, and if [pv1 = Some (p, v)], we atomically resolve the
prophecy variable [p] to [v]. If the [CAS] fails, we do the same of [pv2]:
prophecy variable [p] to [v]. If the [CAS] fails, we do the same with [pv2]:
[let b = CAS p e1 e2 ;;
match (if b then pv1 else pv2) with
......@@ -439,12 +442,14 @@ Arguments vals_cas_compare_safe !_ !_ /.
The following function takes a value and extracts its encoding
of an optional prophecy-value pair.
If [extract_proph_resolve] returns [None], it indicates an invalid encoding,
whereas [Some None] means that it's a valid encoding of no pair.
*)
Definition extract_proph_resolve (v : val) : option (option (proph * val)) :=
match v with
| InjLV (LitV LitUnit) =>
| NONEV =>
Some None
| InjRV (PairV (LitV (LitProphecy p)) v') =>
| SOMEV (PairV (LitV (LitProphecy p)) v') =>
Some (Some (p, v'))
| _ =>
None
......@@ -491,17 +496,19 @@ Inductive head_step : expr → state → option observation -> expr → state
| StoreS l e v σ :
to_val e = Some v is_Some (σ.1 !! l)
head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ.1, σ.2) []
| CasFailS l e1 v1 e2 v2 e3 v3 e4 v4 pv vl σ :
| CasFailS l e1 v1 e2 v2 e3 p1 e4 p2 pv vl σ :
to_val e1 = Some v1 to_val e2 = Some v2
to_val e3 = Some v3 to_val e4 = Some v4
extract_proph_resolve v4 = Some pv
to_val e3 = Some p1 to_val e4 = Some p2
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some pv
σ.1 !! l = Some vl vl v1
vals_cas_compare_safe vl v1
head_step (CAS (Lit $ LitLoc l) e1 e2 e3 e4) σ pv (Lit $ LitBool false) σ []
| CasSucS l e1 v1 e2 v2 e3 v3 e4 v4 pv σ :
| CasSucS l e1 v1 e2 v2 e3 p1 e4 p2 pv σ :
to_val e1 = Some v1 to_val e2 = Some v2
to_val e3 = Some v3 to_val e4 = Some v4
extract_proph_resolve v3 = Some pv
to_val e3 = Some p1 to_val e4 = Some p2
extract_proph_resolve p1 = Some pv
is_Some (extract_proph_resolve p2)
σ.1 !! l = Some v1
vals_cas_compare_safe v1 v1
head_step (CAS (Lit $ LitLoc l) e1 e2 e3 e4) σ pv (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2) []
......
......@@ -37,23 +37,25 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
because it requires both prophecy-value pairs to be None, rather than only
the pair that will be relevant depending on what the CAS evaluates to.
Does this matter? *)
cas_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 : val) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
cas_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 p1 p2 : val) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 p1 IntoVal e4 p2
extract_proph_resolve p1 = Some None
extract_proph_resolve p2 = Some None
val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas (#l, e1, e2, e3, e4) @
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #(if decide (v = w1) then true else false) >>>;
cas_suc_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some (Some (p, w))
cas_suc_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 p1 p2 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 p1 IntoVal e4 p2
extract_proph_resolve p1 = Some (Some (p, w))
is_Some (extract_proph_resolve p2)
val_is_unboxed w1
<<< mapsto l 1 w1 p v >>> cas (#l, e1, e2, e3, e4) @
<<< mapsto l 1 w2 v = Some w, RET #true>>>;
cas_fail_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w4 = Some (Some (p, w))
cas_fail_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 p1 p2 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 p1 IntoVal e4 p2
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 mapsto l 1 v' p v >>> cas (#l, e1, e2, e3, e4) @
<<< mapsto l 1 v' v = Some w, RET #false>>>;
......@@ -75,6 +77,8 @@ Notation "! e" := (load e) : expr_scope.
Notation "e1 <- e2" := (store (e1, e2)%E) : expr_scope.
Notation CAS e1 e2 e3 e4 e5 := (cas (e1, e2, e3, e4, e5)%E).
Notation "'cas:' e1 ',' e2 ',' e3" := (cas (e1, e2, e3, NONEV, NONEV)%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
End notation.
......@@ -120,10 +124,10 @@ Section proof.
wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_spec (l : loc) e1 e2 e3 e4 (w1 w2 w3 w4 : val) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
Lemma primitive_cas_spec (l : loc) e1 e2 e3 e4 (w1 w2 p1 p2 : val) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 p1 IntoVal e4 p2
extract_proph_resolve p1 = Some None
extract_proph_resolve p2 = Some None
val_is_unboxed w1
<<< (v : val), l v >>>
primitive_cas (#l, e1, e2, e3, e4) @
......@@ -136,33 +140,33 @@ Section proof.
iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
Qed.
Lemma primitive_cas_suc_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w3 = Some (Some (p, w))
Lemma primitive_cas_suc_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 p1 p2 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 p1 IntoVal e4 p2
extract_proph_resolve p1 = Some (Some (p, w))
is_Some (extract_proph_resolve p2)
val_is_unboxed w1
<<< l w1 p v >>>
primitive_cas (#l, e1, e2, e3, e4) @
<<< l w2 v = Some w, RET #true>>>.
Proof.
iIntros (<- <- <- <- ? ? Q Φ) "? AU". wp_let. repeat wp_proj.
iIntros (<- <- <- <- ? ? ? Q Φ) "? AU". wp_let. repeat wp_proj.
iMod "AU" as "[[H↦ Hp] [_ Hclose]]".
wp_apply (wp_cas_suc_proph with "[H↦ Hp]"); eauto with iFrame.
{ by left. }
wp_apply (wp_cas_suc_proph with "[H↦ Hp]"); eauto with iFrame; first by left.
iIntros "H". iMod ("Hclose" with "H") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_fail_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 w3 w4 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 w3 IntoVal e4 w4
extract_proph_resolve w4 = Some (Some (p, w))
Lemma primitive_cas_fail_proph_spec (l : loc) (e1 e2 e3 e4 : expr) (w1 w2 p1 p2 w : val) v (p : proph) :
IntoVal e1 w1 IntoVal e2 w2 IntoVal e3 p1 IntoVal e4 p2
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 l v' p v >>>
primitive_cas (#l, e1, e2, e3, e4) @
<<< l v' v = Some w, RET #false>>>.
Proof.
iIntros (<- <- <- <- ? ? Q Φ) "? AU". wp_let. repeat wp_proj.
iIntros (<- <- <- <- ? ? ? Q Φ) "? AU". wp_let. repeat wp_proj.
iMod "AU" as (v') "[(Hn & H↦ & Hp) [_ Hclose]]". iDestruct "Hn" as %Hn.
wp_apply (wp_cas_fail_proph with "[H↦ Hp]"); eauto with iFrame.
{ by right. }
wp_apply (wp_cas_fail_proph with "[H↦ Hp]"); eauto with iFrame; first by right.
iIntros "H". iMod ("Hclose" with "H") as "HΦ". by iApply "HΦ".
Qed.
End proof.
......
......@@ -609,7 +609,7 @@ Section cond_counter.
iDestruct "Accepted" as "[Q >[Hh◯ [Heq' [Hl_ghost_inv Hp']]]]".
iDestruct (sync_histories with "H◯ Hh◯") as %->.
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by iFrame | ..].
[ by left | done | by eauto | by iFrame | ..].
(* show that l3 ≠ l_new *)
destruct H as [|l3' H]; inversion Heq; subst l3'.
destruct (decide (l3 = l_new)) as [-> | Hn].
......@@ -679,7 +679,7 @@ Section cond_counter.
iDestruct (sync_histories with "H◯ Hh◯") as %->.
iDestruct "Hp'" as (v) "[Hp' Heq'']". iDestruct "Heq''" as %Heq'.
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by iFrame | ..].
[ by left | done | by eauto | by iFrame | ..].
iIntros "[_ Heq]". iDestruct "Heq" as %->. inversion Heq'.
*** (* Done: contradiction *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
......@@ -704,7 +704,7 @@ Section cond_counter.
iDestruct (sync_histories with "Hh◯ H◯") as %->. rewrite <- Heq'' in Heq.
by inversion Heq.
*** (* Done: contradiction *)
wp_apply (wp_cas_fail with "Hc"); [ done | by intros [=] | by left | .. ].
wp_apply (wp_cas_fail with "Hc"); [ eauto | done | by intros [=] | by left | .. ].
iDestruct "Done" as "[_ [Hlghost _]]".
iDestruct "Hlghost" as (?) "Hlghost".
by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost") as %?.
......@@ -734,21 +734,25 @@ Section cond_counter.
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
** (* Pending: contradiction *)
iDestruct "Pending" as "[P >[Hh◯ [Heq' [Hp' Hn●']]]]".
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Pending (wrong proph): contradiction *)
iDestruct "Pending_wp" as "[P >[Hh◯ [Heq' [Hp' Hn●']]]]".
iDestruct "Hp'" as (v) "[Hp' Heq'']". iDestruct "Heq''" as %Heq'.
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Accepted: contradiction *)
iDestruct "Accepted" as "[Q >[Hh◯ [Heq' [Hl_ghost_inv Hp']]]]".
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Accepted (wrong proph): contradiction *)
iDestruct "Accepted_wp" as ">[Hh◯ [Heq' [Hl_ghost_inv Hp']]]".
iDestruct "Hp'" as (v) "[Hp' Heq'']". iDestruct "Heq''" as %Heq'.
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Done : contradiction *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
......
......@@ -16,7 +16,7 @@ Section increment.
Definition incr: val :=
rec: "incr" "l" :=
let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1) NONEV NONEV
if: (cas: "l", "oldv", "oldv" + #1)
then "oldv" (* return old value if success *)
else "incr" "l".
......@@ -30,7 +30,7 @@ Section increment.
iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> AU !> _".
(* Now go on *)
wp_let. wp_op. wp_bind (CAS _ _ _ _ _)%I.
wp_let. wp_op. wp_bind (cas: _, _, _)%E.
wp_apply cas_spec; [done|done|done|iAccu|].
(* Prove the atomic update for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
......
......@@ -202,42 +202,43 @@ Proof.
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_fail s E l q v' e1 v1 e2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e3 v3 IntoVal e4 v4
extract_proph_resolve v4 = Some None
Lemma wp_cas_fail s E l q v' e1 v1 e2 e3 p1 e4 p2 :
IntoVal e1 v1 IntoVal e3 p1 IntoVal e4 p2
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some None
AsVal e2 v' v1 vals_cas_compare_safe v' v1
{{{ l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
iIntros (<- <- <- ? [v2 <-] ?? Φ) ">Hl HΦ".
iIntros (<- <- <- ? ? [v2 <-] ?? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_fail s E l q v' e1 v1 e2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e3 v3 IntoVal e4 v4
extract_proph_resolve v4 = Some None
Lemma twp_cas_fail s E l q v' e1 v1 e2 e3 p1 e4 p2 :
IntoVal e1 v1 IntoVal e3 p1 IntoVal e4 p2
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some None
AsVal e2 v' v1 vals_cas_compare_safe v' v1
[[{ l {q} v' }]] CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
[[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
iIntros (<- <- <- ? [v2 <-] ?? Φ) "Hl HΦ".
iIntros (<- <- <- ? ? [v2 <-] ?? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_fail_proph s E l q v' e1 v1 e2 e3 v3 e4 v4 p v w :
IntoVal e1 v1 IntoVal e3 v3 IntoVal e4 v4
extract_proph_resolve v4 = Some (Some (p, w))
Lemma wp_cas_fail_proph s E l q v' e1 v1 e2 e3 p1 e4 p2 p v w :
IntoVal e1 v1 IntoVal e3 p1 IntoVal e4 p2
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some (Some (p, w))
AsVal e2 v' v1 vals_cas_compare_safe v' v1
{{{ (l {q} v' p v) }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
{{{ RET LitV (LitBool false); l {q} v' v = Some w}}}.
Proof.
iIntros (<- <- <- ? [v2 <-] ?? Φ) "[>Hl >Hp] HΦ".
iIntros (<- <- <- ? ? [v2 <-] ?? Φ) "[>Hl >Hp] HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
......@@ -252,14 +253,15 @@ Proof.
- iApply "HΦ". iFrame. iPureIntro. by eapply first_resolve_eq.
Qed.
Lemma wp_cas_suc s E l e1 v1 e2 v2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 v3 IntoVal e4 v4
Lemma wp_cas_suc s E l e1 v1 e2 v2 e3 p1 e4 p2 :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 p1 IntoVal e4 p2
vals_cas_compare_safe v1 v1
extract_proph_resolve v3 = Some None
extract_proph_resolve p1 = Some None
is_Some (extract_proph_resolve p2)
{{{ l v1 }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (<- <- <- <- ? ? Φ) ">Hl HΦ".
iIntros (<- <- <- <- ? ? ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
......@@ -269,14 +271,15 @@ Proof.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_suc s E l e1 v1 e2 v2 e3 v3 e4 v4 :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 v3 IntoVal e4 v4
Lemma twp_cas_suc s E l e1 v1 e2 v2 e3 p1 e4 p2 :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 p1 IntoVal e4 p2
vals_cas_compare_safe v1 v1
extract_proph_resolve v3 = Some None
extract_proph_resolve p1 = Some None
is_Some (extract_proph_resolve p2)
[[{ l v1 }]] CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
[[{ RET LitV (LitBool true); l v2 }]].
Proof.
iIntros (<- <- <- <- ? ? Φ) "Hl HΦ".
iIntros (<- <- <- <- ? ? ? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit.
......@@ -286,15 +289,15 @@ Proof.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_suc_proph s E l e1 v1 e2 v2 e3 v3 e4 v4 p v w :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 v3 IntoVal e4 v4
Lemma wp_cas_suc_proph s E l e1 v1 e2 v2 e3 p1 e4 p2 p v w :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e3 p1 IntoVal e4 p2
vals_cas_compare_safe v1 v1
extract_proph_resolve v3 = Some (Some (p, w))
extract_proph_resolve p1 = Some (Some (p, w))
is_Some (extract_proph_resolve p2)
{{{ (l v1 p v) }}} CAS (Lit (LitLoc l)) e1 e2 e3 e4 @ s; E
{{{ RET LitV (LitBool true); l v2 v = Some w}}}.
Proof.
iIntros (<- <- <- <- ? ? Φ) "[>Hl >Hp] HΦ".
iIntros (<- <- <- <- ? ? ? Φ) "[>Hl >Hp] HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
......
This diff is collapsed.
Markdown is supported
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