Commit d6c53a69 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

small changes as suggested in MR discussion

parent 06e599ed
......@@ -224,11 +224,13 @@ Section rdcss.
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.
......@@ -291,18 +293,16 @@ Section rdcss.
(** ** 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_m l_n P Q p
(m1 n1 n2 n : Z) (l_descr l_ghost : loc) Φ :
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) -
pau P Q γ_n l_m m1 n1 n2 -
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 PAU Hl_ghost HQ Hn●". wp_bind (Resolve _ _ _)%E.
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
......@@ -347,16 +347,14 @@ Section rdcss.
Qed.
(** The part of [complete] for the failing thread *)
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 Φ :
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) -
pau P Q γ_n l_m m1 n1 n2 -
((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 PAU HQ". wp_bind (Resolve _ _ _)%E.
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
......@@ -464,7 +462,7 @@ Section rdcss.
case_bool_decide; simplify_eq; wp_if; wp_pures;
[rewrite decide_True; last done | rewrite decide_False; last tauto];
iApply (complete_succeeding_thread_pending
with "InvC InvS PAU Hl_ghost'2 HQ Hn●").
with "InvC InvS Hl_ghost'2 HQ Hn●").
+ (* Accepted: contradiction *)
iDestruct "Accepted" as "[>Hl_ghost_inv _]".
iDestruct "Hl_ghost_inv" as (v') "Hlghost".
......@@ -488,7 +486,7 @@ Section rdcss.
destruct (decide (v = #m1)) as [-> | ];
case_bool_decide; simplify_eq; wp_if; wp_pures;
iApply (complete_failing_thread
with "InvC InvS PAU HQ"); done.
with "InvC InvS HQ"); done.
Qed.
(** ** Proof of [rdcss] *)
......@@ -590,7 +588,7 @@ Section rdcss.
iSplitR; last by iFrame. iExists ln. iSplit; done.
Qed.
(** ** Proof of [get_spec] *)
(** ** Proof of [get] *)
Lemma get_spec γ_n v :
N ## gcN gc_inv - is_rdcss γ_n v -
<<< (n : Z), rdcss_content γ_n n >>>
......
......@@ -19,8 +19,8 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
rdcss_content (γ : name) (n : Z) : iProp Σ;
(* -- predicate properties -- *)
is_rdcss_persistent N γ v : Persistent (is_rdcss N γ v);
rdcss_content_timeless γ lln : Timeless (rdcss_content γ lln);
rdcss_content_exclusive γ lln1 lln2 : rdcss_content γ lln1 - rdcss_content γ lln2 - False;
rdcss_content_timeless γ n : Timeless (rdcss_content γ n);
rdcss_content_exclusive γ n1 n2 : rdcss_content γ n1 - rdcss_content γ n2 - False;
(* -- operation specs -- *)
new_rdcss_spec N :
{{{ True }}}
......@@ -42,4 +42,5 @@ Arguments atomic_rdcss _ {_} {_}.
Existing Instances
is_rdcss_persistent rdcss_content_timeless
name_countable name_eqdec.
\ No newline at end of file
name_countable name_eqdec.
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