Commit 36e49993 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

minor fixes

parent 9d93a5ed
......@@ -40,7 +40,7 @@ Definition new_rdcss : val :=
complete(l_descr, l_n) :=
let (l_m, m1, n1, n2, p) := !l_descr in
(* data = (l_m, m1, n1, n2, p) *)
let p_ghost = ref #() in
let p_ghost = NewProph in
let n_new = (if !l_m = m1 then n1 else n2) in
Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p p_ghost ; #().
*)
......@@ -210,9 +210,9 @@ Section rdcss.
prove that we will always remain [done]; that's what the one-shot token [γ_s] is for.
- [γ_a] is a token which is owned by the invariant in [pending] and [done] but not in [accepted].
This permits the CAS winner to gain ownership of the token when moving to [accepted] and
it ensures that no other thread can move from [accepted] to [done].
Side remark: One could get rid of this token if one supported fractional ownership to
prophecy resources by only keeping half permission to the prophecy resources
hence ensures that no other thread can move from [accepted] to [done].
Side remark: One could get rid of this token if one supported fractional ownership of
prophecy resources by only keeping half permission to the prophecy resource
in the invariant in [accepted] while the other half would be kept by the CAS winner.
*)
Definition descr_inv P Q (p : proph_id) n (l_n l_descr : loc) (p_ghost_winner : proph_id) γ_n γ_t γ_s γ_a: iProp Σ :=
......@@ -239,7 +239,7 @@ Section rdcss.
[complete] fails always.*)
l_n {1/2} (InjLV n) own γ_n ( Excl' n)
| Updating l_descr l_m m1 n1 n2 p =>
q P Q l_ghost_winner γ_t γ_s γ_a,
q P Q p_ghost_winner γ_t γ_s γ_a,
(* (InjRV #l_descr) = state_to_val (Updating l_descr l_m m1 n1 n2 p) *)
(* There are two pieces of per-[descr]-protocol ghost state:
- [γ_t] is a token owned by whoever created this protocol and used
......@@ -251,7 +251,7 @@ Section rdcss.
be the [l_descr] of any [descr] protocol in the [done] state. *)
val_is_unboxed m1
l_descr {1/2 + q} (#l_m, m1, n1, n2, #p)%V
inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_winner γ_n γ_t γ_s γ_a)
inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost_winner γ_n γ_t γ_s γ_a)
pau P Q γ_n l_m m1 n1 n2 is_gc_loc l_m
end)%I.
......@@ -284,8 +284,8 @@ Section rdcss.
(** Once a [descr] protocol is [done] (as reflected by the [γ_s] token here),
we can at any later point in time extract the [Q]. *)
Lemma state_done_extract_Q P Q p n l_n l_descr l_ghost γ_n γ_t γ_s γ_a :
inv descrN (descr_inv P Q p n l_n l_descr l_ghost γ_n γ_t γ_s γ_a) -
Lemma state_done_extract_Q P Q p n l_n l_descr p_ghost γ_n γ_t γ_s γ_a :
inv descrN (descr_inv P Q p n l_n l_descr p_ghost γ_n γ_t γ_s γ_a) -
own γ_s (Cinr (to_agree ())) -
(own_token γ_t ={}= (Q n)).
Proof.
......@@ -337,7 +337,7 @@ Section rdcss.
{ simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
simpl.
iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
iDestruct "Hrest" as (q P' Q' p_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
(* We perform the CAS. *)
iCombine "Hln Hln'" as "Hln".
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
......@@ -398,7 +398,7 @@ Section rdcss.
of the [rdcss] instance? Impossible, now we will own more than the whole descriptor location! *)
iDestruct "Done" as "(_ & _ & >Hld & _)".
iDestruct "Hld" as (v') "Hld".
iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s' γ_a') "(_ & >[Hld' Hld''] & Hrest)".
iDestruct "Hrest" as (q P' Q' p_ghost' γ_t' γ_s' γ_a') "(_ & >[Hld' Hld''] & Hrest)".
iDestruct (mapsto_combine with "Hld Hld'") as "[Hld _]".
rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
+ (* l_descr' ≠ l_descr: The CAS fails. *)
......@@ -571,7 +571,7 @@ Section rdcss.
wp_cmpxchg_fail.
iModIntro.
(* extract descr invariant *)
iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s γ_a) "(#Hm1'_unbox & [Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
iDestruct "Hrest" as (q P Q p_ghost γ_t γ_s γ_a) "(#Hm1'_unbox & [Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
iDestruct "Hm1'_unbox" as %Hm1'_unbox.
iSplitR "AU Hld2 Hld Hp'".
(* close invariant, retain some permission to l_descr', so it can be read later *)
......@@ -625,7 +625,7 @@ Section rdcss.
iNext. iExists (Quiescent au_n). iFrame.
}
wp_match. iApply "HΦ".
- iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s γ_a) "(#Hm1_unbox & [Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
- iDestruct "Hrest" as (q P Q p_ghost γ_t γ_s γ_a) "(#Hm1_unbox & [Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
iDestruct "Hm1_unbox" as %Hm1_unbox.
iModIntro. iSplitR "AU Hld'". {
iNext. iExists (Updating l_descr lm m1 n1 n2 p). eauto 13 with iFrame.
......
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