Commit 3d17d6a3 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy Committed by Ralf Jung

implement and verify RDCSS (on integers only, for now)

parent 917d7705
......@@ -107,3 +107,6 @@ theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v
theories/logatom/rdcss/lib/gc.v
From iris.algebra Require Import auth excl gmap.
From iris.base_logic.lib Require Export own invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang locations lifting.
Set Default Proof Using "Type".
Import uPred.
Definition gcN: namespace := nroot .@ "gc".
Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valC.
Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
Class gcG (Σ : gFunctors) := GcG {
gc_inG :> inG Σ (authR (gc_mapUR));
gc_name : gname
}.
Arguments gc_name {_} _ : assert.
Class gcPreG (Σ : gFunctors) := {
gc_preG_inG :> inG Σ (authR (gc_mapUR))
}.
Definition gcΣ : gFunctors :=
#[ GFunctor (authR (gc_mapUR)) ].
Instance subG_gcPreG {Σ} : subG gcΣ Σ gcPreG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
Definition gc_inv_P: iProp Σ :=
(((gcm: gmap loc val), own (gc_name gG) ( to_gc_map gcm) ([ map] l v gcm, (l v)) ) )%I.
Definition gc_inv : iProp Σ := inv gcN gc_inv_P.
Definition gc_mapsto (l: loc) (v: val) : iProp Σ := own (gc_name gG) ( {[l := Excl' v]}).
Definition is_gc_loc (l: loc) : iProp Σ := own (gc_name gG) ( {[l := None]}).
End defs.
Section to_gc_map.
Lemma to_gc_map_valid gcm: to_gc_map gcm.
Proof. intros l. rewrite lookup_fmap. by case (gcm !! l). Qed.
Lemma to_gc_map_empty: to_gc_map = .
Proof. by rewrite /to_gc_map fmap_empty. Qed.
Lemma to_gc_map_singleton l v: to_gc_map {[l := v]} = {[l := Excl' v]}.
Proof. by rewrite /to_gc_map fmap_insert fmap_empty. Qed.
Lemma to_gc_map_insert l v gcm:
to_gc_map (<[l := v]> gcm) = <[l := Excl' v]> (to_gc_map gcm).
Proof. by rewrite /to_gc_map fmap_insert. Qed.
Lemma to_gc_map_delete l gcm :
to_gc_map (delete l gcm) = delete l (to_gc_map gcm).
Proof. by rewrite /to_gc_map fmap_delete. Qed.
Lemma lookup_to_gc_map_None gcm l :
gcm !! l = None to_gc_map gcm !! l = None.
Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
Lemma lookup_to_gc_map_Some gcm l v :
gcm !! l = Some v to_gc_map gcm !! l = Some (Excl' v).
Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
Lemma lookup_to_gc_map_Some_2 gcm l w :
to_gc_map gcm !! l = Some w v, gcm !! l = Some v.
Proof.
rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
intros (x & Hsome & Heq). eauto.
Qed.
Lemma lookup_to_gc_map_Some_3 gcm l w :
to_gc_map gcm !! l = Some (Excl' w) gcm !! l = Some w.
Proof.
rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
intros (x & Hsome & Heq). by inversion Heq.
Qed.
Lemma excl_option_included (v: val) y:
y Excl' v y y = Excl' v.
Proof.
intros ? H. destruct y.
- apply Some_included_exclusive in H;[ | apply _ | done ].
setoid_rewrite leibniz_equiv_iff in H.
by rewrite H.
- apply is_Some_included in H.
+ by inversion H.
+ by eapply mk_is_Some.
Qed.
Lemma gc_map_singleton_included gcm l v :
{[l := Some (Excl v)]} to_gc_map gcm gcm !! l = Some v.
Proof.
rewrite singleton_included.
setoid_rewrite Some_included_total.
intros (y & Hsome & Hincluded).
pose proof (lookup_valid_Some _ _ _ (to_gc_map_valid gcm) Hsome) as Hvalid.
pose proof (excl_option_included _ _ Hvalid Hincluded) as Heq.
rewrite Heq in Hsome.
apply lookup_to_gc_map_Some_3.
by setoid_rewrite leibniz_equiv_iff in Hsome.
Qed.
End to_gc_map.
Lemma gc_init `{!invG Σ, !heapG Σ, !gcPreG Σ} E:
(|==> _ : gcG Σ, |={E}=> gc_inv)%I.
Proof.
iMod (own_alloc ( (to_gc_map ))) as (γ) "H●".
{ rewrite auth_auth_valid. exact: to_gc_map_valid. }
iModIntro.
iExists (GcG Σ _ γ).
iAssert (gc_inv_P (gG := GcG Σ _ γ)) with "[H●]" as "P".
{
iExists _. iFrame.
by iApply big_sepM_empty.
}
iMod ((inv_alloc gcN E gc_inv_P) with "P") as "#InvGC".
iModIntro. iFrame "#".
Qed.
Section gc.
Context `{!invG Σ, !heapG Σ, !gcG Σ}.
(* FIXME: still needs a constructor. *)
Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
Proof. rewrite /is_gc_loc. apply _. Qed.
Global Instance is_gc_loc_timeless (l: loc): Timeless (is_gc_loc l).
Proof. rewrite /is_gc_loc. apply _. Qed.
Global Instance gc_mapsto_timeless (l: loc) (v: val): Timeless (gc_mapsto l v).
Proof. rewrite /is_gc_loc. apply _. Qed.
Global Instance gc_inv_P_timeless: Timeless gc_inv_P.
Proof. rewrite /gc_inv_P. apply _. Qed.
Lemma make_gc l v E: gcN E gc_inv - l v ={E}= gc_mapsto l v.
Proof.
iIntros (HN) "#Hinv Hl".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iDestruct "P" as (gcm) "[H● HsepM]".
destruct (gcm !! l) as [v' | ] eqn: Hlookup.
- (* auth map contains l --> contradiction *)
iDestruct (big_sepM_lookup with "HsepM") as "Hl'"=>//.
by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
- iMod (own_update with "H●") as "[H● H◯]".
{
apply lookup_to_gc_map_None in Hlookup.
apply (auth_update_alloc _ (to_gc_map (<[l := v]> gcm)) (to_gc_map ({[l := v]}))).
rewrite to_gc_map_insert to_gc_map_singleton.
pose proof (to_gc_map_valid gcm).
setoid_rewrite alloc_singleton_local_update=>//.
}
iMod ("Hclose" with "[H● HsepM Hl]").
+ iExists _.
iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame. iFrame.
+ iModIntro. by rewrite /gc_mapsto to_gc_map_singleton.
Qed.
Lemma gc_is_gc l v: gc_mapsto l v - is_gc_loc l.
Proof.
iIntros "Hgc_l". rewrite /gc_mapsto.
assert (Excl' v = (Excl' v) None)%I as ->. { done. }
rewrite -op_singleton auth_frag_op own_op.
iDestruct "Hgc_l" as "[_ H◯_none]".
iFrame.
Qed.
Lemma is_gc_lookup_Some l gcm: is_gc_loc l - own (gc_name _) ( to_gc_map gcm) - ⌜∃ v, gcm !! l = Some v.
iIntros "Hgc_l H◯".
iCombine "H◯ Hgc_l" as "Hcomb".
iDestruct (own_valid with "Hcomb") as %Hvalid.
iPureIntro.
apply auth_both_valid in Hvalid as [Hincluded Hvalid].
setoid_rewrite singleton_included in Hincluded.
destruct Hincluded as (y & Hsome & _).
eapply lookup_to_gc_map_Some_2.
by apply leibniz_equiv_iff in Hsome.
Qed.
Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v - own (gc_name _) ( to_gc_map gcm) - gcm !! l = Some v .
Proof.
iIntros "Hgc_l H●".
iCombine "H● Hgc_l" as "Hcomb".
iDestruct (own_valid with "Hcomb") as %Hvalid.
iPureIntro.
apply auth_both_valid in Hvalid as [Hincluded Hvalid].
by apply gc_map_singleton_included.
Qed.
(** An accessor to make use of [gc_mapsto].
This opens the invariant *before* consuming [gc_mapsto] so that you can use
this before opening an atomic update that provides [gc_mapsto]!. *)
Lemma gc_access E:
gcN E
gc_inv ={E, E gcN}= l v, gc_mapsto l v -
(l v ( w, l w == gc_mapsto l w |={E gcN, E}=> True)).
Proof.
iIntros (HN) "#Hinv".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iIntros "!>" (l v) "Hgc_l".
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (gc_mapsto_lookup_Some with "Hgc_l H●") as %Hsome.
iDestruct (big_sepM_delete with "HsepM") as "[Hl HsepM]"=>//.
iFrame. iIntros (w) "Hl".
iMod (own_update_2 with "H● Hgc_l") as "[H● H◯]".
{ apply (auth_update _ _ (<[l := Excl' w]> (to_gc_map gcm)) {[l := Excl' w]}).
eapply singleton_local_update.
{ by apply lookup_to_gc_map_Some in Hsome. }
by apply option_local_update, exclusive_local_update.
}
iDestruct (big_sepM_insert with "[Hl HsepM]") as "HsepM"; [ | iFrame | ].
{ apply lookup_delete. }
rewrite insert_delete. rewrite <- to_gc_map_insert.
iModIntro. iFrame.
iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].
Qed.
Lemma is_gc_access l E: gcN E gc_inv - is_gc_loc l ={E, E gcN}= v, l v (l v ={E gcN, E}= True).
Proof.
iIntros (HN) "#Hinv Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iModIntro.
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (is_gc_lookup_Some with "Hgc_l H●") as %Hsome.
destruct Hsome as [v Hsome].
iDestruct (big_sepM_lookup_acc with "HsepM") as "[Hl HsepM]"=>//.
iExists _. iFrame.
iIntros "Hl".
iMod ("Hclose" with "[H● HsepM Hl]"); last done.
iExists _. iFrame.
by (iApply ("HsepM" with "Hl")).
Qed.
End gc.
From iris.algebra Require Import excl auth agree frac list cmra csum.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris_examples.logatom.rdcss Require Import spec.
From iris_examples.logatom.rdcss Require Export gc.
Import uPred bi List Decidable.
Set Default Proof Using "Type".
(** Using prophecy variables with helping: implementing a simplified version of
the restricted double-compare single-swap from "A Practical Multi-Word Compare-and-Swap Operation" by Harris et al. (DISC 2002)
*)
(** * Implementation of the functions. *)
(* 1) l_m corresponds to the A location in the paper and can differ when helping another thread
in the same RDCSS instance.
2) l_n corresponds to the B location in the paper and identifies a single RDCSS instance.
3) Values stored at the B location have type
Int + Ref (Ref * Int * Int * Int * Proph)
3.1) If the value is injL n, then no operation is on-going and the logical state is n.
3.2) If the value is injR (Ref (l_m', m1', n1', n2', p)), then an operation is on-going
with corresponding A location l_m'. The reference pointing to the tuple of values
corresponds to the descriptor in the paper. We use the name l_descr for the
such a descriptor reference.
*)
(*
new_rdcss() :=
let l_n = ref ( ref(injL 0) ) in
ref l_n
*)
Definition new_rdcss : val :=
λ: <>,
let: "l_n" := ref (InjL #0) in "l_n".
(*
complete(l_descr, l_n) :=
let (l_m, m1, n1, n2, p) := !l_descr in
(* data = (l_m, m1, n1, n2, p) *)
let l_ghost = ref #() in
let n_new = (if !l_m = m1 then n1 else n2) in
Resolve (CAS l_n (InjR l_descr) (ref (InjL n_new))) p l_ghost ; #().
*)
Definition complete : val :=
λ: "l_descr" "l_n",
let: "data" := !"l_descr" in
(* data = (l_m, m1, n1, n2, p) *)
let: "l_m" := Fst (Fst (Fst (Fst ("data")))) in
let: "m1" := Snd (Fst (Fst (Fst ("data")))) in
let: "n1" := Snd (Fst (Fst ("data"))) in
let: "n2" := Snd (Fst ("data")) in
let: "p" := Snd ("data") in
let: "l_ghost" := ref #() in
let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
Resolve (CAS "l_n" (InjR "l_descr") (InjL "n_new")) "p" "l_ghost" ;; #().
(*
get(l_n) :=
match: !l_n with
| injL n => n
| injR (l_descr) =>
complete(l_descr, l_n);
get(l_n)
end.
*)
Definition get : val :=
rec: "get" "l_n" :=
match: !"l_n" with
InjL "n" => "n"
| InjR "l_descr" =>
complete "l_descr" "l_n" ;;
"get" "l_n"
end.
(*
rdcss(l_m, l_n, m1, n1, n2) :=
let p := NewProph in
let l_descr := ref (l_m, m1, n1, n2, p) in
(rec: rdcss_inner()
let r := CAS(l_n, InjL n1, InjR l_descr) in
match r with
InjL n =>
if n = n1 then
complete(l_descr, l_n) ; n1
else
n
| InjR l_descr_other =>
complete(l_descr_other, l_n) ;
rdcss_inner()
end
)()
*)
Definition rdcss: val :=
λ: "l_m" "l_n" "m1" "n1" "n2",
(* allocate fresh descriptor *)
let: "p" := NewProph in
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
(* start rdcss computation with allocated descriptor *)
( rec: "rdcss_inner" "_" :=
let: "r" := (CAS "l_n" (InjL "n1") (InjR "l_descr")) in
match: "r" with
InjL "n" =>
(* non-descriptor value read, check if CAS was successful *)
if: "n" = "n1" then
(* CAS was successful, finish operation *)
complete "l_descr" "l_n" ;; "n1"
else
(* CAS failed, hence we could linearize at the CAS *)
"n"
| InjR "l_descr_other" =>
(* a descriptor from a different operation was read, try to help and then restart *)
complete "l_descr_other" "l_n" ;;
"rdcss_inner" #()
end
) #().
(** ** Proof setup *)
Definition numUR := authR $ optionUR $ exclR ZC.
Definition tokenUR := exclR unitC.
Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
Class rdcssG Σ := RDCSSG {
rdcss_numG :> inG Σ numUR;
rdcss_tokenG :> inG Σ tokenUR;
rdcss_one_shotG :> inG Σ one_shotUR;
}.
Definition rdcssΣ : gFunctors :=
#[GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
Instance subG_rdcssΣ {Σ} : subG rdcssΣ Σ rdcssG Σ.
Proof. solve_inG. Qed.
Section rdcss.
Context {Σ} `{!heapG Σ, !rdcssG Σ, !gcG Σ }.
Context (N : namespace).
Local Definition descrN := N .@ "descr".
Local Definition rdcssN := N .@ "rdcss".
(** Updating and synchronizing the number RAs *)
Lemma sync_num_values γ_n (n m : Z) :
own γ_n ( Excl' n) - own γ_n ( Excl' m) - n = m.
Proof.
iIntros "H● H◯". iCombine "H●" "H◯" as "H". iDestruct (own_valid with "H") as "H".
by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma update_num_value γ_n (n1 n2 m : Z) :
own γ_n ( Excl' n1) - own γ_n ( Excl' n2) == own γ_n ( Excl' m) own γ_n ( Excl' m).
Proof.
iIntros "H● H◯". iCombine "H●" "H◯" as "H". rewrite -own_op. iApply (own_update with "H").
by apply auth_update, option_local_update, exclusive_local_update.
Qed.
Definition rdcss_content (γ_n : gname) (n : Z) := (own γ_n ( Excl' n))%I.
(** Definition of the invariant *)
Fixpoint val_to_some_loc (ln: loc) (vs : list (val * val)) : option loc :=
match vs with
| (InjRV (LitV (LitLoc ln')), LitV (LitLoc l)) :: _ => if bool_decide(ln = ln') then Some l else None
| _ :: vs => val_to_some_loc ln vs
| _ => None
end.
Inductive abstract_state : Set :=
| Quiescent : Z abstract_state
| Updating : loc loc Z Z Z proph_id abstract_state.
Definition state_to_val (s : abstract_state) : val :=
match s with
| Quiescent n => InjLV #n
| Updating ld lm m1 n1 n2 p => InjRV #ld
end.
Definition own_token γ := (own γ (Excl ()))%I.
Definition pending_state P (n1 : Z) (proph_winner : option loc) l_ghost_winner (γ_n : gname) :=
(P match proph_winner with None => True | Some l => l = l_ghost_winner end own γ_n ( Excl' n1))%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 loc) (l_ghost_winner : loc) :=
(l_ghost_winner {1/2} - match proph_winner with None => True | Some l => l = l_ghost_winner Q end)%I.
(* The same thread then wins the CAS 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
is owned by the thread whose request this is.
In this state, [l_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
"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 l_ghost_winner : loc) (γ_t : gname) :=
((Qn own_token γ_t) l_ghost_winner - (l_descr {1/2} -) )%I.
(* 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 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
accepted_state (Q #n) (val_to_some_loc l_descr vs) l_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q #n) l_descr l_ghost_winner γ_t))%I.
Definition pau P Q γ l_m m1 n1 n2 :=
( P - AU << (m n : Z), (gc_mapsto l_m #m) rdcss_content γ n >> @ (⊤∖↑N)∖↑gcN,
<< (gc_mapsto l_m #m) (rdcss_content γ (if (decide ((m = m1) (n = n1))) then n2 else n)),
COMM Q #n >>)%I.
Definition rdcss_inv γ_n l_n :=
( (s : abstract_state),
l_n {1/2} (state_to_val s)
match s with
| Quiescent n =>
(* (InjLV #n) = state_to_val (Quiescent n) *)
(* In this state the CAS 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 =>
q P Q l_ghost_winner γ_t γ_s,
(* (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:
- [γ_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 [descr] protocol in the [done] state. *)
l_descr {1/2 + q} (#l_m, #m1, #n1, #n2, #p)%V
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.
Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _ _)) => unfold rdcss_inv.
Definition is_rdcss (γ_n : gname) (rdcss_data: val) :=
( (l_n : loc), rdcss_data = #l_n inv rdcssN (rdcss_inv γ_n l_n) gc_inv N ## gcN)%I.
Global Instance is_rdcss_persistent γ_n l_n: Persistent (is_rdcss γ_n l_n) := _.
Global Instance rdcss_content_timeless γ_n n : Timeless (rdcss_content γ_n n) := _.
Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (Quiescent 0).
Lemma rdcss_content_exclusive γ_n l_n_1 l_n_2 :
rdcss_content γ_n l_n_1 - rdcss_content γ_n l_n_2 - False.
Proof.
iIntros "Hn1 Hn2". iDestruct (own_valid_2 with "Hn1 Hn2") as %?.
done.
Qed.
(** A few more helper lemmas that will come up later *)
Lemma mapsto_valid_3 l v1 v2 q :
l v1 - l {q} v2 - False.
Proof.
iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %Hv.
apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
Qed.
(** 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 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 descrN as (vs) "(Hp & [NotDone | Done])".
* (* Moved back to NotDone: contradiction. *)
iDestruct "NotDone" as "(>Hs' & _ & _)".
iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
* iDestruct "Done" as "(_ & QT & Hghost)".
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 descr_inv.
iExists _. iFrame "Hp". iRight.
unfold done_state. iFrame "#∗".
Qed.
(** ** Proof of [complete] *)
(** The part of [complete] for the succeeding thread that moves from [accepted] to [done] state *)
Lemma complete_succeeding_thread_pending (γ_n γ_t γ_s : gname) l_n P Q p
(n1 n : Z) (l_descr l_ghost : loc) Φ :
inv rdcssN (rdcss_inv γ_n l_n) -
inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost γ_n γ_t γ_s) -
l_ghost {1 / 2} #() -
((own_token γ_t ={}= (Q #n1)) - Φ #()) -
own γ_n ( Excl' n) -
WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
iIntros "#InvC #InvS Hl_ghost HQ Hn●". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
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 & _)".
iDestruct "Hlghost" as (v') ">Hlghost".
by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") 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.
}
(* 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
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. }
iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
simpl.
iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s') "([>Hld >Hld'] & Hrest)".
(* We perform the CAS. *)
iCombine "Hln Hln'" as "Hln".
wp_apply (wp_resolve with "Hp"); first done. wp_cas_suc.
iIntros (vs' ->) "Hp'". simpl. case_bool_decide; simplify_eq.
(* Update to Done. *)
iDestruct "Accepted" as "[Hl_ghost_inv [HEq Q]]".
iMod (own_update with "Hs") as "Hs".
{ apply (cmra_update_exclusive (Cinr (to_agree ()))). done. }
iDestruct "Hs" as "#Hs'". iModIntro.
iSplitL "Hl_ghost_inv Hl_ghost Q Hp' Hld".
(* Update state to Done. *)
{ iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
iFrame "#∗". iSplitR "Hld"; iExists _; done. }
iModIntro. iSplitR "HQ".
{ iNext. iDestruct "Hln" as "[Hln1 Hln2]".
iExists (Quiescent n). iFrame. }
iApply wp_fupd. wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
Qed.
(** The part of [complete] for the failing thread *)
Lemma complete_failing_thread γ_n γ_t γ_s l_n l_descr P Q p n1 n l_ghost_inv l_ghost Φ :
l_ghost_inv l_ghost
inv rdcssN (rdcss_inv γ_n l_n) -
inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -
((own_token γ_t ={}= (Q #n1)) - Φ #()) -
WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
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. *)
iDestruct "NotDone" as "(_ & >Hln' & State)".
iDestruct (mapsto_agree with "Hln Hln'") as %[=->].
iCombine "Hln Hln'" as "Hlln".
wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
iIntros (vs' ->). simpl. case_bool_decide; simplify_eq.
iDestruct "State" as "[Pending | Accepted]".
+ iDestruct "Pending" 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]. *)
(* It must be that (state_to_val s) ≠ l because we are in the failing thread. *)
destruct s as [n' |l_descr' ].
{ (* (injL n) is the current value, hence the CAS fails *)
(* FIXME: proof duplication *)
wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
iIntros (vs' ->) "Hp". iModIntro.
iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
}
(* (injR l_descr') is the current value *)
destruct (decide (l_descr' = l_descr)) as [->|Hn]. {
(* 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".
iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s') "(>[Hld' Hld''] & Hrest)".
iDestruct (mapsto_combine with "Hld Hld'") as "[Hld _]".
rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
}
(* The CAS fails. *)
wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
iIntros (vs' ->) "Hp". iModIntro.
iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.