Skip to content
Snippets Groups Projects
Commit 2f2a2219 authored by Ralf Jung's avatar Ralf Jung
Browse files

support (pure) invariants associated with GC locations

parent 44cf491f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/lib/gc.v
+ 107
− 99
View file @ 2f2a2219
......@@ -6,11 +6,15 @@ Set Default Proof Using "Type".
Import uPred.
(** A "GC" location is a location that can never be deallocated explicitly by
the program. It provides a persistent witness that wuill always allow reading
the location, albeit with no way to predict what is going to be read. This is
useful for data structures like RDCSS that need to read locations long after
their ownership has been passed back to the client, but do not care *what* it is
that they are reading in that case.
the program. It provides a persistent witness that will always allow reading
the location. The location is moreover associated with a (pure, Coq-level)
invariant determining which values are allowed to be stored in that location.
The persistent witness cannot know the exact value that will be read, but it
*can* know that the value satisfies the invariant.
This is useful for data structures like RDCSS that need to read locations long
after their ownership has been passed back to the client, but do not care *what*
it is that they are reading in that case.
Note that heap_lang does not actually have explicit dealloaction. However, the
proof rules we provide for heap operations currently are conservative in the
......@@ -18,11 +22,16 @@ sense that they do not expose this fact. By making "GC" locations a separate
assertion, we can keep all the other proofs that do not need it conservative.
*)
Local Notation loc_inv := (val → Prop).
Definition gcN: namespace := nroot .@ "gc".
Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valO.
Definition gc_mapUR : ucmraT := gmapUR loc $ prodR
(optionR $ exclR $ valO)
(agreeR $ leibnizO loc_inv).
Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
Definition to_gc_map (gcm: gmap loc (val * loc_inv)) : gc_mapUR :=
(λ p: val * loc_inv, (Excl' p.1, to_agree p.2)) <$> gcm.
Class gcG (Σ : gFunctors) := GcG {
gc_inG :> inG Σ (authR (gc_mapUR));
......@@ -45,30 +54,34 @@ 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_P : iProp Σ :=
(∃ gcm : gmap loc (val * loc_inv),
own (gc_name gG) (● to_gc_map gcm) ∗ ([∗ map] l ↦ p ∈ gcm, ⌜p.2 p.1⌝ ∗ (l ↦ p.1)) )%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 gc_mapsto (l : loc) (v : val) (I : loc_inv) : iProp Σ :=
own (gc_name gG) (◯ {[l := (Excl' v, to_agree I)]}).
Definition is_gc_loc (l: loc) : iProp Σ := own (gc_name gG) (◯ {[l := None]}).
Definition is_gc_loc (l : loc) (I : loc_inv) : iProp Σ :=
own (gc_name gG) (◯ {[l := (None, to_agree I)]}).
End defs.
Section to_gc_map.
Lemma to_gc_map_valid gcm: ✓ to_gc_map gcm.
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 ∅ = ∅.
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]}.
Lemma to_gc_map_singleton l v I :
to_gc_map {[l := (v, I)]} = {[l := (Excl' v, to_agree I)]}.
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).
Lemma to_gc_map_insert l v I gcm :
to_gc_map (<[l := (v, I)]> gcm) = <[l := (Excl' v, to_agree I)]> (to_gc_map gcm).
Proof. by rewrite /to_gc_map fmap_insert. Qed.
Lemma to_gc_map_delete l gcm :
......@@ -79,59 +92,26 @@ Section to_gc_map.
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).
Lemma lookup_to_gc_map_Some gcm l v I :
gcm !! l = Some (v, I) → to_gc_map gcm !! l = Some (Excl' v, to_agree I).
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.
Lemma lookup_to_gc_map_Some_2 gcm l v' I' :
to_gc_map gcm !! l ≡ Some (v', I') → ∃ v I, v' ≡ Excl' v ∧ I' ≡ to_agree I /\ gcm !! l = Some (v, I).
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.
rewrite /to_gc_map lookup_fmap. rewrite fmap_Some_equiv.
intros ([] & Hsome & [Heqv HeqI]). eauto.
Qed.
End to_gc_map.
Lemma gc_init `{!invG Σ, !heapG Σ, !gcPreG Σ} E:
(|==> ∃ _ : gcG Σ, |={E}=> gc_inv)%I.
⊢ |==> ∃ _ : 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".
iAssert (gc_inv_P (gG := GcG Σ _ γ)) with "[H●]" as "P".
{
iExists _. iFrame.
by iApply big_sepM_empty.
......@@ -142,115 +122,143 @@ Qed.
Section gc.
Context `{!invG Σ, !heapG Σ, !gcG Σ}.
Implicit Types (l : loc) (I : loc_inv).
Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
Global Instance is_gc_loc_persistent l I : Persistent (is_gc_loc l I).
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 I : Timeless (is_gc_loc l I).
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 v I : Timeless (gc_mapsto l v I).
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.
Lemma make_gc l v I E :
↑gcN ⊆ E →
I v →
gc_inv -∗ l ↦ v ={E}=∗ gc_mapsto l v I.
Proof.
iIntros (HN) "#Hinv Hl".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iIntros (HN HI) "#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'"=>//.
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]}))).
apply (auth_update_alloc _ (to_gc_map (<[l := (v, I)]> gcm)) (to_gc_map ({[l := (v, I)]}))).
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]").
iMod ("Hclose" with "[H● HsepM Hl]").
+ iExists _.
iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame. iFrame.
iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame.
auto with 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.
Lemma gc_is_gc l v I : gc_mapsto l v I -∗ is_gc_loc l I.
Proof.
iIntros "Hgc_l". rewrite /gc_mapsto.
assert (Excl' v = (Excl' v) ⋅ None)%I as ->. { done. }
rewrite -op_singleton auth_frag_op own_op.
(* We need to help Coq type inference... *)
change loc_inv with (ofe_car $ leibnizO loc_inv) in I.
(* FIXME: is there any good way to avoid repeating the goal here? *)
assert (◯ {[l := (Excl' v, to_agree I)]} ≡ ◯ {[l := (Excl' v, to_agree I)]} ⋅ ◯ {[l := (None, to_agree I)]}) as ->.
{ rewrite -auth_frag_op op_singleton -pair_op agree_idemp //. }
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⌝.
Lemma is_gc_lookup_Some l gcm I :
is_gc_loc l I -∗ own (gc_name _) (● to_gc_map gcm) -∗ ⌜∃ v, gcm !! l = Some (v, I)⌝.
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].
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.
apply auth_both_valid in Hvalid as [Hincluded Hvalid].
setoid_rewrite singleton_included in Hincluded.
destruct Hincluded as ([v' I'] & Hsome & Hincl).
edestruct lookup_to_gc_map_Some_2 as [v'' [I'' (_ & HI & Hgcm)]]; first done.
rewrite ->HI in Hincl. exists v''. rewrite Hgcm. f_equal.
rewrite ->Some_included_total in Hincl.
apply pair_included in Hincl. simpl in Hincl.
destruct Hincl as [_ Hincl%to_agree_included].
fold_leibniz. subst I''. done.
Qed.
Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v -∗ own (gc_name _) (● to_gc_map gcm) -∗ ⌜ gcm !! l = Some v ⌝.
Lemma gc_mapsto_lookup_Some l v gcm I :
gc_mapsto l v I -∗ own (gc_name _) (● to_gc_map gcm) -∗ ⌜ gcm !! l = Some (v, I) ⌝.
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.
apply auth_both_valid in Hvalid as [Hincluded Hvalid].
setoid_rewrite singleton_included in Hincluded.
destruct Hincluded as ([v' I'] & Hsome & Hincl).
edestruct lookup_to_gc_map_Some_2 as [v'' [I'' (Hv & HI & ->)]]; first done.
rewrite ->HI in Hincl. f_equal.
rewrite ->Some_included_total in Hincl.
apply pair_included in Hincl. simpl in Hincl.
destruct Hincl as [Hinclv HinclI%to_agree_included].
rewrite ->Hv in Hinclv.
apply Excl_included in Hinclv.
fold_leibniz. subst. done.
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:
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)).
gc_inv ={E, E ∖ ↑gcN}=∗ ∀ l v I, gc_mapsto l v I -∗
(⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗ gc_mapsto l w I ∗ |={E ∖ ↑gcN, E}=> True)).
Proof.
iIntros (HN) "#Hinv".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iIntros "!>" (l v) "Hgc_l".
iMod (inv_acc_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iIntros "!>" (l v I) "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".
iDestruct (big_sepM_delete with "HsepM") as "[[HI 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.
{ apply (auth_update _ _ (<[l := (Excl' w, to_agree I)]> (to_gc_map gcm)) {[l := (Excl' w, to_agree I)]}).
apply: singleton_local_update.
{ by apply lookup_to_gc_map_Some in Hsome. }
by apply option_local_update, exclusive_local_update.
apply prod_local_update; simpl.
- by apply option_local_update, exclusive_local_update.
- done.
}
iDestruct (big_sepM_insert with "[Hl HsepM]") as "HsepM"; [ | iFrame | ].
iDestruct (big_sepM_insert _ _ _ (w, I) with "[Hl HsepM]") as "HsepM"; [ | by 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.
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⌝).
Lemma is_gc_access l I E :
↑gcN ⊆ E →
gc_inv -∗ is_gc_loc l I ={E, E ∖ ↑gcN}=∗
∃ v, ⌜I 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]"=>//.
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.
iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"=>//.
iExists _. iFrame "∗#".
iIntros "Hl".
iMod ("Hclose" with "[H● HsepM Hl]"); last done.
iExists _. iFrame.
by (iApply ("HsepM" with "Hl")).
iApply ("HsepM" with "[Hl]"). by iFrame.
Qed.
End gc.
Typeclasses Opaque is_gc_loc gc_mapsto.
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