From 787080a0e8660aad7982544de6d0c5290b03a88d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 Jun 2019 13:15:16 +0200
Subject: [PATCH] GC-location library by Gaurav

---
 _CoqProject               |   1 +
 theories/logatom/lib/gc.v | 221 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 222 insertions(+)
 create mode 100644 theories/logatom/lib/gc.v

diff --git a/_CoqProject b/_CoqProject
index a51673bd..cffa7ccb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -91,6 +91,7 @@ theories/hocap/lib/oneshot.v
 theories/hocap/concurrent_runners.v
 theories/hocap/parfib.v
 
+theories/logatom/lib/gc.v
 theories/logatom/treiber.v
 theories/logatom/treiber2.v
 theories/logatom/elimination_stack/hocap_spec.v
diff --git a/theories/logatom/lib/gc.v b/theories/logatom/lib/gc.v
new file mode 100644
index 00000000..ea371171
--- /dev/null
+++ b/theories/logatom/lib/gc.v
@@ -0,0 +1,221 @@
+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) := 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_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.
+
+Section gc.
+  Context `{!invG Σ, !heapG Σ, gG: 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_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 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.
+    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 gG) (● 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.
+
+  Lemma gc_access l v E:
+    ↑gcN ⊆ E → gc_inv -∗ gc_mapsto l v ={E, E ∖ ↑gcN}=∗ (l ↦ v ∗ (∀ w, l ↦ w ={E ∖ ↑gcN, E}=∗ gc_mapsto l w)).
+  Proof.
+    iIntros (HN) "#Hinv Hgc_l".
+    iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
+    iModIntro.
+    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.
+    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.
-- 
GitLab