From ddbc49ba9185fa661edb331c7a29aa71e65adcaf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 21:05:19 +0100
Subject: [PATCH] Fractional heap.
---
heap_lang/heap.v | 117 ++++++++++++++++++++++++++++-------------------
1 file changed, 70 insertions(+), 47 deletions(-)
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 14c681b84..b6d415b14 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,5 +1,5 @@
From heap_lang Require Export lifting.
-From algebra Require Import upred_big_op frac.
+From algebra Require Import upred_big_op frac dec_agree.
From program_logic Require Export invariants ghost_ownership.
From program_logic Require Import ownership auth.
Import uPred.
@@ -7,7 +7,7 @@ Import uPred.
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
predicates over finmaps instead of just ownP. *)
-Definition heapRA : cmraT := mapRA loc (exclRA (leibnizC val)).
+Definition heapRA : cmraT := mapRA loc (fracRA (dec_agreeRA val)).
Definition heapGF : iFunctor := authGF heapRA.
Class heapG Σ := HeapG {
@@ -17,13 +17,15 @@ Class heapG Σ := HeapG {
Instance heap_authG `{i : heapG Σ} : authG heap_lang Σ heapRA :=
{| auth_inG := heap_inG |}.
-Definition to_heap : state → heapRA := fmap Excl.
-Definition of_heap : heapRA → state := omap (maybe Excl).
+Definition to_heap : state → heapRA := fmap (λ v, Frac 1 (DecAgree v)).
+Definition of_heap : heapRA → state :=
+ omap (mbind (maybe DecAgree ∘ snd) ∘ maybe2 Frac).
(* heap_mapsto is defined strongly opaquely, to prevent unification from
matching it against other forms of ownership. *)
-Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
- auth_own heap_name {[ l := Excl v ]}.
+Definition heap_mapsto `{heapG Σ}
+ (l : loc)(q : Qp) (v: val) : iPropG heap_lang Σ :=
+ auth_own heap_name {[ l := Frac q (DecAgree v) ]}.
Typeclasses Opaque heap_mapsto.
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
@@ -31,7 +33,9 @@ Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
auth_ctx heap_name N heap_inv.
-Notation "l ↦ v" := (heap_mapsto l v) (at level 20) : uPred_scope.
+Notation "l ↦{ q } v" := (heap_mapsto l q v)
+ (at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
+Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : iFunctorG}.
@@ -50,27 +54,45 @@ Section heap.
Qed.
Lemma to_heap_valid σ : ✓ to_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
- Lemma of_heap_insert l v h : of_heap (<[l:=Excl v]> h) = <[l:=v]> (of_heap h).
- Proof. by rewrite /of_heap -(omap_insert _ _ _ (Excl v)). Qed.
- Lemma to_heap_insert l v σ : to_heap (<[l:=v]> σ) = <[l:=Excl v]> (to_heap σ).
+ Lemma of_heap_insert l v h :
+ of_heap (<[l:=Frac 1 (DecAgree v)]> h) = <[l:=v]> (of_heap h).
+ Proof. by rewrite /of_heap -(omap_insert _ _ _ (Frac 1 (DecAgree v))). Qed.
+ Lemma of_heap_singleton_op l q v h :
+ ✓ ({[l := Frac q (DecAgree v)]} ⋅ h) →
+ of_heap ({[l := Frac q (DecAgree v)]} â‹… h) = <[l:=v]> (of_heap h).
+ Proof.
+ intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|].
+ - move: (Hv l). rewrite /of_heap lookup_insert
+ lookup_omap (lookup_op _ h) lookup_singleton.
+ case _:(h !! l)=>[[q' [v'|]|]|] //=; last by move=> [??].
+ move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
+ - rewrite /of_heap lookup_insert_ne // !lookup_omap.
+ by rewrite (lookup_op _ h) lookup_singleton_ne // left_id.
+ Qed.
+ Lemma to_heap_insert l v σ :
+ to_heap (<[l:=v]> σ) = <[l:=Frac 1 (DecAgree v)]> (to_heap σ).
Proof. by rewrite /to_heap -fmap_insert. Qed.
Lemma of_heap_None h l :
- ✓ h → of_heap h !! l = None → h !! l = None ∨ h !! l ≡ Some ExclUnit.
+ ✓ h → of_heap h !! l = None → h !! l = None ∨ h !! l ≡ Some FracUnit.
Proof.
move=> /(_ l). rewrite /of_heap lookup_omap.
- by case: (h !! l)=> [[]|]; auto.
+ by case: (h !! l)=> [[q [v|]|]|] //=; destruct 1; auto.
Qed.
- Lemma heap_singleton_inv_l h l v :
- ✓ ({[l := Excl v]} ⋅ h) → h !! l = None ∨ h !! l ≡ Some ExclUnit.
+ Lemma heap_store_valid l h v1 v2 :
+ ✓ ({[l := Frac 1 (DecAgree v1)]} ⋅ h) →
+ ✓ ({[l := Frac 1 (DecAgree v2)]} ⋅ h).
Proof.
- move=> /(_ l). rewrite lookup_op lookup_singleton.
- by case: (h !! l)=> [[]|]; auto.
+ intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
+ - rewrite !lookup_op !lookup_singleton.
+ case: (h !! l)=>[x|]; [|done]=> /frac_valid_inv_l=>-> //.
+ - by rewrite !lookup_op !lookup_singleton_ne.
Qed.
+ Hint Resolve heap_store_valid.
(** Allocation *)
Lemma heap_alloc E N σ :
authG heap_lang Σ heapRA → nclose N ⊆ E →
- ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} heap_mapsto).
+ ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} (λ l v, l ↦ v)).
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro.
@@ -95,11 +117,19 @@ Section heap.
Proof. solve_proper. Qed.
(** General properties of mapsto *)
- Lemma heap_mapsto_disjoint l v1 v2 : (l ↦ v1 ★ l ↦ v2)%I ⊑ False.
+ Lemma heap_mapsto_op_eq l q1 q2 v :
+ (l ↦{q1} v ★ l ↦{q2} v)%I ≡ (l ↦{q1+q2} v)%I.
+ Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.
+
+ Lemma heap_mapsto_op l q1 q2 v1 v2 :
+ (l ↦{q1} v1 ★ l ↦{q2} v2)%I ≡ (v1 = v2 ∧ l ↦{q1+q2} v1)%I.
Proof.
- rewrite -auth_own_op auth_own_valid map_op_singleton.
- rewrite map_validI (forall_elim l) lookup_singleton.
- by rewrite option_validI excl_validI.
+ destruct (decide (v1 = v2)) as [->|].
+ { by rewrite heap_mapsto_op_eq const_equiv // left_id. }
+ rewrite -auth_own_op map_op_singleton Frac_op dec_agree_ne //.
+ apply (anti_symm (⊑)); last by apply const_elim_l.
+ rewrite auth_own_valid map_validI (forall_elim l) lookup_singleton.
+ rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
Qed.
(** Weakest precondition *)
@@ -120,29 +150,28 @@ Section heap.
apply sep_mono_r; rewrite HP; apply later_mono.
apply forall_mono=> l; apply wand_intro_l.
rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
- rewrite -(exist_intro (op {[ l := Excl v ]})).
+ rewrite -(exist_intro (op {[ l := Frac 1 (DecAgree v) ]})).
repeat erewrite <-exist_intro by apply _; simpl.
rewrite -of_heap_insert left_id right_id.
rewrite /heap_mapsto. ecancel [_ -★ Φ _]%I.
rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
- rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
- apply later_intro.
+ rewrite const_equiv; last by apply (map_insert_valid h).
+ by rewrite left_id -later_intro.
Qed.
- Lemma wp_load N E l v P Φ :
+ Lemma wp_load N E l q v P Φ :
P ⊑ heap_ctx N → nclose N ⊆ E →
- P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Φ v)) →
+ P ⊑ (▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) →
P ⊑ || Load (Loc l) @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
- with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
+ with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
rewrite const_equiv // left_id.
- rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
- rewrite -of_heap_insert.
+ rewrite /heap_inv of_heap_singleton_op //.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Qed.
@@ -153,33 +182,30 @@ Section heap.
P ⊑ || Store (Loc l) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ??? HPΦ.
- apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
- with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
+ apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
+ with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
- rewrite /heap_inv alter_singleton insert_insert.
- rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
- rewrite -!of_heap_insert const_equiv;
- last (split; [naive_solver|by eapply map_insert_valid, cmra_valid_op_r]).
+ rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
+ rewrite const_equiv; last naive_solver.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Qed.
- Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Φ :
+ Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 P Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠v1 →
P ⊑ heap_ctx N → nclose N ⊆ E →
- P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Φ (LitV (LitBool false)))) →
+ P ⊑ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) →
P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=>????? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
- with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
+ with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
rewrite const_equiv // left_id.
- rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
- rewrite -of_heap_insert.
+ rewrite /heap_inv !of_heap_singleton_op //.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Qed.
@@ -190,17 +216,14 @@ Section heap.
P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ???? HPΦ.
- apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
- with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
+ apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
+ with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
last by rewrite lookup_insert.
- rewrite /heap_inv alter_singleton insert_insert.
- rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
- rewrite -!of_heap_insert const_equiv; last first.
- { split; last by eapply map_insert_valid, cmra_valid_op_r.
- eexists; rewrite lookup_insert; naive_solver. }
+ rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
+ rewrite lookup_insert const_equiv; last naive_solver.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Qed.
End heap.
--
GitLab