Commit 25207539 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

applied ghost state singleton pattern to gc library

updated _CoqProject file
parent 51b96e28
Pipeline #17783 canceled with stage
......@@ -108,3 +108,4 @@ 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
......@@ -13,26 +13,33 @@ Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$>
Class gcG (Σ : gFunctors) := Gc_mapG {
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_gcG {Σ} : subG gcΣ Σ gcG Σ.
Instance subG_gcPreG {Σ} : subG gcΣ Σ gcPreG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{!invG Σ, !heapG Σ, !gcG Σ} (γ: gname).
Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
Definition gc_inv_P: iProp Σ :=
(((gcm: gmap loc val), own γ ( to_gc_map gcm) ([ map] l v gcm, (l v)) ) )%I.
(((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 γ ( {[l := Excl' v]}).
Definition gc_mapsto (l: loc) (v: val) : iProp Σ := own (gc_name gG) ( {[l := Excl' v]}).
Definition is_gc_loc (l: loc) : iProp Σ := own γ ( {[l := None]}).
Definition is_gc_loc (l: loc) : iProp Σ := own (gc_name gG) ( {[l := None]}).
End defs.
......@@ -106,21 +113,21 @@ End to_gc_map.
Section gc.
Context `{!invG Σ, !heapG Σ, !gcG Σ} (γ: gname).
Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc γ l).
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).
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).
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 γ).
Global Instance gc_inv_P_timeless: Timeless gc_inv_P.
Proof. rewrite /gc_inv_P. apply _. Qed.
Lemma make_gc (l: loc) (v: val): gc_inv γ - l v ={gcN}= gc_mapsto γ l v.
Lemma make_gc l v: gc_inv - l v ={gcN}= gc_mapsto l v.
Proof.
iIntros "#Hinv Hl".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
......@@ -143,7 +150,7 @@ Section gc.
+ iModIntro. by rewrite /gc_mapsto to_gc_map_singleton.
Qed.
Lemma gc_is_gc (l: loc) (v: val): gc_mapsto γ l v - is_gc_loc γ l.
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. }
......@@ -152,7 +159,7 @@ Section gc.
iFrame.
Qed.
Lemma is_gc_lookup_Some l gcm: is_gc_loc γ l - own γ ( to_gc_map gcm) - v, gcm !! l = Some v.
Lemma is_gc_lookup_Some l gcm: is_gc_loc l - own (gc_name gG) ( 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.
......@@ -164,7 +171,7 @@ Section gc.
by apply leibniz_equiv_iff in Hsome.
Qed.
Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto γ l v - own γ ( to_gc_map gcm) - gcm !! l = Some v .
Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v - own (gc_name gG) ( to_gc_map gcm) - gcm !! l = Some v .
Proof.
iIntros "Hgc_l H●".
iCombine "H● Hgc_l" as "Hcomb".
......@@ -174,8 +181,8 @@ Section gc.
by apply gc_map_singleton_included.
Qed.
Lemma gc_access (l: loc) (v: val):
gc_inv γ - gc_mapsto γ l v ={gcN, }= (l v ( w, l w ={, gcN}= gc_mapsto γ l w)).
Lemma gc_access l v:
gc_inv - gc_mapsto l v ={gcN, }= (l v ( w, l w ={, gcN}= gc_mapsto l w)).
Proof.
iIntros "#Hinv Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
......@@ -196,7 +203,7 @@ Section gc.
iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].
Qed.
Lemma is_gc_access (l: loc): gc_inv γ - is_gc_loc γ l ={gcN, }= v, l v (l v ={, gcN}= True).
Lemma is_gc_access l: gc_inv - is_gc_loc l ={gcN, }= v, l v (l v ={, gcN}= True).
Proof.
iIntros "#Hinv Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
......
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