Commit 8088d25f authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

minor changes as discussed in MR 24

parent f05c22b2
Pipeline #18179 failed with stage
......@@ -103,7 +103,7 @@ Definition rdcss: val :=
let: "r" := CmpXchg "l_n" (InjL "n1") (InjR "l_descr") in
match: Fst "r" with
InjL "n" =>
(* non-descriptor value read, check if CAS was successful *)
(* non-descriptor value read, check if CmpXchg was successful *)
if: Snd "r" then
(* CmpXchg was successful, finish operation *)
complete "l_descr" "l_n" ;; "n1"
......@@ -162,10 +162,10 @@ Section rdcss.
(** Definition of the invariant *)
Fixpoint val_to_some_loc (pvs : list (val * val)) : option proph_id :=
Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with
| ((_, #true)%V, LitV (LitProphecy p)) :: _ => Some p
| _ :: vs => val_to_some_loc vs
| _ :: vs => proph_extract_winner vs
| _ => None
end.
......@@ -182,26 +182,31 @@ Section rdcss.
Definition own_token γ := (own γ (Excl ()))%I.
Definition pending_state P (n1 : val) (proph_winner : option proph_id) p_ghost_winner (γ_n γ_a: gname) :=
(P match proph_winner with None => True | Some p => p = p_ghost_winner end
own γ_n ( Excl' n1)
own_token γ_a)%I.
(P
match proph_winner with None => True | Some p => p = p_ghost_winner end
own γ_n ( Excl' n1)
own_token γ_a)%I.
(* After the prophecy said we are going to win the race, we commit and run the AU,
switching from [pending] to [accepted]. *)
Definition accepted_state Q (proph_winner : option proph_id) (p_ghost_winner : proph_id) :=
(( vs, (proph p_ghost_winner vs)) match proph_winner with None => True | Some p => p = p_ghost_winner Q end)%I.
(( vs, proph p_ghost_winner vs)
match proph_winner with
None => True
| Some p => p = p_ghost_winner Q
end)%I.
(* The same thread then wins the CAS and moves from [accepted] to [done].
(* The same thread then wins the CmpXchg and moves from [accepted] to [done].
Then, the [γ_t] token guards the transition to take out [Q].
Remember that the thread winning the CAS might be just helping. The token
Remember that the thread winning the CmpXchg might be just helping. The token
is owned by the thread whose request this is.
In this state, [p_ghost_winner] serves as a token to make sure that
only the CAS winner can transition to here, and owning half of [l_descr] serves as a
only the CmpXchg winner can transition to here, and owning half of [l_descr] serves as a
"location" token to ensure there is no ABA going on. Notice how [rdcss_inv]
owns *more than* half of its [l_descr] in the Updating state,
which means we know that the [l_descr] there and here cannot be the same. *)
Definition done_state Qn (l_descr : loc) (p_ghost_winner : proph_id) (γ_t γ_a: gname) :=
((Qn own_token γ_t) ( vs, (proph p_ghost_winner vs)) (l_descr {1/2} -) own_token γ_a)%I.
((Qn own_token γ_t) ( vs, proph p_ghost_winner vs) (l_descr {1/2} -) own_token γ_a)%I.
(* Invariant expressing the descriptor protocol.
- We always need the [proph] in here so that failing threads coming late can
......@@ -209,17 +214,17 @@ Section rdcss.
- We need a way for anyone who has observed the [done] state to
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
This permits the CmpXchg winner to gain ownership of the token when moving to [accepted] and
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.
in the invariant in [accepted] while the other half would be kept by the CmpXchg 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 Σ :=
( vs, proph p vs
(own γ_s (Cinl $ Excl ())
(l_n {1/2} InjRV #l_descr ( pending_state P n (val_to_some_loc vs) p_ghost_winner γ_n γ_a
accepted_state (Q n) (val_to_some_loc vs) p_ghost_winner ))
(l_n {1/2} InjRV #l_descr ( pending_state P n (proph_extract_winner vs) p_ghost_winner γ_n γ_a
accepted_state (Q n) (proph_extract_winner vs) p_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q n) l_descr p_ghost_winner γ_t γ_a))%I.
Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv.
......@@ -235,7 +240,7 @@ Section rdcss.
match s with
| Quiescent n =>
(* (InjLV #n) = state_to_val (Quiescent n) *)
(* In this state the CAS which expects to read (InjRV _) in
(* In this state the CmpXchg which expects to read (InjRV _) in
[complete] fails always.*)
l_n {1/2} (InjLV n) own γ_n ( Excl' n)
| Updating l_descr l_m m1 n1 n2 p =>
......@@ -245,7 +250,7 @@ Section rdcss.
- [γ_t] is a token owned by whoever created this protocol and used
to get out the [Q] in the end.
- [γ_s] reflects whether the protocol is [done] yet or not.
- [γ_a] is a token which is used to ensure that only the CAS winner
- [γ_a] is a token which is used to ensure that only the CmpXchg winner
can move from the [accepted] to the [done] state. *)
(* We own *more than* half of [l_descr], which shows that this cannot
be the [l_descr] of any [descr] protocol in the [done] state. *)
......@@ -324,11 +329,9 @@ Section rdcss.
by iDestruct (own_valid_2 with "Token_a Token_a'") as %?.
}
iDestruct "NotDone" as "(>Hs & >Hln' & [Pending | Accepted])".
{ (* We also cannot be [Pending] any more we have [own γ_n] showing that this
transition has happened *)
iDestruct "Pending" as "[_ >(_ & Hn●' &_)]".
iCombine "Hn●" "Hn●'" as "Contra".
iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
{ (* We also cannot be [Pending] any more because we own the [γ_a] token. *)
iDestruct "Pending" as "[_ >(_ & _ & Token_a')]".
by iDestruct (own_valid_2 with "Token_a Token_a'") as %?.
}
(* So, we are [Accepted]. Now we can show that (InjRV l_descr) = (state_to_val s), because
while a [descr] protocol is not [done], it owns enough of
......@@ -338,7 +341,7 @@ Section rdcss.
iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
simpl.
iDestruct "Hrest" as (q P' Q' p_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
(* We perform the CAS. *)
(* We perform the CmpXchg. *)
iCombine "Hln Hln'" as "Hln".
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
iIntros (vs'' ->) "Hp'". simpl.
......@@ -369,7 +372,7 @@ Section rdcss.
iInv rdcssN as (s) "(>Hln & Hrest)".
iInv descrN as (vs) "(>Hp & [NotDone | [#Hs Done]])".
{ (* [descr] protocol is not done yet: we can show that it
is the active protocol still (l = l'). But then the CAS would
is the active protocol still (l = l'). But then the CmpXchg would
succeed, and our prophecy would have told us that.
So here we can prove that the prophecy was wrong. *)
iDestruct "NotDone" as "(_ & >Hln' & State)".
......@@ -384,7 +387,7 @@ Section rdcss.
(* So, we know our protocol is [Done]. *)
(* It must be that (state_to_val s) ≠ (InjRV l_descr) because we are in the failing thread. *)
destruct s as [n' | l_descr' l_m' m1' n1' n2' p'].
- (* (injL n) is the current value, hence the CAS fails *)
- (* (injL n) is the current value, hence the CmpXchg fails *)
(* FIXME: proof duplication *)
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros (vs'' ->) "Hp". iModIntro.
......@@ -401,10 +404,11 @@ Section rdcss.
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. *)
+ (* l_descr' ≠ l_descr: The CmpXchg fails. *)
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros (vs'' ->) "Hp". iModIntro.
iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
iSplitL "Done Hp". { by eauto 12 with iFrame. }
iModIntro.
iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
......@@ -464,7 +468,7 @@ Section rdcss.
iModIntro. iSplitL "Q Hp_ghost Hp Hvs Hs Hln'".
{ iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
iRight. iSplitL "Hp_ghost"; first by iExists _.
destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
destruct (proph_extract_winner vs) eqn:Hvts; iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Token_a HQ Hn●".
{ by eauto 12 with iFrame. }
......@@ -519,14 +523,14 @@ Section rdcss.
(* invoke inner recursive function [rdcss_inner] *)
iLöb as "IH".
wp_bind (CmpXchg _ _ _)%E.
(* open outer invariant for the CAS *)
(* open outer invariant for the CmpXchg *)
iInv rdcssN as (s) "(>Hln & Hrest)".
destruct s as [n | l_descr' l_m' m1' n1' n2' p'].
- (* l_n ↦ injL n *)
(* a non-value descriptor n is currently stored at l_n *)
iDestruct "Hrest" as ">[Hln' Hn●]".
destruct (decide (n1 = n)) as [-> | Hneq].
+ (* values match -> CAS is successful *)
+ (* values match -> CmpXchg is successful *)
iCombine "Hln Hln'" as "Hln".
wp_cmpxchg_suc.
(* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
......@@ -539,22 +543,22 @@ Section rdcss.
iMod (own_alloc (Excl ())) as (γ_a) "Token_a"; first done.
iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
iDestruct "Hln" as "[Hln Hln']".
set (winner := default p (val_to_some_loc proph_values)).
set (winner := default p (proph_extract_winner proph_values)).
iMod (inv_alloc descrN _ (descr_inv AU_later _ _ _ _ _ winner _ _ _ _)
with "[AU Hs Hp Hln' Hn● Token_a]") as "#Hinv".
{
iNext. iExists _. iFrame "Hp". iLeft. iFrame. iLeft.
iFrame. destruct (val_to_some_loc proph_values); simpl; done.
iFrame. destruct (proph_extract_winner proph_values); simpl; done.
}
iModIntro. iDestruct "Hld" as "[Hld1 [Hld2 Hld3]]". iSplitR "Hld2 Token_t".
{ (* close outer invariant *)
iNext. iCombine "Hld1 Hld3" as "Hld1". iExists (Updating l_descr l_m m1 n n2 p).
eauto 13 with iFrame.
eauto 15 with iFrame.
}
wp_pures.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]");[ done..|].
iIntros "Ht". iMod ("Ht" with "Token_t") as "Φ". by wp_seq.
+ (* values do not match -> CAS fails
+ (* values do not match -> CmpXchg fails
we can commit here *)
wp_cmpxchg_fail.
iMod "AU" as (m'' n'') "[[Hm◯ Hn◯] [_ Hclose]]"; simpl.
......@@ -566,7 +570,7 @@ Section rdcss.
{ iModIntro. iExists (Quiescent n''). iFrame. }
wp_pures. iFrame.
- (* l_n ↦ injR l_ndescr' *)
(* a descriptor l_descr' is currently stored at l_n -> CAS fails
(* a descriptor l_descr' is currently stored at l_n -> CmpXchg fails
try to help the on-going operation *)
wp_cmpxchg_fail.
iModIntro.
......@@ -575,7 +579,7 @@ Section rdcss.
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 *)
{ iModIntro. iExists (Updating l_descr' l_m' m1' n1' n2' p'). eauto 13 with iFrame. }
{ iModIntro. iExists (Updating l_descr' l_m' m1' n1' n2' p'). eauto 15 with iFrame. }
wp_pures.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]"); [done..|].
iIntros "_". wp_seq. wp_pures.
......@@ -628,7 +632,7 @@ Section rdcss.
- 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 l_m m1 n1 n2 p). eauto 13 with iFrame.
iNext. iExists (Updating l_descr l_m m1 n1 n2 p). eauto 15 with iFrame.
}
wp_match.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld']"); [done..|].
......
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