Commit 06e599ed authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

name change: state protocol to descr protocol

parent 19e774cb
......@@ -140,7 +140,7 @@ Section rdcss.
Context {Σ} `{!heapG Σ, !rdcssG Σ, !gcG Σ }.
Context (N : namespace).
Local Definition stateN := N .@ "state".
Local Definition descrN := N .@ "descr".
Local Definition rdcssN := N .@ "rdcss".
(** Updating and synchronizing the number RAs *)
......@@ -202,11 +202,12 @@ Section rdcss.
Definition done_state Qn (l_descr l_ghost_winner : loc) (γ_t : gname) :=
((Qn own_token γ_t) l_ghost_winner - (l_descr {1/2} -) )%I.
(* We always need the [proph] in here so that failing threads coming late can
(* Invariant expressing the descriptor protocol.
We always need the [proph] in here so that failing threads coming late can
always resolve their stuff.
Moreover, 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. *)
Definition state_inv P Q (p : proph_id) n (l_n l_descr l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
Definition descr_inv P Q (p : proph_id) n (l_n l_descr l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
( vs, proph p vs
(own γ_s (Cinl $ Excl ())
(l_n {1/2} InjRV #l_descr ( pending_state P n (val_to_some_loc l_descr vs) l_ghost_winner γ_n
......@@ -228,14 +229,14 @@ Section rdcss.
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,
(* There are two pieces of per-[state]-protocol ghost state:
(* There are two pieces of per-[descr]-protocol ghost state:
- [γ_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. *)
(* We own *more than* half of [l_descr], which shows that this cannot
be the [l_descr] of any [state] protocol in the [done] state. *)
be the [l_descr] of any [descr] protocol in the [done] state. *)
l_descr {1/2 + q} (#l_m, #m1, #n1, #n2, #p)%V
inv stateN (state_inv P Q p n1 l_n l_descr l_ghost_winner γ_n γ_t γ_s)
inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_winner γ_n γ_t γ_s)
pau P Q γ_n l_m m1 n1 n2 is_gc_loc l_m
end)%I.
......@@ -269,12 +270,12 @@ Section rdcss.
(** Once a [state] 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 :
inv stateN (state_inv P Q p n l_n l_descr l_ghost γ_n γ_t γ_s) -
inv descrN (descr_inv P Q p n l_n l_descr l_ghost γ_n γ_t γ_s) -
own γ_s (Cinr (to_agree ())) -
(own_token γ_t ={}= (Q #n)).
Proof.
iIntros "#Hinv #Hs !# Ht".
iInv stateN as (vs) "(Hp & [NotDone | Done])".
iInv descrN as (vs) "(Hp & [NotDone | Done])".
* (* Moved back to NotDone: contradiction. *)
iDestruct "NotDone" as "(>Hs' & _ & _)".
iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
......@@ -282,7 +283,7 @@ Section rdcss.
iDestruct "QT" as "[Qn | >T]"; last first.
{ iDestruct (own_valid_2 with "Ht T") as %Contra.
by inversion Contra. }
iSplitR "Qn"; last done. iIntros "!> !>". unfold state_inv.
iSplitR "Qn"; last done. iIntros "!> !>". unfold descr_inv.
iExists _. iFrame "Hp". iRight.
unfold done_state. iFrame "#∗".
Qed.
......@@ -293,7 +294,7 @@ Section rdcss.
Lemma complete_succeeding_thread_pending (γ_n γ_t γ_s : gname) l_m l_n P Q p
(m1 n1 n2 n : Z) (l_descr l_ghost : loc) Φ :
inv rdcssN (rdcss_inv γ_n l_n) -
inv stateN (state_inv P Q p n1 l_n l_descr l_ghost γ_n γ_t γ_s) -
inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost γ_n γ_t γ_s) -
pau P Q γ_n l_m m1 n1 n2 -
l_ghost {1 / 2} #() -
((own_token γ_t ={}= (Q #n1)) - Φ #()) -
......@@ -303,7 +304,7 @@ Section rdcss.
Proof.
iIntros "#InvC #InvS PAU Hl_ghost HQ Hn●". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
iInv stateN as (vs) "(>Hp & [NotDone | Done])"; last first.
iInv descrN as (vs) "(>Hp & [NotDone | Done])"; last first.
{ (* We cannot be [done] yet, as we own the "ghost location" that serves
as token for that transition. *)
iDestruct "Done" as "(_ & _ & Hlghost & _)".
......@@ -318,7 +319,7 @@ Section rdcss.
iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
}
(* So, we are [Accepted]. Now we can show that (InjRV l_descr) = (state_to_val s), because
while a [state] protocol is not [done], it owns enough of
while a [descr] protocol is not [done], it owns enough of
the [rdcss] protocol to ensure that does not move anywhere else. *)
destruct s as [n' |ld' lm' m1' n1' n2' p'].
{ simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
......@@ -349,7 +350,7 @@ Section rdcss.
Lemma complete_failing_thread γ_n γ_t γ_s l_m l_n l_descr P Q p m1 n1 n2 n l_ghost_inv l_ghost Φ :
l_ghost_inv l_ghost
inv rdcssN (rdcss_inv γ_n l_n) -
inv stateN (state_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -
inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -
pau P Q γ_n l_m m1 n1 n2 -
((own_token γ_t ={}= (Q #n1)) - Φ #()) -
......@@ -357,8 +358,8 @@ Section rdcss.
Proof.
iIntros (Hnl) "#InvC #InvS PAU HQ". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
iInv stateN as (vs) "(>Hp & [NotDone | [#Hs Done]])".
{ (* If the [state] protocol is not done yet, we can show that it
iInv descrN as (vs) "(>Hp & [NotDone | [#Hs Done]])".
{ (* If the [descr] protocol is not done yet, we can show that it
is the active protocol still (l = l'). But then the CAS would
succeed, and our prophecy would have told us that.
So here we can prove that the prophecy was wrong. *)
......@@ -384,7 +385,7 @@ Section rdcss.
}
(* (injR l_descr') is the current value *)
destruct (decide (l_descr' = l_descr)) as [->|Hn]. {
(* The [state] protocol is [done] while still being the active protocol
(* The [descr] protocol is [done] while still being the active protocol
of the [rdcss] instance? Impossible, now we will own more than the whole descriptor location! *)
iDestruct "Done" as "(_ & _ & >Hld)".
iDestruct "Hld" as (v') "Hld".
......@@ -409,7 +410,7 @@ Section rdcss.
Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : Z) (p : proph_id) γ_n γ_t γ_s l_ghost_inv P Q q:
N ## gcN
inv rdcssN (rdcss_inv γ_n l_n) -
inv stateN (state_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -
inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -
pau P Q γ_n l_m m1 n1 n2 -
is_gc_loc l_m -
gc_inv -
......@@ -428,7 +429,7 @@ Section rdcss.
destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
- (* we are the succeeding thread *)
(* we need to move from [pending] to [accepted]. *)
iInv stateN as (vs) "(>Hp & [(>Hs & >Hln' & [Pending | Accepted]) | [#Hs Done]])".
iInv descrN as (vs) "(>Hp & [(>Hs & >Hln' & [Pending | Accepted]) | [#Hs Done]])".
+ (* Pending: update to accepted *)
iDestruct "Pending" as "[P >[Hvs Hn●]]".
iDestruct ("PAU" with "P") as ">AU".
......@@ -449,7 +450,7 @@ Section rdcss.
(* give back access to A location *)
iMod ("Hclose" with "[Hn◯ Hgc_lm]") as "Q"; first by iFrame.
iModIntro. iMod "Hgc_close" as "_".
(* close state inv *)
(* close descr inv *)
iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hln'".
{ iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
iRight. iSplitL "Hl_ghost'"; first by iExists _.
......@@ -520,13 +521,13 @@ Section rdcss.
+ (* values match -> CAS is successful *)
iCombine "Hln Hln'" as "Hln".
wp_cas_suc.
(* Initialize new [state] protocol .*)
(* Initialize new [descr] protocol .*)
iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
iDestruct "Hln" as "[Hln Hln']".
set (winner := default l_descr (val_to_some_loc l_descr proph_values)).
iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ winner _ _ _)
iMod (inv_alloc descrN _ (descr_inv AU_later _ _ _ _ _ winner _ _ _)
with "[AU Hs Hp' Hln' Hn●]") as "#Hinv".
{
iNext. iExists _. iFrame "Hp'". iLeft. iFrame. iLeft.
......@@ -558,7 +559,7 @@ Section rdcss.
try to help the on-going operation *)
wp_cas_fail.
iModIntro.
(* extract state invariant *)
(* extract descr invariant *)
iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
iSplitR "AU Hld2 Hld Hp'".
(* close invariant, retain some permission to l_descr', so it can be read later *)
......
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