Commit 3f2a1f72 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

adjusted is_rdcss abstract predicate to contain gc_inv and disjointness

parent d6c53a69
......@@ -245,7 +245,7 @@ Section rdcss.
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))%I.
( (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) := _.
......@@ -491,13 +491,13 @@ Section rdcss.
(** ** Proof of [rdcss] *)
Lemma rdcss_spec γ_n v (l_m: loc) (m1 n1 n2: Z) :
N ## gcN is_rdcss γ_n v - is_gc_loc l_m - gc_inv -
is_rdcss γ_n v - is_gc_loc l_m -
<<< (m n: Z), gc_mapsto l_m #m rdcss_content γ_n n >>>
rdcss #l_m v #m1 #n1 #n2 @((∖↑N)∖↑gcN)
<<< gc_mapsto l_m #m rdcss_content γ_n (if decide (m = m1 n = n1) then n2 else n), RET #n >>>.
Proof.
iIntros (Hdisj) "#InvC #GC #InvGC". iDestruct "InvC" as (l_n) "[Heq InvC]".
iDestruct "Heq" as %->. iIntros (Φ) "AU".
iIntros "Hrdcss #GC". iDestruct "Hrdcss" as (l_n) "(Heq & #InvR & #InvGC & Hdisj)".
iDestruct "Heq" as %->. iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
(* allocate fresh descriptor *)
wp_lam. wp_pures.
wp_apply wp_new_proph; first done.
......@@ -570,33 +570,36 @@ Section rdcss.
(** ** Proof of [new_rdcss] *)
Lemma new_rdcss_spec :
N ## gcN gc_inv -
{{{ True }}}
new_rdcss #()
{{{ l_n γ_n, RET l_n ; is_rdcss γ_n l_n rdcss_content γ_n 0 }}}.
Proof.
iIntros (Hdisj) "#InvGC". iModIntro.
iIntros (Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
wp_alloc ln as "Hln".
iMod (own_alloc ( Excl' 0 Excl' 0)) as (γ_n) "[Hn● Hn◯]".
{ by apply auth_both_valid. }
iMod (inv_alloc rdcssN _ (rdcss_inv γ_n ln)
with "[Hln Hn●]") as "#InvC".
with "[Hln Hn●]") as "#InvR".
{ iNext. iDestruct "Hln" as "[Hln1 Hln2]".
iExists (Quiescent 0). iFrame. }
wp_let.
iModIntro.
iApply ("HΦ" $! #ln γ_n).
iSplitR; last by iFrame. iExists ln. iSplit; done.
iSplitR; last by iFrame. iExists ln. by iFrame "#".
Qed.
(** ** Proof of [get] *)
Lemma get_spec γ_n v :
N ## gcN gc_inv - is_rdcss γ_n v -
is_rdcss γ_n v -
<<< (n : Z), rdcss_content γ_n n >>>
get v @(∖↑N)
<<< rdcss_content γ_n n, RET #n >>>.
Proof.
iIntros (Hdisj) "#InvGC". iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (lln) "[Heq InvC]".
iDestruct "Heq" as %->. iLöb as "IH". wp_lam. repeat (wp_proj; wp_let). wp_bind (! _)%E.
iIntros "Hrdcss". iDestruct "Hrdcss" as (l_n) "(Heq & #InvR & #InvGC & Hdisj)".
iDestruct "Heq" as %->. iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
iLöb as "IH". wp_lam. repeat (wp_proj; wp_let). wp_bind (! _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)".
wp_load.
destruct s as [n|l_descr lm m1 n1 n2 p].
......
......@@ -23,16 +23,17 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
rdcss_content_exclusive γ n1 n2 : rdcss_content γ n1 - rdcss_content γ n2 - False;
(* -- operation specs -- *)
new_rdcss_spec N :
N ## gcN gc_inv -
{{{ True }}}
new_rdcss #()
{{{ lln γ, RET lln ; is_rdcss N γ lln rdcss_content γ 0 }}};
rdcss_spec N γ v lm (m1 n1 n2 : Z):
N ## gcN is_rdcss N γ v - is_gc_loc lm - gc_inv -
is_rdcss N γ v - is_gc_loc lm -
<<< (m n: Z), gc_mapsto lm #m rdcss_content γ n >>>
rdcss #lm v #m1 #n1 #n2 @((∖↑N)∖↑gcN)
<<< gc_mapsto lm #m rdcss_content γ (if decide (m = m1 n = n1) then n2 else n), RET #n >>>;
get_spec N γ v:
N ## gcN gc_inv - is_rdcss N γ v -
is_rdcss N γ v -
<<< (n : Z), rdcss_content γ n >>>
get v @(∖↑N)
<<< rdcss_content γ n, RET #n >>>;
......
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