From 8088d25fbb3dbf3f143775ea0016c3fb7a08a6bb Mon Sep 17 00:00:00 2001 From: Gaurav Parthasarathy Date: Thu, 4 Jul 2019 11:46:52 +0200 Subject: [PATCH] minor changes as discussed in MR 24 --- theories/logatom/rdcss/rdcss.v | 78 ++++++++++++++++++---------------- 1 file changed, 41 insertions(+), 37 deletions(-) diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v index f3bc9f9..e36d0cb 100644 --- a/theories/logatom/rdcss/rdcss.v +++ b/theories/logatom/rdcss/rdcss.v @@ -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..|]. -- GitLab