Commit 143a66ca authored by Dan Frumin's avatar Dan Frumin
Browse files

New locking heap representation

- Use the level resource algebra/lattice.
  This allows us to unlock partially owned locations
- Upclose the mapsto predicates.
  This allows us to "downgrade" unlocked locations.
parent ad1df34c
......@@ -110,14 +110,10 @@ Section proofs.
wp_let. wp_proj.
wp_apply (mset_add_spec with "[$HX]"); eauto.
iIntros "HX". wp_seq.
iAssert (⌜σ !! l = Some ULvl%I) with "[Hσ Hv]" as %?.
{ rewrite mapsto_eq /mapsto_def.
iDestruct "Hv" as "[Hv Hl]".
by iDestruct (own_valid_2 with "Hσ Hl")
as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
iDestruct (full_locking_heap_unlocked with "Hv Hσ") as %?.
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hv") as "[Hσ Hv]".
do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
iDestruct "Hv" as "[Hv Hl]".
iDestruct "Hv" as (b') "(Hb' & Hv & Hl)".
rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
......@@ -133,7 +129,8 @@ Section proofs.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
- iApply "HΦ". iFrame.
- iApply "HΦ". iFrame. iExists b'; iSplit; eauto.
iPureIntro. apply lvl_included. destruct b'; eauto.
Qed.
Lemma a_load_spec R Φ q e :
......@@ -159,11 +156,13 @@ Section proofs.
wp_apply (mset_member_spec #l env with "HX").
iIntros "Henv /=". case_decide; first by exfalso. simpl.
wp_op. iSplit; eauto. iNext. wp_seq.
rewrite mapsto_eq /mapsto_def. iDestruct "Hl" as "[Hv Hl]". wp_load.
rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as (b') "(% & Hv & Hl)".
wp_load.
iCombine "Hv Hl" as "Hv". iFrame "HR".
iSplitR "HΦ Hv".
- iExists X,σ. by iFrame.
- by iApply "HΦ".
- iApply "HΦ". iExists b'. iSplit; eauto.
Qed.
Lemma a_un_op_spec R Φ e op:
......@@ -210,18 +209,14 @@ Section proofs.
iNext. iIntros "HX".
iDestruct "HΦ" as (us) "[Hus HΦ]".
clear Hlocks.
iInduction us as [|u us] "IH" forall (σ); simpl.
iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
- iModIntro. iFrame "HR". iSplitR "HΦ".
+ iExists , σ. iFrame. iPureIntro.
rewrite /correct_locks /set_Forall. set_solver.
+ by iApply "HΦ".
- iDestruct "Hus" as "[Hu Hus]".
iAssert (⌜σ !! u.1 = Some LLvl%I) with "[Hσ Hu]" as %?.
{ rewrite mapsto_eq /mapsto_def.
iDestruct "Hu" as "[Hu Hl]".
by iDestruct (own_valid_2 with "Hσ Hl")
as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]".
iDestruct (full_locking_heap_present with "Hu Hσ") as %[z Hz].
iMod (locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX").
{ iIntros "Hus". iApply "HΦ". by iFrame. }
{ rewrite -big_sepM_insert_override; eauto. }
......
......@@ -8,9 +8,9 @@ Section contents.
(** * Unlocking modality *)
Definition U (P : iProp Σ) : iProp Σ :=
( ls : list (loc*val),
([ list] x ls, x.1 L x.2)
(([ list] x ls, x.1 U x.2) - P))%I.
( ls : list (loc*(frac*val)),
([ list] x ls, x.1 L{x.2.1} x.2.2)
(([ list] x ls, x.1 U{x.2.1} x.2.2) - P))%I.
Lemma U_mono P Q : (P Q) U P U Q.
Proof.
......@@ -50,9 +50,9 @@ Section contents.
iApply ("HP2" with "HP1").
Qed.
Lemma U_unlock l v : l L v U (l U v).
Lemma U_unlock l q v : l L{q} v U (l U{q} v).
Proof.
iIntros "Hl". iExists [(l,v)]. iIntros "/= {$Hl} [$ _]".
iIntros "Hl". iExists [(l,(q,v))]. iIntros "/= {$Hl} [$ _]".
Qed.
Class IntoUnlock (P Q : iProp Σ) := into_unlock : P U Q.
......@@ -60,7 +60,7 @@ Section contents.
Proof. rewrite /IntoUnlock. reflexivity. Qed.
Global Instance into_unlock_id P : IntoUnlock P P | 10.
Proof. apply U_intro. Qed.
Global Instance into_unlock_unlock l v : IntoUnlock (l L v)%I (l U v)%I | 0.
Global Instance into_unlock_unlock l q v : IntoUnlock (l L{q} v)%I (l U{q} v)%I | 0.
Proof. apply U_unlock. Qed.
Lemma modality_U_mixin :
......
......@@ -11,9 +11,56 @@ Inductive level : Set :=
| ULvl : level.
Canonical Structure lvlC := leibnizC level.
(* Auth (Loc -> (Q * Agree Level)) *)
Instance level_EqDecision : EqDecision level.
Proof. solve_decision. Defined.
Instance level_op : Op level := λ l1 l2,
match l1, l2 with
| ULvl,_ => ULvl
| _,ULvl => ULvl
| _,_ => LLvl
end.
Instance level_valid : Valid level := λ _, True.
Instance level_unit : Unit level := LLvl.
Instance level_pcore : PCore level := λ _, Some LLvl.
Instance level_equiv : Equiv level := λ l1 l2, l1 = l2.
Lemma lvl_included (x y : level) :
x y (x = y \/ (x = LLvl /\ y = ULvl)).
Proof.
destruct x; compute; firstorder.
destruct y; firstorder.
exists LLvl; eauto.
exists ULvl; eauto.
Qed.
Lemma lvl_idemp (x : level) : x x = x.
Proof. by destruct x. Qed.
Lemma lvl_ra_mixin : RAMixin level.
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.
Qed.
Canonical Structure lvlR : cmraT := discreteR level lvl_ra_mixin.
Global Instance lvl_cmra_discrete : CmraDiscrete lvlR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma lvl_ucmra_mixin : UcmraMixin level.
Proof.
split; try (apply _ || done).
intros [|]; done.
Qed.
Canonical Structure lvlUR : ucmraT := UcmraT level lvl_ucmra_mixin.
(* Auth (Loc -> (Q * Level)) *)
Definition locking_heapUR : ucmraT :=
gmapUR loc (prodR fracR (agreeR lvlC)).
gmapUR loc (prodR fracR lvlUR).
(** The CMRA we need. *)
Class locking_heapG (Σ : gFunctors) := LHeapG {
......@@ -34,7 +81,7 @@ Section definitions.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Definition to_locking_heap (σ : gmap loc level) : locking_heapUR :=
fmap (λ x, (1%Qp, to_agree x)) σ.
fmap (λ x, (1%Qp, x)) σ.
Definition is_lock_lvl (a : loc * level) : bool :=
match (snd a) with
......@@ -50,17 +97,17 @@ Section definitions.
own (@lheap_name _ hG) ( (to_locking_heap σ)).
Definition mapsto_def (l : loc) (b : level) (q : frac) (v: val) : iProp Σ :=
(l {q*(1/2)} v
own (@lheap_name _ hG) ( {[ l := (q, to_agree b) ]}))%I.
( b' : level, b b' l {q*(1/2)} v
own (@lheap_name _ hG) ( {[ l := (q, b') ]}))%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 ↦[ x & q ] v" := (mapsto l x q%Qp v%V)
(at level 20, q at level 50, format "l ↦[ x & q ] v") : uPred_scope.
Notation "l ↦[ x ] v" := (mapsto l x 1%Qp v%V)
Local Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, x at level 50, q at level 50, format "l ↦( x , q ) v") : bi_scope.
Notation "l ↦[ x ] v" := (l (x,1) v)%I
(at level 20, x at level 50, format "l ↦[ x ] v") : bi_scope.
Notation "l ↦L v" := (l [LLvl] v)%I
(at level 20, format "l ↦L v") : bi_scope.
......@@ -95,29 +142,46 @@ Section properties.
Global Instance mapsto_timeless l x q v : Timeless (mapsto l x q v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l x v : Fractional (λ q, mapsto l x q v)%I.
Proof.
intros p q. rewrite mapsto_eq /mapsto_def.
assert ((p + q) * (1 / 2) = (p * (1 / 2)) + (q * (1 / 2)))%Qp as ->.
{ apply Qp_mult_plus_distr_l. }
iSplit.
- iIntros "[Hl Ho]".
- iDestruct 1 as (b') "(#Hb & Hl & Ho)".
(* iIntros "(Hl & Ho)". *)
iDestruct "Hl" as "[$ $]".
rewrite -own_op -auth_frag_op op_singleton pair_op agree_idemp. done.
- iIntros "[[Hl1 Ho1] [Hl2 Ho2]]".
iCombine "Hl1 Hl2" as "Hl". iFrame.
iCombine "Ho1 Ho2" as "$".
rewrite -{2}(lvl_idemp b').
iDestruct "Ho" as "[Ho Ho']".
iSplitL "Ho"; 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.
Qed.
Global Instance mapsto_as_fractional l q x v :
AsFractional (mapsto l x q v) (λ q, mapsto l x q v)%I q.
Proof. split. done. apply _. Qed.
Lemma mapsto_downgrade x l q v : l U{q} v - l (x,q) v.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (b') "(% & $ & Ho)".
iExists b'. iSplit; eauto.
iPureIntro. transitivity ULvl; last done.
apply lvl_included. destruct x; eauto.
Qed.
Lemma to_locking_heap_insert σ l x :
to_locking_heap (<[l := x]> σ) = <[l := (1%Qp, to_agree x)]>(to_locking_heap σ).
to_locking_heap (<[l := x]> σ) = <[l := (1%Qp, x)]>(to_locking_heap σ).
Proof. by rewrite /to_locking_heap fmap_insert. Qed.
Lemma to_locking_heap_lookup_Some σ l x :
σ !! l = Some x to_locking_heap σ !! l = Some (1%Qp, to_agree x).
σ !! l = Some x to_locking_heap σ !! l = Some (1%Qp, x).
Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Lemma to_locking_heap_lookup_None σ l :
σ !! l = None to_locking_heap σ !! l = None.
......@@ -169,34 +233,47 @@ Section properties.
Qed.
Lemma heap_singleton_included (σ : gmap loc level) l x q :
{[l := (q, to_agree x)]} (to_locking_heap σ) σ !! l = Some x.
{[l := (q, x)]} (to_locking_heap σ) y, x y σ !! l = Some y.
Proof.
rewrite singleton_included=> -[[q' av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[y [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] Hxy.
exists y; done.
Qed.
Lemma locked_locs_locked σ l v q :
l L{q} v - full_locking_heap σ - l locked_locs σ⌝.
Lemma locked_locs_unlocked σ l v q :
l U{q} v - full_locking_heap σ - l locked_locs σ⌝.
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iIntros "[Hl Hpart] Hfull".
iDestruct 1 as (b') "(Hb' & Hl & Hpart)". iIntros "Hfull".
iDestruct "Hb'" as %Hb'%lvl_included.
iDestruct (own_valid_2 with "Hfull Hpart")
as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
as %[[y [Hy%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2.
assert (y = ULvl) as -> by (destruct y; eauto; inversion Hy; inversion Hb'; naive_solver).
iPureIntro. rewrite /locked_locs.
eapply elem_of_dom_2. apply map_filter_lookup_Some. eauto.
eapply not_elem_of_dom. apply map_filter_lookup_None.
right. intros. simplify_eq/=. eauto.
Qed.
Lemma locked_locs_unlocked σ l v q :
l U{q} v - full_locking_heap σ - l locked_locs σ.
Lemma full_locking_heap_unlocked σ l v q :
l U{q} v - full_locking_heap σ - σ !! l = Some ULvl.
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iIntros "[Hl Hpart] Hfull".
iDestruct 1 as (b') "(Hb' & Hl & Hpart)". iIntros "Hfull".
iDestruct "Hb'" as %Hb'%lvl_included.
iDestruct (own_valid_2 with "Hfull Hpart")
as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
iPureIntro. rewrite /locked_locs.
eapply not_elem_of_dom. apply map_filter_lookup_None.
right. intros. simplify_eq/=. eauto.
as %[[y [Hy%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2.
iPureIntro. naive_solver.
Qed.
Lemma full_locking_heap_present σ l v q :
l L{q} v - full_locking_heap σ - is_Some (σ !! l).
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iDestruct 1 as (b') "(#Hb & Hl & Hpart)". iIntros "Hfull".
iDestruct (own_valid_2 with "Hfull Hpart")
as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2.
eauto.
Qed.
Lemma locking_heap_change_lock (l : loc) (v : val) (x y : level) σ :
......@@ -204,15 +281,33 @@ Section properties.
== full_locking_heap (<[l:=y]>σ) l [ y ] v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def.
iIntros "Hauth ($ & Hl)".
iDestruct (own_valid_2 with "Hauth Hl")
as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hauth Hl") as "Hauth".
{ apply (auth_update _ _ (to_locking_heap (<[l:=y]>σ)) {[l := (1%Qp, to_agree y)]}).
iIntros "Hfull". iDestruct 1 as (b') "(#Hb & Hl & 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]>σ)) {[l := (1%Qp, y)]}).
rewrite to_locking_heap_insert.
eapply singleton_local_update; first by eapply to_locking_heap_lookup_Some.
by apply exclusive_local_update. }
by iDestruct "Hauth" as "[$ $]".
iDestruct "Hfull" as "[$ Hpart]". iExists y. eauto with iFrame.
Qed.
Lemma locking_heap_unlock (l : loc) (v : val) (x : level) (q : frac) σ :
full_locking_heap σ - l (x,q) v
== full_locking_heap (<[l:=ULvl]>σ) l (ULvl,q) v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def.
iIntros "Hfull". 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:=ULvl]>σ)) {[l := (q, ULvl)]}).
rewrite to_locking_heap_insert.
eapply singleton_local_update; first by eapply to_locking_heap_lookup_Some.
apply prod_local_update_2.
apply local_update_unital_discrete.
intros h Hh. fold_leibniz. intros ->. split; eauto. }
iDestruct "Hfull" as "[$ Hpart]". eauto with iFrame.
Qed.
Lemma locking_heap_alloc σ l x v :
......@@ -222,10 +317,10 @@ Section properties.
rewrite /full_locking_heap mapsto_eq /mapsto_def Qp_mult_1_l.
iIntros (?) "$ Hauth".
iMod (own_update with "Hauth") as "Hauth".
{ eapply (auth_update_alloc _ (to_locking_heap (<[l:=x]> σ)) {[l := (1%Qp, to_agree x)]}).
{ eapply (auth_update_alloc _ (to_locking_heap (<[l:=x]> σ)) {[l := (1%Qp, x)]}).
rewrite to_locking_heap_insert.
apply alloc_singleton_local_update; last done.
by apply to_locking_heap_lookup_None. }
by iDestruct "Hauth" as "[$ $]".
iDestruct "Hauth" as "[$ Hpart]". eauto with iFrame.
Qed.
End properties.
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