Skip to content
Snippets Groups Projects
Commit 7a4c79a9 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy
Browse files

made clearer that the ghost prophecy is a thread id and adjusted some comments

parent 17e193a3
No related branches found
No related tags found
1 merge request!26Continuation change, extract_proph_winner change
This commit is part of merge request !26. Comments created here will be created in the context of that merge request.
Hide whitespace changes
Inline Side-by-side
theories/logatom/rdcss/rdcss.v
+ 49
− 44
View file @ 7a4c79a9
......@@ -34,9 +34,9 @@ Definition new_rdcss : val := λ: "n", ref (InjL "n").
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 = NewProph in
let tid_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 ; #().
Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p tid_ghost ; #().
*)
Definition complete : val :=
λ: "l_descr" "l_n",
......@@ -47,9 +47,14 @@ Definition complete : val :=
let: "n1" := Snd (Fst (Fst ("data"))) in
let: "n2" := Snd (Fst ("data")) in
let: "p" := Snd ("data") in
let: "p_ghost" := NewProph in
(* Create a thread identifier using NewProph.
tid_ghost is not used as a traditional prophecy, i.e. it is never resolved.
The reason we use NewProph is so that we can use the erasure theorem to argue that
it has no effect on the code.
*)
let: "tid_ghost" := NewProph in
let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "p_ghost" ;; #().
Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "tid_ghost" ;; #().
(*
get(l_n) :=
......@@ -158,7 +163,7 @@ Section rdcss.
Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with
| ((_, #true)%V, LitV (LitProphecy p)) :: _ => Some p
| ((_, #true)%V, LitV (LitProphecy tid)) :: _ => Some tid
| _ => None
end.
......@@ -174,30 +179,30 @@ 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) :=
Definition pending_state P (n1 : val) (proph_winner : option proph_id) tid_ghost_winner (γ_n γ_a: gname) :=
(P ∗
⌜match proph_winner with None => True | Some p => p = p_ghost_winner end⌝ ∗
⌜match proph_winner with None => True | Some p => p = tid_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) ∗
Definition accepted_state Q (proph_winner : option proph_id) (tid_ghost_winner : proph_id) :=
((∃ vs, proph tid_ghost_winner vs) ∗
Q ∗
⌜match proph_winner with None => True | Some p => p = p_ghost_winner end⌝)%I.
⌜match proph_winner with None => True | Some tid => tid = tid_ghost_winner end⌝)%I.
(* 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 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
In this state, [tid_ghost_winner] serves as a token to make sure that
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.
Definition done_state Qn (l_descr : loc) (tid_ghost_winner : proph_id) (γ_t γ_a: gname) :=
((Qn ∨ own_token γ_t) ∗ (∃ vs, proph tid_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
......@@ -211,12 +216,12 @@ Section rdcss.
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 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 Σ :=
Definition descr_inv P Q (p : proph_id) n (l_n l_descr : loc) (tid_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 (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.
(l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (proph_extract_winner vs) tid_ghost_winner γ_n γ_a
∨ accepted_state (Q n) (proph_extract_winner vs) tid_ghost_winner ))
∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q n) l_descr tid_ghost_winner γ_t γ_a))%I.
Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv.
......@@ -235,9 +240,9 @@ 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 p_ghost_winner γ_t γ_s γ_a,
∃ q P Q tid_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:
(* There are three 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.
......@@ -247,7 +252,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 p_ghost_winner γ_n γ_t γ_s γ_a) ∗
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_winner γ_n γ_t γ_s γ_a) ∗
□ pau P Q γ_n l_m m1 n1 n2 ∗ is_gc_loc l_m
end)%I.
......@@ -280,8 +285,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 p_ghost γ_n γ_t γ_s γ_a :
inv descrN (descr_inv P Q p n l_n l_descr p_ghost γ_n γ_t γ_s γ_a) -∗
Lemma state_done_extract_Q P Q p n l_n l_descr tid_ghost γ_n γ_t γ_s γ_a :
inv descrN (descr_inv P Q p n l_n l_descr tid_ghost γ_n γ_t γ_s γ_a) -∗
own γ_s (Cinr (to_agree ())) -∗
□(own_token γ_t ={⊤}=∗ ▷ (Q n)).
Proof.
......@@ -303,13 +308,13 @@ Section rdcss.
(** The part of [complete] for the succeeding thread that moves from [accepted] to [done] state *)
Lemma complete_succeeding_thread_pending (γ_n γ_t γ_s γ_a: gname) l_n P Q p
(n1 n : val) (l_descr : loc) (p_ghost : proph_id) Φ :
(n1 n : val) (l_descr : loc) (tid_ghost : proph_id) Φ :
inv rdcssN (rdcss_inv γ_n l_n) -∗
inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost γ_n γ_t γ_s γ_a) -∗
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost γ_n γ_t γ_s γ_a) -∗
own_token γ_a -∗
(□(own_token γ_t ={⊤}=∗ ▷ (Q n1)) -∗ Φ #()) -∗
own γ_n (● Excl' n) -∗
WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #p_ghost ;; #() {{ v, Φ v }}.
WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #tid_ghost ;; #() {{ v, Φ v }}.
Proof.
iIntros "#InvC #InvS Token_a HQ Hn●". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
......@@ -331,7 +336,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' p_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
iDestruct "Hrest" as (q P' Q' tid_ghost' γ_t' γ_s' γ_a') "(_ & [>Hld >Hld'] & Hrest)".
(* We perform the CmpXchg. *)
iCombine "Hln Hln'" as "Hln".
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
......@@ -352,12 +357,12 @@ Section rdcss.
Qed.
(** The part of [complete] for the failing thread *)
Lemma complete_failing_thread γ_n γ_t γ_s γ_a l_n l_descr P Q p n1 n p_ghost_inv p_ghost Φ :
p_ghost_inv ≠ p_ghost →
Lemma complete_failing_thread γ_n γ_t γ_s γ_a l_n l_descr P Q p n1 n tid_ghost_inv tid_ghost Φ :
tid_ghost_inv ≠ tid_ghost →
inv rdcssN (rdcss_inv γ_n l_n) -∗
inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost_inv γ_n γ_t γ_s γ_a) -∗
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_inv γ_n γ_t γ_s γ_a) -∗
(□(own_token γ_t ={⊤}=∗ ▷ (Q n1)) -∗ Φ #()) -∗
WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #p_ghost ;; #() {{ v, Φ v }}.
WP Resolve (CmpXchg #l_n (InjRV #l_descr) (InjLV n)) #p #tid_ghost ;; #() {{ v, Φ v }}.
Proof.
iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
......@@ -393,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' p_ghost' γ_t' γ_s' γ_a') "(_ & >[Hld' Hld''] & Hrest)".
iDestruct "Hrest" as (q P' Q' tid_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 CmpXchg fails. *)
......@@ -411,11 +416,11 @@ Section rdcss.
this request, then you get [Q]. But we also try to complete other
thread's requests, which is why we cannot ask for the token
as a precondition. *)
Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : val) (p : proph_id) γ_n γ_t γ_s γ_a p_ghost_inv P Q q:
Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : val) (p : proph_id) γ_n γ_t γ_s γ_a tid_ghost_inv P Q q:
val_is_unboxed m1 →
N ## gcN →
inv rdcssN (rdcss_inv γ_n l_n) -∗
inv descrN (descr_inv P Q p n1 l_n l_descr p_ghost_inv γ_n γ_t γ_s γ_a) -∗
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_inv γ_n γ_t γ_s γ_a) -∗
□ pau P Q γ_n l_m m1 n1 n2 -∗
is_gc_loc l_m -∗
gc_inv -∗
......@@ -427,12 +432,12 @@ Section rdcss.
iModIntro. iIntros (Φ) "Hld HQ". wp_lam. wp_let.
wp_bind (! _)%E. wp_load. iClear "Hld". wp_pures.
wp_apply wp_new_proph; first done.
iIntros (vs_ghost p_ghost) "Hp_ghost". wp_pures.
iIntros (vs_ghost tid_ghost) "Htid_ghost". wp_pures.
wp_bind (! _)%E.
(* open outer invariant *)
iInv rdcssN as (s) "(>Hln & Hrest)"=>//.
(* two different proofs depending on whether we are succeeding thread *)
destruct (decide (p_ghost_inv = p_ghost)) as [-> | Hnl].
destruct (decide (tid_ghost_inv = tid_ghost)) as [-> | Hnl].
- (* we are the succeeding thread *)
(* we need to move from [pending] to [accepted]. *)
iInv descrN as (vs) "(>Hp & [(>Hs & >Hln' & [Pending | Accepted]) | [#Hs Done]])".
......@@ -457,7 +462,7 @@ Section rdcss.
iMod ("Hclose" with "[Hn◯ Hgc_lm]") as "Q"; first by iFrame.
iModIntro. iMod "Hgc_close" as "_".
(* close descr inv *)
iModIntro. iSplitL "Q Hp_ghost Hp Hvs Hs Hln'".
iModIntro. iSplitL "Q Htid_ghost Hp Hvs Hs Hln'".
{ iModIntro. iNext. iExists _. iFrame "Hp". eauto 12 with iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Token_a HQ Hn●".
......@@ -470,13 +475,13 @@ Section rdcss.
iApply (complete_succeeding_thread_pending
with "InvC InvS Token_a HQ Hn●").
+ (* Accepted: contradiction *)
iDestruct "Accepted" as "[>Hp_ghost_inv _]".
iDestruct "Hp_ghost_inv" as (p') "Hp_ghost_inv".
by iDestruct (proph_exclusive with "Hp_ghost Hp_ghost_inv") as %?.
iDestruct "Accepted" as "[>Htid_ghost_inv _]".
iDestruct "Htid_ghost_inv" as (p') "Htid_ghost_inv".
by iDestruct (proph_exclusive with "Htid_ghost Htid_ghost_inv") as %?.
+ (* Done: contradiction *)
iDestruct "Done" as "[QT >[Hp_ghost_inv _]]".
iDestruct "Hp_ghost_inv" as (p') "Hp_ghost_inv".
by iDestruct (proph_exclusive with "Hp_ghost Hp_ghost_inv") as %?.
iDestruct "Done" as "[QT >[Htid_ghost_inv _]]".
iDestruct "Htid_ghost_inv" as (p') "Htid_ghost_inv".
by iDestruct (proph_exclusive with "Htid_ghost Htid_ghost_inv") as %?.
- (* we are the failing thread *)
(* close invariant *)
iMod (is_gc_access with "InvGC isGC") as (v) "[Hlm Hclose]"; first solve_ndisj.
......@@ -565,7 +570,7 @@ Section rdcss.
wp_cmpxchg_fail.
iModIntro.
(* extract descr invariant *)
iDestruct "Hrest" as (q P Q p_ghost γ_t γ_s γ_a) "(#Hm1'_unbox & [Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
iDestruct "Hrest" as (q P Q tid_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 *)
......@@ -618,7 +623,7 @@ Section rdcss.
iNext. iExists (Quiescent au_n). iFrame.
}
wp_match. iApply "HΦ".
- iDestruct "Hrest" as (q P Q p_ghost γ_t γ_s γ_a) "(#Hm1_unbox & [Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
- iDestruct "Hrest" as (q P Q tid_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 15 with iFrame.
......
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