Skip to content
Snippets Groups Projects
Commit a58a15e2 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' into 'master' 

Continuation change, extract_proph_winner change

See merge request !26
parents 77e03801 84a26b18
No related branches found
No related tags found
1 merge request!26Continuation change, extract_proph_winner change
Pipeline #18332 passed
Hide whitespace changes
Inline Side-by-side
theories/logatom/rdcss/rdcss.v
+ 64
− 65
View file @ a58a15e2
...@@ -13,18 +13,16 @@ Set Default Proof Using "Type". ...@@ -13,18 +13,16 @@ Set Default Proof Using "Type".
(** * Implementation of the functions. *) (** * Implementation of the functions. *)
(* 1) l_m corresponds to the A location in the paper and can differ when helping another thread (* 1) The M location l_m can differ when helping another thread in the same RDCSS instance
in the same RDCSS instance. (Harris et al. refer to it as a location in the control section.)
2) l_n corresponds to the B location in the paper and identifies a single RDCSS instance. 2) The N location l_n identifies a single RDCSS instance.
3) Values stored at the B location have type (Harris et al. refer to it as a location in the data section.)
3) There are two kinds of values stored at N locations
Val + Ref (Ref * Val * Val * Val * Proph)
3.1) The value is injL n for some n: no operation is on-going and the logical state is n.
3.1) If the value is injL n, then no operation is on-going and the logical state is n. 3.2) The value is injR l_descr for some location l_descr (which we call a descriptor):
3.2) If the value is injR (Ref (l_m', m1', n1', n2', p)), then an operation is on-going l_descr must point to a tuple (l_m, m1, n1, n2, p) for some M location l_m, values m1, n1, n2 and prophecy p.
with corresponding A location l_m'. The reference pointing to the tuple of values In this case an operation is on-going with corresponding M location l_m.
corresponds to the descriptor in the paper. We use the name l_descr for such a
descriptor reference.
*) *)
(* (*
...@@ -36,9 +34,9 @@ Definition new_rdcss : val := λ: "n", ref (InjL "n"). ...@@ -36,9 +34,9 @@ Definition new_rdcss : val := λ: "n", ref (InjL "n").
complete(l_descr, l_n) := complete(l_descr, l_n) :=
let (l_m, m1, n1, n2, p) := !l_descr in let (l_m, m1, n1, n2, p) := !l_descr in
(* data = (l_m, m1, n1, n2, p) *) (* 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 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 := Definition complete : val :=
λ: "l_descr" "l_n", λ: "l_descr" "l_n",
...@@ -49,9 +47,14 @@ Definition complete : val := ...@@ -49,9 +47,14 @@ Definition complete : val :=
let: "n1" := Snd (Fst (Fst ("data"))) in let: "n1" := Snd (Fst (Fst ("data"))) in
let: "n2" := Snd (Fst ("data")) in let: "n2" := Snd (Fst ("data")) in
let: "p" := Snd ("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 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) := get(l_n) :=
...@@ -158,10 +161,10 @@ Section rdcss. ...@@ -158,10 +161,10 @@ Section rdcss.
(** Definition of the invariant *) (** Definition of the invariant *)
(** Extract the TID of the winner from the prophecy value. The winner is the first thread that performs a CAS. *)
Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id := Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with match pvs with
| ((_, #true)%V, LitV (LitProphecy p)) :: _ => Some p | (_, LitV (LitProphecy tid)) :: _ => Some tid
| _ :: vs => proph_extract_winner vs
| _ => None | _ => None
end. end.
...@@ -177,32 +180,30 @@ Section rdcss. ...@@ -177,32 +180,30 @@ Section rdcss.
Definition own_token γ := (own γ (Excl ()))%I. 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 ∗ (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 γ_n (● Excl' n1) ∗
own_token γ_a)%I. own_token γ_a)%I.
(* After the prophecy said we are going to win the race, we commit and run the AU, (* After the prophecy said we are going to win the race, we commit and run the AU,
switching from [pending] to [accepted]. *) switching from [pending] to [accepted]. *)
Definition accepted_state Q (proph_winner : option proph_id) (p_ghost_winner : proph_id) := Definition accepted_state Q (proph_winner : option proph_id) (tid_ghost_winner : proph_id) :=
((∃ vs, proph p_ghost_winner vs) ∗ ((∃ vs, proph tid_ghost_winner vs) ∗
match proph_winner with Q ∗
None => True ⌜match proph_winner with None => True | Some tid => tid = tid_ghost_winner end⌝)%I.
| Some p => ⌜p = p_ghost_winner⌝ ∗ Q
end)%I.
(* The same thread then wins the CmpXchg 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]. Then, the [γ_t] token guards the transition to take out [Q].
Remember that the thread winning the CmpXchg 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. 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 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] "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, 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. *) 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) := Definition done_state Qn (l_descr : loc) (tid_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 tid_ghost_winner vs) ∗ (l_descr ↦{1/2} -) ∗ own_token γ_a)%I.
(* Invariant expressing the descriptor protocol. (* Invariant expressing the descriptor protocol.
- We always need the [proph] in here so that failing threads coming late can - We always need the [proph] in here so that failing threads coming late can
...@@ -216,12 +217,12 @@ Section rdcss. ...@@ -216,12 +217,12 @@ Section rdcss.
prophecy resources by only keeping half permission to the prophecy resource 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. 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 ∗ (∃ vs, proph p vs ∗
(own γ_s (Cinl $ Excl ()) ∗ (own γ_s (Cinl $ Excl ()) ∗
(l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (proph_extract_winner vs) p_ghost_winner γ_n γ_a (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) p_ghost_winner )) ∨ accepted_state (Q n) (proph_extract_winner vs) tid_ghost_winner ))
∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q n) l_descr p_ghost_winner γ_t γ_a))%I. ∨ 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. Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv.
...@@ -240,9 +241,9 @@ Section rdcss. ...@@ -240,9 +241,9 @@ Section rdcss.
[complete] fails always.*) [complete] fails always.*)
l_n ↦{1/2} (InjLV n) ∗ own γ_n (● Excl' n) l_n ↦{1/2} (InjLV n) ∗ own γ_n (● Excl' n)
| Updating l_descr l_m m1 n1 n2 p => | 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) *) (* (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 - [γ_t] is a token owned by whoever created this protocol and used
to get out the [Q] in the end. to get out the [Q] in the end.
- [γ_s] reflects whether the protocol is [done] yet or not. - [γ_s] reflects whether the protocol is [done] yet or not.
...@@ -252,7 +253,7 @@ Section rdcss. ...@@ -252,7 +253,7 @@ Section rdcss.
be the [l_descr] of any [descr] protocol in the [done] state. *) be the [l_descr] of any [descr] protocol in the [done] state. *)
⌜val_is_unboxed m1⌝ ∗ ⌜val_is_unboxed m1⌝ ∗
l_descr ↦{1/2 + q} (#l_m, m1, n1, n2, #p)%V ∗ 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 □ pau P Q γ_n l_m m1 n1 n2 ∗ is_gc_loc l_m
end)%I. end)%I.
...@@ -285,8 +286,8 @@ Section rdcss. ...@@ -285,8 +286,8 @@ Section rdcss.
(** Once a [descr] protocol is [done] (as reflected by the [γ_s] token here), (** Once a [descr] protocol is [done] (as reflected by the [γ_s] token here),
we can at any later point in time extract the [Q]. *) 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 : 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 p_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 γ_s (Cinr (to_agree ())) -∗
□(own_token γ_t ={⊤}=∗ ▷ (Q n)). □(own_token γ_t ={⊤}=∗ ▷ (Q n)).
Proof. Proof.
...@@ -308,13 +309,13 @@ Section rdcss. ...@@ -308,13 +309,13 @@ Section rdcss.
(** The part of [complete] for the succeeding thread that moves from [accepted] to [done] state *) (** 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 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 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 γ_a -∗
(□(own_token γ_t ={⊤}=∗ ▷ (Q n1)) -∗ Φ #()) -∗ (□(own_token γ_t ={⊤}=∗ ▷ (Q n1)) -∗ Φ #()) -∗
own γ_n (● Excl' n) -∗ 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. Proof.
iIntros "#InvC #InvS Token_a HQ Hn●". wp_bind (Resolve _ _ _)%E. iIntros "#InvC #InvS Token_a HQ Hn●". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)". iInv rdcssN as (s) "(>Hln & Hrest)".
...@@ -336,13 +337,13 @@ Section rdcss. ...@@ -336,13 +337,13 @@ Section rdcss.
{ simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. } { simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
iDestruct (mapsto_agree with "Hln Hln'") as %[= ->]. iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
simpl. 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. *) (* We perform the CmpXchg. *)
iCombine "Hln Hln'" as "Hln". iCombine "Hln Hln'" as "Hln".
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc. wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
iIntros (vs'' ->) "Hp'". simpl. iIntros (vs'' ->) "Hp'". simpl.
(* Update to Done. *) (* Update to Done. *)
iDestruct "Accepted" as "[Hp_phost_inv [HEq Q]]". iDestruct "Accepted" as "[Hp_phost_inv [Q Heq]]".
iMod (own_update with "Hs") as "Hs". iMod (own_update with "Hs") as "Hs".
{ apply (cmra_update_exclusive (Cinr (to_agree ()))). done. } { apply (cmra_update_exclusive (Cinr (to_agree ()))). done. }
iDestruct "Hs" as "#Hs'". iModIntro. iDestruct "Hs" as "#Hs'". iModIntro.
...@@ -357,12 +358,12 @@ Section rdcss. ...@@ -357,12 +358,12 @@ Section rdcss.
Qed. Qed.
(** The part of [complete] for the failing thread *) (** 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 Φ : Lemma complete_failing_thread γ_n γ_t γ_s γ_a l_n l_descr P Q p n1 n tid_ghost_inv tid_ghost Φ :
p_ghost_inv ≠ p_ghost → tid_ghost_inv ≠ tid_ghost →
inv rdcssN (rdcss_inv γ_n l_n) -∗ 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)) -∗ Φ #()) -∗ (□(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. Proof.
iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E. iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)". iInv rdcssN as (s) "(>Hln & Hrest)".
...@@ -378,7 +379,7 @@ Section rdcss. ...@@ -378,7 +379,7 @@ Section rdcss.
iIntros (vs'' ->). simpl. iIntros (vs'' ->). simpl.
iDestruct "State" as "[Pending | Accepted]". iDestruct "State" as "[Pending | Accepted]".
+ iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs. + iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs. + iDestruct "Accepted" as "[_ [_ Hvs]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
} }
(* So, we know our protocol is [Done]. *) (* 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. *) (* It must be that (state_to_val s) ≠ (InjRV l_descr) because we are in the failing thread. *)
...@@ -398,7 +399,7 @@ Section rdcss. ...@@ -398,7 +399,7 @@ Section rdcss.
of the [rdcss] instance? Impossible, now we will own more than the whole descriptor location! *) of the [rdcss] instance? Impossible, now we will own more than the whole descriptor location! *)
iDestruct "Done" as "(_ & _ & >Hld & _)". iDestruct "Done" as "(_ & _ & >Hld & _)".
iDestruct "Hld" as (v') "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 _]". iDestruct (mapsto_combine with "Hld Hld'") as "[Hld _]".
rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]". rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
+ (* l_descr' ≠ l_descr: The CmpXchg fails. *) + (* l_descr' ≠ l_descr: The CmpXchg fails. *)
...@@ -416,11 +417,11 @@ Section rdcss. ...@@ -416,11 +417,11 @@ Section rdcss.
this request, then you get [Q]. But we also try to complete other 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 thread's requests, which is why we cannot ask for the token
as a precondition. *) 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 → val_is_unboxed m1 →
N ## gcN → N ## gcN →
inv rdcssN (rdcss_inv γ_n l_n) -∗ 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 -∗ □ pau P Q γ_n l_m m1 n1 n2 -∗
is_gc_loc l_m -∗ is_gc_loc l_m -∗
gc_inv -∗ gc_inv -∗
...@@ -432,12 +433,12 @@ Section rdcss. ...@@ -432,12 +433,12 @@ Section rdcss.
iModIntro. iIntros (Φ) "Hld HQ". wp_lam. wp_let. iModIntro. iIntros (Φ) "Hld HQ". wp_lam. wp_let.
wp_bind (! _)%E. wp_load. iClear "Hld". wp_pures. wp_bind (! _)%E. wp_load. iClear "Hld". wp_pures.
wp_apply wp_new_proph; first done. 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. wp_bind (! _)%E.
(* open outer invariant *) (* open outer invariant *)
iInv rdcssN as (s) "(>Hln & Hrest)"=>//. iInv rdcssN as (s) "(>Hln & Hrest)"=>//.
(* two different proofs depending on whether we are succeeding thread *) (* 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 are the succeeding thread *)
(* we need to move from [pending] to [accepted]. *) (* we need to move from [pending] to [accepted]. *)
iInv descrN as (vs) "(>Hp & [(>Hs & >Hln' & [Pending | Accepted]) | [#Hs Done]])". iInv descrN as (vs) "(>Hp & [(>Hs & >Hln' & [Pending | Accepted]) | [#Hs Done]])".
...@@ -462,10 +463,8 @@ Section rdcss. ...@@ -462,10 +463,8 @@ Section rdcss.
iMod ("Hclose" with "[Hn◯ Hgc_lm]") as "Q"; first by iFrame. iMod ("Hclose" with "[Hn◯ Hgc_lm]") as "Q"; first by iFrame.
iModIntro. iMod "Hgc_close" as "_". iModIntro. iMod "Hgc_close" as "_".
(* close descr inv *) (* 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". iLeft. iFrame. { iModIntro. iNext. iExists _. iFrame "Hp". eauto 12 with iFrame. }
iRight. iSplitL "Hp_ghost"; first by iExists _.
destruct (proph_extract_winner vs) eqn:Hvts; iFrame. }
(* close outer inv *) (* close outer inv *)
iModIntro. iSplitR "Token_a HQ Hn●". iModIntro. iSplitR "Token_a HQ Hn●".
{ by eauto 12 with iFrame. } { by eauto 12 with iFrame. }
...@@ -477,13 +476,13 @@ Section rdcss. ...@@ -477,13 +476,13 @@ Section rdcss.
iApply (complete_succeeding_thread_pending iApply (complete_succeeding_thread_pending
with "InvC InvS Token_a HQ Hn●"). with "InvC InvS Token_a HQ Hn●").
+ (* Accepted: contradiction *) + (* Accepted: contradiction *)
iDestruct "Accepted" as "[>Hp_ghost_inv _]". iDestruct "Accepted" as "[>Htid_ghost_inv _]".
iDestruct "Hp_ghost_inv" as (p') "Hp_ghost_inv". iDestruct "Htid_ghost_inv" as (p') "Htid_ghost_inv".
by iDestruct (proph_exclusive with "Hp_ghost Hp_ghost_inv") as %?. by iDestruct (proph_exclusive with "Htid_ghost Htid_ghost_inv") as %?.
+ (* Done: contradiction *) + (* Done: contradiction *)
iDestruct "Done" as "[QT >[Hp_ghost_inv _]]". iDestruct "Done" as "[QT >[Htid_ghost_inv _]]".
iDestruct "Hp_ghost_inv" as (p') "Hp_ghost_inv". iDestruct "Htid_ghost_inv" as (p') "Htid_ghost_inv".
by iDestruct (proph_exclusive with "Hp_ghost Hp_ghost_inv") as %?. by iDestruct (proph_exclusive with "Htid_ghost Htid_ghost_inv") as %?.
- (* we are the failing thread *) - (* we are the failing thread *)
(* close invariant *) (* close invariant *)
iMod (is_gc_access with "InvGC isGC") as (v) "[Hlm Hclose]"; first solve_ndisj. iMod (is_gc_access with "InvGC isGC") as (v) "[Hlm Hclose]"; first solve_ndisj.
...@@ -572,7 +571,7 @@ Section rdcss. ...@@ -572,7 +571,7 @@ Section rdcss.
wp_cmpxchg_fail. wp_cmpxchg_fail.
iModIntro. iModIntro.
(* extract descr invariant *) (* 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. iDestruct "Hm1'_unbox" as %Hm1'_unbox.
iSplitR "AU Hld2 Hld Hp". iSplitR "AU Hld2 Hld Hp".
(* close invariant, retain some permission to l_descr', so it can be read later *) (* close invariant, retain some permission to l_descr', so it can be read later *)
...@@ -625,7 +624,7 @@ Section rdcss. ...@@ -625,7 +624,7 @@ Section rdcss.
iNext. iExists (Quiescent au_n). iFrame. iNext. iExists (Quiescent au_n). iFrame.
} }
wp_match. iApply "HΦ". 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. iDestruct "Hm1_unbox" as %Hm1_unbox.
iModIntro. iSplitR "AU Hld'". { iModIntro. iSplitR "AU Hld'". {
iNext. iExists (Updating l_descr l_m m1 n1 n2 p). eauto 15 with iFrame. 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