gc.v 8.06 KB
Newer Older
1 2 3 4 5 6 7 8 9
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".

10
Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valO.
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114

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.
115 116 117
  Context `{!invG Σ, !heapG Σ, !gcG Σ}.

  (* FIXME: still needs a constructor. *)
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162

  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.

163
  Lemma is_gc_lookup_Some  l gcm: is_gc_loc l - own (gc_name _) ( to_gc_map gcm) - ⌜∃ v, gcm !! l = Some v.
164 165 166 167 168 169 170 171 172 173 174
    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.

175
  Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v - own (gc_name _) ( to_gc_map gcm) -  gcm !! l = Some v .
176 177 178 179 180 181 182 183 184
  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.

185 186 187 188 189 190 191
  (** 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)).
192
  Proof.
193
    iIntros (HN) "#Hinv".
194
    iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
195
    iIntros "!>" (l v) "Hgc_l".
196 197 198 199 200 201 202 203 204 205 206 207 208
    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.
209
    iModIntro. iFrame.
210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
    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.