Commit 87adc879 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More consistent names in locking_heap.

parent dcf68bdf
......@@ -14,8 +14,8 @@ Canonical Structure lvlC := leibnizC lvl.
Instance lvl_EqDecision : EqDecision lvl.
Proof. solve_decision. Defined.
Instance lvl_op : Op lvl := λ l1 l2,
match l1, l2 with
Instance lvl_op : Op lvl := λ lv1 lv2,
match lv1, lv2 with
| ULvl,_ => ULvl
| _,ULvl => ULvl
| _,_ => LLvl
......@@ -23,27 +23,25 @@ Instance lvl_op : Op lvl := λ l1 l2,
Instance lvl_valid : Valid lvl := λ _, True.
Instance lvl_unit : Unit lvl := LLvl.
Instance lvl_pcore : PCore lvl := λ _, Some LLvl.
Instance lvl_equiv : Equiv lvl := λ l1 l2, l1 = l2.
Lemma lvl_included (x y : lvl) :
x y x = y x = LLvl y = ULvl.
Lemma lvl_included lv1 lv2 : lv1 lv2 lv1 = lv2 lv1 = LLvl lv2 = ULvl.
Proof.
split.
- intros [z ->%leibniz_equiv]. destruct x, z; naive_solver.
- intros [->|[-> ->]]. exists y. by destruct y. by exists ULvl.
- intros [[] ->%leibniz_equiv]; destruct lv1; naive_solver.
- intros [->|[-> ->]]. exists lv2. by destruct lv2. by exists ULvl.
Qed.
Lemma lvl_idemp (x : lvl) : x x = x.
Proof. by destruct x. Qed.
Lemma lvl_idemp (lv : lvl) : lv lv = lv.
Proof. by destruct lv. Qed.
Lemma lvl_ra_mixin : RAMixin lvl.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
- intros x y z. destruct x,y,z; compute; done.
- intros x y. destruct x,y; compute; done.
- intros [|]; compute; reflexivity.
- intros x y Hxy%lvl_included.
apply lvl_included. destruct x, y; compute; firstorder.
- by intros [] [] [].
- by intros [] [].
- by intros [].
- intros lv1 lv2 ?%lvl_included.
apply lvl_included. destruct lv1, lv2; compute; firstorder.
Qed.
Canonical Structure lvlR : cmraT := discreteR lvl lvl_ra_mixin.
......@@ -51,10 +49,7 @@ Global Instance lvl_cmra_discrete : CmraDiscrete lvlR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma lvl_ucmra_mixin : UcmraMixin lvl.
Proof.
split; try (apply _ || done).
intros [|]; done.
Qed.
Proof. split; try (apply _ || done). by intros []. Qed.
Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin.
(* Auth (Loc -> (Q * Level)) *)
......@@ -79,44 +74,43 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Definition to_locking_heap (σ : gmap loc (lvl*val)) : locking_heapUR :=
fmap (λ '(b,v), (1%Qp, b, to_agree v)) σ.
Definition to_locking_heap (σ : gmap loc (lvl * val)) : locking_heapUR :=
fmap (λ '(lv,v), (1%Qp, lv, to_agree v)) σ.
Definition is_lock_lvl (a : loc * (lvl*val)) : bool :=
Definition is_lock_lvl (a : loc * (lvl * val)) : bool :=
match a.2.1 with
| LLvl => true
| ULvl => false
end.
(* σ^{-1}(L) *)
Definition locked_locs (σ : gmap loc (lvl*val)) : gset loc :=
Definition locked_locs (σ : gmap loc (lvl * val)) : gset loc :=
dom (gset loc) (filter is_lock_lvl σ).
Definition full_locking_heap (σ : gmap loc (lvl*val)) :=
(own (@lheap_name _ hG) ( (to_locking_heap σ))
[ map] lbvσ, l bv.2)%I.
Definition full_locking_heap (σ : gmap loc (lvl * val)) :=
(own lheap_name ( (to_locking_heap σ)) [ map] lbvσ, l bv.2)%I.
Definition mapsto_def (l : loc) (b : lvl) (q : frac) (v: val) : iProp Σ :=
( b' : lvl, b b'
own (@lheap_name _ hG) ( {[ l := (q, b', to_agree v) ]}))%I.
Definition mapsto_def (l : loc) (lv : lvl) (q : frac) (v: val) : iProp Σ :=
( lv' : lvl, lv lv'
own lheap_name ( {[ l := (q, lv', to_agree v) ]}))%I.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
End definitions.
Notation "l ↦C[ x ]{ q } v" :=
(mapsto l x q%Qp v%V)
(at level 20, x, q at level 50, format "l ↦C[ x ]{ q } v") : bi_scope.
Notation "l ↦C[ x ] v" := (l C[x]{1} v)%I
(at level 20, x at level 50, format "l ↦C[ x ] v") : bi_scope.
Notation "l ↦C[ lv ]{ q } v" :=
(mapsto l lv q%Qp v%V)
(at level 20, lv, q at level 50, format "l ↦C[ lv ]{ q } v") : bi_scope.
Notation "l ↦C[ lv ] v" := (l C[lv]{1} v)%I
(at level 20, lv at level 50, format "l ↦C[ lv ] v") : bi_scope.
Notation "l ↦C{ q } v" := (l C[ULvl]{q} v)%I
(at level 20, q at level 50, format "l ↦C{ q } v") : bi_scope.
Notation "l ↦C v" := (l C[ULvl]{1} v)%I
(at level 20, format "l ↦C v") : bi_scope.
Lemma to_locking_heap_valid (σ : gmap loc (lvl*val)) : to_locking_heap σ.
Proof. intros l. rewrite lookup_fmap. destruct (σ !! l) as [[b v]|]; done. Qed.
Lemma to_locking_heap_valid (σ : gmap loc (lvl * val)) : to_locking_heap σ.
Proof. intros l. rewrite lookup_fmap. by destruct (σ !! l) as [[]|]. Qed.
Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
(|==> _ : locking_heapG Σ, full_locking_heap )%I.
......@@ -129,79 +123,70 @@ Qed.
Section properties.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Implicit Type σ : gmap loc (lvl*val).
Implicit Type x y : lvl.
Implicit Type σ : gmap loc (lvl * val).
Implicit Type lv : lvl.
Implicit Type l : loc.
Global Instance mapsto_timeless l x q v : Timeless (mapsto l x q v).
Global Instance mapsto_timeless l lv q v : Timeless (l C[lv]{q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l x v : Fractional (λ q, l C[x]{q} v)%I.
Global Instance mapsto_fractional l lv v : Fractional (λ q, l C[lv]{q} v)%I.
Proof.
intros p q. rewrite mapsto_eq /mapsto_def.
iSplit.
- iDestruct 1 as (b') "(#Hb & Ho)".
rewrite -{2}(lvl_idemp b').
iDestruct "Ho" as "[Ho Ho']".
iSplitL "Ho"; eauto.
intros p q. rewrite mapsto_eq /mapsto_def. iSplit.
- iDestruct 1 as (lv' ?) "Hl". rewrite -(lvl_idemp lv').
iDestruct "Hl" as "[Hl Hl']". iSplitL "Hl"; eauto.
- iIntros "[H1 H2]".
iDestruct "H1" as (b1) "(#Hb1 & Ho1)".
iDestruct "H2" as (b2) "(#Hb2 & Ho2)".
iCombine "Ho1 Ho2" as "Ho".
rewrite frac_op'. iExists (b1 b2). iFrame.
destruct b1,b2; eauto.
iDestruct "H1" as (lv1 ?) "Hl1". iDestruct "H2" as (lv2 ?) "Hl2".
iCombine "Hl1 Hl2" as "Hl".
rewrite frac_op'. iExists (lv1 lv2). iFrame. destruct lv1,lv2; eauto.
Qed.
Global Instance mapsto_as_fractional l q x v :
AsFractional (mapsto l x q v) (λ q, l C[x]{q} v)%I q.
Global Instance mapsto_as_fractional l q lv v :
AsFractional (l C[lv]{q} v) (λ q, l C[lv]{q} v)%I q.
Proof. split. done. apply _. Qed.
Lemma mapsto_downgrade' x y l q v : x y l C[y]{q} v - l C[x]{q} v.
Lemma mapsto_downgrade' lv lv' l q v : lv lv' l C[lv']{q} v - l C[lv]{q} v.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (b' ?) "Ho".
iExists b'. iSplit; eauto.
iPureIntro. transitivity y; done.
iDestruct 1 as (lv'' ?) "Ho".
iExists lv''. iSplit; eauto. iPureIntro. by transitivity lv'.
Qed.
Lemma mapsto_downgrade x l q v : l C{q} v - l C[x]{q} v.
Proof. apply mapsto_downgrade'. apply lvl_included. destruct x; eauto. Qed.
Lemma mapsto_downgrade lv l q v : l C{q} v - l C[lv]{q} v.
Proof. apply mapsto_downgrade'. apply lvl_included. destruct lv; eauto. Qed.
Lemma mapsto_value_agree x x' l q q' v v' : l C[x]{q} v - l C[x']{q'} v' - v = v'.
Lemma mapsto_value_agree lv lv' l q q' v v' :
l C[lv]{q} v - l C[lv']{q'} v' - v = v'.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (b1 ?) "Ho1".
iDestruct 1 as (b2 ?) "Ho2".
iCombine "Ho1 Ho2" as "Ho".
rewrite own_valid discrete_valid.
iDestruct "Ho" as %Ho. iPureIntro. revert Ho.
move=> /auth_own_valid /=. rewrite singleton_valid.
by intros [_ ?%agree_op_invL'].
iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2".
iDestruct (own_valid_2 with "Hl1 Hl2") as %Ho%auth_own_valid. iPureIntro.
revert Ho. rewrite /= op_singleton singleton_valid. by intros [_ ?%agree_op_invL'].
Qed.
Lemma mapsto_combine x x' l q q' v : l C[x]{q} v - l C[x']{q'} v - l C[x x']{q+q'} v.
Lemma mapsto_combine lv lv' l q q' v :
l C[lv]{q} v - l C[lv']{q'} v - l C[lvlv']{q+q'} v.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (b1 Hb1) "Ho1".
iDestruct 1 as (b2 Hb2) "Ho2".
iExists (b1 b2). iSplitR.
{ iPureIntro. destruct x,x',b1,b2; eauto. }
iCombine "Ho1 Ho2" as "Ho". rewrite frac_op'. iFrame.
iDestruct 1 as (lv1 ?) "Hl1". iDestruct 1 as (lv2 ?) "Hl2".
iExists (lv1 lv2). iSplitR.
{ iPureIntro. destruct lv,lv',lv1,lv2; eauto. }
iCombine "Hl1 Hl2" as "Hl". rewrite frac_op'. iFrame.
Qed.
Global Instance from_sep_mapsto l x x' q q' v :
FromSep (l C[xx']{q+q'} v) (l C[x]{q} v) (l C[x']{q'} v).
Global Instance from_sep_mapsto l lv lv' q q' v :
FromSep (l C[lvlv']{q+q'} v) (l C[lv]{q} v) (l C[lv']{q'} v).
Proof.
rewrite /FromSep. iIntros "[Hl1 Hl2]".
iApply (mapsto_combine with "Hl1 Hl2").
Qed.
Lemma to_locking_heap_insert σ l x v :
to_locking_heap (<[l := (x,v)]> σ) = <[l := (1%Qp, x, to_agree v)]>(to_locking_heap σ).
Lemma to_locking_heap_insert σ l lv v :
to_locking_heap (<[l := (lv,v)]> σ) = <[l := (1%Qp, lv, to_agree v)]>(to_locking_heap σ).
Proof. by rewrite /to_locking_heap fmap_insert. Qed.
Lemma to_locking_heap_lookup_Some σ l x v :
σ !! l = Some (x,v) to_locking_heap σ !! l = Some (1%Qp, x, to_agree v).
Lemma to_locking_heap_lookup_Some σ l lv v :
σ !! l = Some (lv,v) to_locking_heap σ !! l = Some (1%Qp, lv, to_agree v).
Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Lemma to_locking_heap_lookup_None σ l :
σ !! l = None to_locking_heap σ !! l = None.
......@@ -232,14 +217,14 @@ Section properties.
rewrite !map_filter_lookup_Some lookup_insert_Some. naive_solver.
Qed.
Lemma heap_singleton_included σ l x q v :
{[l := (q, x, to_agree v)]} (to_locking_heap σ) y, x y σ !! l = Some (y, v).
Lemma heap_singleton_included σ l lv q v :
{[l := (q, lv, to_agree v)]} to_locking_heap σ
lv', lv lv' σ !! l = Some (lv', v).
Proof.
rewrite singleton_included=> -[[[q' b] av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[[b' av'] [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [/Some_pair_included_total_2] [_] Hxb' Hp.
apply to_agree_included in Hp. fold_leibniz. subst.
by exists b'.
rewrite singleton_included=> -[[[q' lv'] av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[[lv'' av'] [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [/Some_pair_included_total_2] [_] Hxb'.
move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''.
Qed.
Lemma locked_locs_unlocked σ l v q :
......@@ -277,16 +262,16 @@ Section properties.
eauto.
Qed.
Lemma locking_heap_change_lock (l : loc) (v : val) (x y : lvl) σ :
full_locking_heap σ - l C[x] v
== full_locking_heap (<[l:=(y,v)]>σ) l C[y] v.
Lemma locking_heap_change_lock l v lv lv' σ :
full_locking_heap σ - l C[lv] v
== full_locking_heap (<[l:=(lv',v)]>σ) l C[lv'] v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def.
iIntros "[Hfull Hmap]". iDestruct 1 as (b') "(#Hb & Hpart)".
iDestruct (own_valid_2 with "Hfull Hpart")
as %[[z [Hz%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hfull Hpart") as "Hfull".
{ apply (auth_update _ _ (to_locking_heap (<[l:=(y,v)]>σ)) {[l := (1%Qp, y, to_agree v)]}).
{ apply (auth_update _ _ (to_locking_heap (<[l:=(lv',v)]>σ)) {[l := (1%Qp, lv', to_agree v)]}).
rewrite to_locking_heap_insert.
eapply singleton_local_update; first by eapply to_locking_heap_lookup_Some.
by apply exclusive_local_update. }
......@@ -297,9 +282,9 @@ Section properties.
rewrite lookup_fmap Hl //.
Qed.
Lemma locking_heap_unlock (l : loc) (v : val) (x : lvl) (q : frac) σ :
full_locking_heap σ - l C[x]{q} v
== full_locking_heap (<[l:=(ULvl,v)]>σ) l C{q} v.
Lemma locking_heap_unlock l v lv q σ :
full_locking_heap σ - l C[lv]{q} v ==
full_locking_heap (<[l:=(ULvl,v)]>σ) l C{q} v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def.
iIntros "[Hfull Hmap]". iDestruct 1 as (b') "(#Hb' & Hpart)".
......@@ -319,14 +304,14 @@ Section properties.
rewrite lookup_fmap Hl //.
Qed.
Lemma locking_heap_alloc σ l x v :
Lemma locking_heap_alloc σ l lv v :
σ !! l = None
l v - full_locking_heap σ == full_locking_heap (<[l:=(x,v)]>σ) l C[ x ] v.
l v - full_locking_heap σ == full_locking_heap (<[l:=(lv,v)]>σ) l C[lv] v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def.
iIntros (?) "Hl [Hauth Hmap]".
iMod (own_update with "Hauth") as "Hauth".
{ eapply (auth_update_alloc _ (to_locking_heap (<[l:=(x,v)]> σ)) {[l := (1%Qp, x, to_agree v)]}).
{ eapply (auth_update_alloc _ (to_locking_heap (<[l:=(lv,v)]> σ)) {[l := (1%Qp, lv, to_agree v)]}).
rewrite to_locking_heap_insert.
apply alloc_singleton_local_update; last done.
by apply to_locking_heap_lookup_None. }
......
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