Commit 99f8ad18 authored by Ralf Jung's avatar Ralf Jung

replace gc.v by inv_heap Iris lib

parent 66c22fad
......@@ -96,7 +96,6 @@ theories/hocap/parfib.v
theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/lib/gc.v
theories/logatom/elimination_stack/hocap_spec.v
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.v
......
......@@ -102,7 +102,7 @@ Instance subG_cincΣ {Σ} : subG cincΣ Σ → cincG Σ.
Proof. solve_inG. Qed.
Section conditional_counter.
Context {Σ} `{!heapG Σ, !gcG Σ, !cincG Σ}.
Context {Σ} `{!heapG Σ, !inv_heapG loc val Σ, !cincG Σ}.
Context (N : namespace).
Local Definition stateN := N .@ "state".
......@@ -185,8 +185,8 @@ Section conditional_counter.
own γ_s (Cinr $ to_agree ()) done_state Q l l_ghost_winner γ_t))%I.
Definition pau P Q γs f :=
( P - AU << (b : bool) (n : Z), counter_content γs n gc_mapsto f #b >> @ ∖↑N∖↑gcN,
<< counter_content γs (if b then n + 1 else n) gc_mapsto f #b, COMM Q >>)%I.
( P - AU << (b : bool) (n : Z), counter_content γs n f _(λ _, True) #b >> @ ∖↑N∖↑inv_heapN,
<< counter_content γs (if b then n + 1 else n) f _(λ _, True) #b, COMM Q >>)%I.
Definition counter_inv γ_n c :=
( (l : loc) (q : Qp) (s : abstract_state),
......@@ -202,13 +202,13 @@ Section conditional_counter.
to get out the [Q] in the end.
- [γ_s] reflects whether the protocol is [done] yet or not. *)
inv stateN (state_inv P Q p n c l l_ghost_winner γ_n γ_t γ_s)
pau P Q γ_n f is_gc_loc f
pau P Q γ_n f f ↦□ (λ _, True)
end)%I.
Local Hint Extern 0 (environments.envs_entails _ (counter_inv _ _)) => unfold counter_inv : core.
Definition is_counter (γ_n : gname) (ctr : val) :=
( (c : loc), ctr = #c N ## gcN gc_inv inv counterN (counter_inv γ_n c))%I.
( (c : loc), ctr = #c N ## inv_heapN inv_heap_inv loc val inv counterN (counter_inv γ_n c))%I.
Global Instance is_counter_persistent γs ctr : Persistent (is_counter γs ctr) := _.
......@@ -354,12 +354,12 @@ Section conditional_counter.
thread's requests, which is why we cannot ask for the token
as a precondition. *)
Lemma complete_spec (c f l : loc) (n : Z) (p : proph_id) γ_n γ_t γ_s l_ghost_inv P Q :
N ## gcN
gc_inv -
N ## inv_heapN
inv_heap_inv loc val -
inv counterN (counter_inv γ_n c) -
inv stateN (state_inv P Q p n c l l_ghost_inv γ_n γ_t γ_s) -
pau P Q γ_n f -
is_gc_loc f -
f ↦□ (λ _, True) -
{{{ True }}}
complete #c #f #l #n #p
{{{ RET #(); (own_token γ_t ={}= Q) }}}.
......@@ -378,12 +378,12 @@ Section conditional_counter.
+ (* Pending: update to accepted *)
iDestruct "Pending" as "[P >[Hvs Hn●]]".
iDestruct ("PAU" with "P") as ">AU".
iMod (gc_access with "GC") as "Hgc"; first solve_ndisj.
iMod (inv_mapsto_own_acc_strong with "GC") as "Hgc"; first solve_ndisj.
(* open and *COMMIT* AU, sync flag and counter *)
iMod "AU" as (b n2) "[[Hn◯ Hf] [_ Hclose]]".
iDestruct ("Hgc" with "Hf") as "[Hf Hfclose]".
iDestruct ("Hgc" with "Hf") as "(_ & Hf & Hfclose)".
wp_load.
iMod ("Hfclose" with "Hf") as "[Hf Hfclose]".
iMod ("Hfclose" with "[//] Hf") as "[Hf Hfclose]".
iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
iMod (update_counter_value _ _ _ (if b then n2 + 1 else n2) with "Hn● Hn◯")
as "[Hn● Hn◯]".
......@@ -412,7 +412,7 @@ Section conditional_counter.
iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
- (* we are the failing thread. exploit that [f] is a GC location. *)
iMod (is_gc_access with "GC isGC") as (b) "[H↦ Hclose]"; first solve_ndisj.
iMod (inv_mapsto_acc with "GC isGC") as (b) "(_ & H↦ & Hclose)"; first solve_ndisj.
wp_load.
iMod ("Hclose" with "H↦") as "_". iModIntro.
(* close invariant *)
......@@ -429,9 +429,9 @@ Section conditional_counter.
Lemma cinc_spec γs v (f: loc) :
is_counter γs v -
<<< (b : bool) (n : Z), counter_content γs n gc_mapsto f #b >>>
cinc v #f @∖↑N∖↑gcN
<<< counter_content γs (if b then n + 1 else n) gc_mapsto f #b, RET #() >>>.
<<< (b : bool) (n : Z), counter_content γs n f _(λ _, True) #b >>>
cinc v #f @∖↑N∖↑inv_heapN
<<< counter_content γs (if b then n + 1 else n) f _(λ _, True) #b, RET #() >>>.
Proof.
iIntros "#InvC". iDestruct "InvC" as (c_l [-> ?]) "[#GC #InvC]".
iIntros (Φ) "AU". iLöb as "IH".
......@@ -454,7 +454,7 @@ Section conditional_counter.
wp_cmpxchg_suc.
(* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
iMod "AU" as (b' n') "[[CC Hf] [Hclose _]]".
iDestruct (gc_is_gc with "Hf") as "#Hgc".
iDestruct (inv_mapsto_own_inv with "Hf") as "#Hgc".
iMod ("Hclose" with "[CC Hf]") as "AU"; first by iFrame.
(* Initialize new [state] protocol .*)
iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
......@@ -490,8 +490,8 @@ Section conditional_counter.
Qed.
Lemma new_counter_spec :
N ## gcN
gc_inv -
N ## inv_heapN
inv_heap_inv loc val -
{{{ True }}}
new_counter #()
{{{ ctr γs, RET ctr ; is_counter γs ctr counter_content γs 0 }}}.
......@@ -514,7 +514,7 @@ Section conditional_counter.
Lemma get_spec γs v :
is_counter γs v -
<<< (n : Z), counter_content γs n >>>
get v @∖↑N∖↑gcN
get v @∖↑N∖↑inv_heapN
<<< counter_content γs n, RET #n >>>.
Proof.
iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (c_l [-> ?]) "[GC InvC]".
......@@ -541,7 +541,7 @@ Section conditional_counter.
End conditional_counter.
Definition atomic_cinc `{!heapG Σ, !cincG Σ, !gcG Σ} :
Definition atomic_cinc `{!heapG Σ, !cincG Σ, !inv_heapG loc val Σ} :
spec.atomic_cinc Σ :=
{| spec.new_counter_spec := new_counter_spec;
spec.cinc_spec := cinc_spec;
......
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export gen_inv_heap.
From iris.program_logic Require Export atomic.
From iris_examples.logatom.lib Require Export gc.
From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_cinc {Σ} `{!heapG Σ, !gcG Σ} := AtomicCinc {
Record atomic_cinc {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicCinc {
(* -- operations -- *)
new_counter : val;
cinc : val;
......@@ -24,20 +24,20 @@ Record atomic_cinc {Σ} `{!heapG Σ, !gcG Σ} := AtomicCinc {
counter_content γs c1 - counter_content γs c2 - False;
(* -- operation specs -- *)
new_counter_spec N :
N ## gcN
gc_inv -
N ## inv_heapN
inv_heap_inv loc val -
{{{ True }}}
new_counter #()
{{{ ctr γs, RET ctr ; is_counter N γs ctr counter_content γs 0 }}};
cinc_spec N γs v (f : loc) :
is_counter N γs v -
<<< (b : bool) (n : Z), counter_content γs n gc_mapsto f #b >>>
cinc v #f @∖↑N∖↑gcN
<<< counter_content γs (if b then n + 1 else n) gc_mapsto f #b, RET #() >>>;
<<< (b : bool) (n : Z), counter_content γs n f _(λ _, True) #b >>>
cinc v #f @∖↑N∖↑inv_heapN
<<< counter_content γs (if b then n + 1 else n) f _(λ _, True) #b, RET #() >>>;
get_spec N γs v:
is_counter N γs v -
<<< (n : Z), counter_content γs n >>>
get v @∖↑N∖↑gcN
get v @∖↑N∖↑inv_heapN
<<< counter_content γs n, RET #n >>>;
}.
Arguments atomic_cinc _ {_ _}.
......
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 $ valO.
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_l.
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.
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 Σ}.
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_acc_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 -singleton_op 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_l 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_acc_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_acc_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.
......@@ -172,7 +172,7 @@ Instance subG_rdcssΣ {Σ} : subG rdcssΣ Σ → rdcssG Σ.
Proof. solve_inG. Qed.
Section rdcss.
Context {Σ} `{!heapG Σ, !rdcssG Σ, !gcG Σ }.
Context {Σ} `{!heapG Σ, !rdcssG Σ, !inv_heapG loc val Σ }.
Context (N : namespace).
Implicit Types γ_n γ_a γ_t γ_s : gname.
......@@ -287,8 +287,8 @@ Section rdcss.
Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv : core.
Definition pau P Q l_n l_m m1 n1 n2 :=
( P - AU << (m n : val), (gc_mapsto l_m m) rdcss_state l_n n >> @ (∖↑N)∖↑gcN,
<< (gc_mapsto l_m m) (rdcss_state l_n (if (decide ((m = m1) (n = n1))) then n2 else n)),
( P - AU << (m n : val), (l_m _(λ _, True) m) rdcss_state l_n n >> @ (∖↑N)∖↑inv_heapN,
<< (l_m _(λ _, True) m) (rdcss_state l_n (if (decide ((m = m1) (n = n1))) then n2 else n)),
COMM Q n >>)%I.
Definition rdcss_inv l_n :=
......@@ -314,13 +314,13 @@ Section rdcss.
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 tid_ghost_winner γ_t γ_s γ_a)
pau P Q l_n l_m m1 n1 n2 is_gc_loc l_m
pau P Q l_n l_m m1 n1 n2 l_m ↦□ (λ _, True)
end)%I.
Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _)) => unfold rdcss_inv : core.
Definition is_rdcss (l_n : loc) :=
(inv rdcssN (rdcss_inv l_n) gc_inv N ## gcN)%I.
(inv rdcssN (rdcss_inv l_n) inv_heap_inv loc val N ## inv_heapN)%I.
Global Instance is_rdcss_persistent l_n : Persistent (is_rdcss l_n) := _.
......@@ -481,12 +481,12 @@ Section rdcss.
as a precondition. *)
Lemma complete_spec l_n l_m l_descr (m1 n1 n2 : val) p γ_t γ_s γ_a tid_ghost_inv P Q q :
val_is_unboxed m1
N ## gcN
N ## inv_heapN
inv rdcssN (rdcss_inv l_n) -
inv descrN (descr_inv P Q p n1 l_n l_descr tid_ghost_inv γ_t γ_s γ_a) -
pau P Q l_n l_m m1 n1 n2 -
is_gc_loc l_m -
gc_inv -
l_m ↦□ (λ _, True) -
inv_heap_inv loc val -
{{{ l_descr {q} (#l_m, m1, n1, n2, #p) }}}
complete #l_descr #l_n
{{{ RET #(); (own_token γ_t ={}= (Q n1)) }}}.
......@@ -505,7 +505,7 @@ Section rdcss.
+ (* Pending: update to accepted *)
iDestruct "Pending" as "[P >(Hvs & Hn● & Token_a)]".
iDestruct ("PAU" with "P") as ">AU".
iMod (gc_access with "InvGC") as "Hgc"; first solve_ndisj.
iMod (inv_mapsto_own_acc_strong with "InvGC") as "Hgc"; first solve_ndisj.
(* open and *COMMIT* AU, sync B location l_n and A location l_m *)
iMod "AU" as (m' n') "[CC [_ Hclose]]".
iDestruct "CC" as "[Hgc_lm Hn◯]".
......@@ -514,11 +514,11 @@ Section rdcss.
iMod (update_value _ _ _ (if decide (m' = m1 n' = n') then n2 else n') with "Hn● Hn◯")
as "[Hn● Hn◯]".
(* get access to A location *)
iDestruct ("Hgc" with "Hgc_lm") as "[Hl Hgc_close]".
iDestruct ("Hgc" with "Hgc_lm") as "(_ & Hl & Hgc_close)".
(* read A location *)
wp_load.
(* sync A location *)
iMod ("Hgc_close" with "Hl") as "[Hgc_lm Hgc_close]".
iMod ("Hgc_close" with "[//] Hl") as "[Hgc_lm Hgc_close]".
(* give back access to A location *)
iMod ("Hclose" with "[Hn◯ $Hgc_lm]") as "Q"; first done.
iModIntro. iMod "Hgc_close" as "_".
......@@ -544,7 +544,7 @@ Section rdcss.
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.
iMod (inv_mapsto_acc with "InvGC isGC") as (v) "(_ & Hlm & Hclose)"; first solve_ndisj.
wp_load.
iMod ("Hclose" with "Hlm") as "_". iModIntro.
iModIntro.
......@@ -562,9 +562,9 @@ Section rdcss.
val_is_unboxed m1
val_is_unboxed (InjLV n1)
is_rdcss l_n -
<<< (m n: val), gc_mapsto l_m m rdcss_state l_n n >>>
rdcss #l_m #l_n m1 n1 n2 @((∖↑N)∖↑gcN)
<<< gc_mapsto l_m m rdcss_state l_n (if decide (m = m1 n = n1) then n2 else n), RET n >>>.
<<< (m n: val), l_m _(λ _, True) m rdcss_state l_n n >>>
rdcss #l_m #l_n m1 n1 n2 @((∖↑N)∖↑inv_heapN)
<<< l_m _(λ _, True) m rdcss_state l_n (if decide (m = m1 n = n1) then n2 else n), RET n >>>.
Proof.
iIntros (Hm1_unbox Hn1_unbox) "(#InvR & #InvGC & %)". iIntros (Φ) "AU".
(* allocate fresh descriptor *)
......@@ -586,7 +586,7 @@ Section rdcss.
wp_cmpxchg_suc.
(* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
iMod "AU" as (b' n') "[[Hf CC] [Hclose _]]".
iDestruct (gc_is_gc with "Hf") as "#Hgc".
iDestruct (inv_mapsto_own_inv with "Hf") as "#Hgc".
iMod ("Hclose" with "[Hf CC]") as "AU"; first by iFrame.
(* Initialize new [descr] protocol .*)
iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
......@@ -638,7 +638,7 @@ Section rdcss.
(** ** Proof of [new_rdcss] *)
Lemma new_rdcss_spec (n : val) :
N ## gcN gc_inv -
N ## inv_heapN inv_heap_inv loc val -
{{{ True }}}
new_rdcss n
{{{ l_n, RET #l_n ; is_rdcss l_n rdcss_state l_n n }}}.
......@@ -685,7 +685,7 @@ Section rdcss.
End rdcss.
Definition atomic_rdcss `{!heapG Σ, !rdcssG Σ, !gcG Σ} :
Definition atomic_rdcss `{!heapG Σ, !rdcssG Σ, !inv_heapG loc val Σ} :
spec.atomic_rdcss Σ :=
{| spec.new_rdcss_spec := new_rdcss_spec;
spec.rdcss_spec := rdcss_spec;
......
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export gen_inv_heap.
From iris.program_logic Require Export atomic.
From iris_examples.logatom.lib Require Export gc.
From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for RDCSS.
......@@ -12,7 +12,7 @@ as given by [rdcss_spec] relies on the [gc_mapsto l_m m] assertion. It roughly
corresponds to the usual [l_m ↦ m] but with an additional guarantee that [l_m]
will not be deallocated. This guarantees that unique immutable descriptors can
be associated to each operation, and that they cannot be "reused". *)
Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
Record atomic_rdcss {Σ} `{!heapG Σ, !inv_heapG loc val Σ} := AtomicRdcss {
(* -- operations -- *)
new_rdcss : val;
rdcss: val;
......@@ -27,7 +27,7 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {