Commit 1cfdc584 authored by Dan Frumin's avatar Dan Frumin
Browse files

Store locations in the locking heap

- Get rid of fractions in `env_inv`.
- Separate the concerns
parent e109af04
......@@ -62,10 +62,9 @@ Section a_wp.
set_Forall (λ v, l : loc, v = #l l preσ) X.
Definition env_inv (env : val) : iProp Σ :=
( (X : gset val) (σ : gmap loc lvl),
( (X : gset val) (σ : gmap loc (lvl*val)),
is_mset env X
full_locking_heap σ
([ map] l _ σ, v', l {1/2} v')
correct_locks X (locked_locs σ))%I.
Definition awp (e : expr)
......@@ -256,7 +255,7 @@ Section a_wp_run.
iIntros ([ev <-]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "Henv". wp_let.
iMod (locking_heap_init ) as (?) "Hσ".
iMod locking_heap_init as (?) "Hσ".
pose (amg := AMonadG Σ _ _ _ _).
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
......
......@@ -92,24 +92,35 @@ Section proofs.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iApply wp_fupd.
wp_let. wp_alloc l as "Hl".
iAssert ⌜σ !! l = None%I with "[Hl Hls]" as %Hl.
{ remember (σ !! l) as σl. destruct σl; simplify_eq; eauto.
iAssert ⌜σ !! l = None%I with "[Hl Hσ]" as %Hl.
{ remember (σ !! l) as σl. destruct σl as [[? ?]|]; simplify_eq; eauto.
iDestruct "Hσ" as "[_ Hls]".
iExFalso. rewrite (big_sepM_lookup _ σ l _); last eauto.
iDestruct "Hls" as (v') "Hl'".
by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
iDestruct "Hl" as "[Hl Hl']".
iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
by iDestruct (mapsto_valid_2 l with "Hl Hls") as %[]. }
iMod (locking_heap_alloc σ l ULvl v with "Hl Hσ") as "[Hσ Hl']"; eauto.
iModIntro. iFrame "HR". iSplitR "H Hl'".
- iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
+ rewrite big_sepM_insert; eauto. iFrame. eauto.
+ iPureIntro. by rewrite locked_locs_alloc_unlocked.
- iExists X,(<[l:=(ULvl,v)]>σ). iFrame.
iPureIntro. by rewrite locked_locs_alloc_unlocked.
- iApply ("H" with "Hl'").
Qed.
(* DF TODO: move this somewhere else? *)
Lemma big_sepM_insert_overwrite `{Countable K, EqDecision K} {A : Type}
(Φ : K A iProp Σ) (m : gmap K A) i x x' :
m !! i = Some x
([ map] ky m, Φ k y)
Φ i x (Φ i x' - ([ map] ky <[i:=x']> m, Φ k y)).
Proof.
intros ?.
rewrite {1}big_sepM_delete //. iIntros "[$ ?]".
rewrite -insert_delete big_sepM_insert ?lookup_delete //.
eauto with iFrame.
Qed.
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ Ψ2 }} -
......@@ -127,7 +138,7 @@ Section proofs.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
assert (#l X).
......@@ -137,26 +148,30 @@ Section proofs.
wp_apply (mset_add_spec with "HX"); first done.
iIntros "HX". wp_seq.
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %?.
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hl") as "[Hσ Hl]".
do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as (b') "(Hb' & Hv & Hl)".
rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
rewrite Qp_mult_1_l.
iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
iCombine "Hv Hl'" as "Hv".
do 2 wp_proj.
iDestruct "Hσ" as "[Hσ Hls]".
rewrite {1}mapsto_eq /mapsto_def.
iDestruct "Hl" as (b' Hb%lvl_included) "Hl".
assert (b' = ULvl) as -> by (destruct b'; naive_solver).
rewrite (big_sepM_insert_overwrite _ _ l _ (ULvl, w2)) ?lookup_insert //.
iDestruct "Hls" as "[Hl' Hls] /=".
wp_store.
iDestruct "Hv" as "[Hv Hl']".
iSpecialize ("Hls" with "[Hl']"); eauto.
wp_proj. iFrame "HR". iSplitR "HΦ Hl Hv".
- iExists ({[#l]} X),(<[l:=LLvl]> σ). iFrame. iSplitL.
+ rewrite -big_sepM_insert_override; eauto.
iSpecialize ("Hls" with "Hl'").
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ apply (auth_update _ _ (to_locking_heap (<[l:=(ULvl,w2)]>σ)) {[l := (1%Qp, ULvl, agree.to_agree w2)]}).
rewrite !to_locking_heap_insert.
eapply (gmap.singleton_local_update (to_locking_heap σ)); first by apply to_locking_heap_lookup_Some.
by apply exclusive_local_update. }
iCombine "Hσ Hls" as "Hσ".
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ [Hl]") as "[Hσ Hl]".
{ rewrite mapsto_eq /mapsto_def. eauto. }
wp_proj. iFrame "HR". iSplitR "HΦ Hl".
- iExists ({[#l]} X),(<[l:=(LLvl,w2)]> σ). iFrame. iSplitL.
+ rewrite /full_locking_heap insert_insert //.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
- iApply "HΦ". iFrame. iExists b'; iSplit; eauto.
iPureIntro. apply lvl_included. destruct b'; eauto.
- iApply "HΦ". iFrame.
Qed.
Lemma a_load_spec_exists_frac R Φ e :
......@@ -172,7 +187,7 @@ Section proofs.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hl.
assert (#l X).
......@@ -183,13 +198,17 @@ Section proofs.
wp_apply (mset_member_spec with "HX").
iIntros "Henv /=". case_decide; first by exfalso. simpl.
wp_op. iSplit; eauto. iNext. wp_seq.
iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hσl.
rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as (b') "(% & Hv & Hl)".
wp_load.
iCombine "Hv Hl" as "Hv". iFrame "HR".
iSplitR "HΦ Hv".
iDestruct "Hl" as (b' Hb%lvl_included) "Hl".
assert (b' = ULvl) as -> by (destruct b'; naive_solver).
iDestruct "Hσ" as "[Hσ Hls]".
rewrite (big_sepM_lookup_acc _ _ l) //. iDestruct "Hls" as "[Hl' Hls] /=".
wp_load. iSpecialize ("Hls" with "Hl'").
iFrame "HR".
iSplitR "HΦ Hl".
- iExists X,σ. by iFrame.
- iApply "HΦ". iExists b'. iSplit; eauto.
- iApply "HΦ". eauto.
Qed.
Lemma a_load_spec R Φ q e :
......@@ -241,7 +260,7 @@ Section proofs.
iIntros (env) "Henv HR".
iApply wp_fupd.
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Henv" as (X σ) "(HX & Hσ & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
wp_let. iApply (mset_clear_spec with "HX").
iNext. iIntros "HX".
......@@ -255,9 +274,8 @@ Section proofs.
- iDestruct "Hus" as "[Hu Hus]".
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").
iApply ("IH" with "Hus [HΦ Hu] Hσ HR HX").
{ iIntros "Hus". iApply "HΦ". by iFrame. }
{ rewrite -big_sepM_insert_override; eauto. }
Qed.
Lemma a_sequence_spec R Φ (f e : expr) :
......@@ -316,7 +334,7 @@ Section proofs.
Qed.
Lemma a_while_spec' R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
awp c R (λ v, (v = #true
awp c R (λ v, (v = #true
awp b R (λ _, U (awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ)))
(v = #false awp (a_seq #()) R Φ)) -
awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
......
......@@ -59,7 +59,7 @@ Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin.
(* Auth (Loc -> (Q * Level)) *)
Definition locking_heapUR : ucmraT :=
gmapUR loc (prodR fracR lvlUR).
gmapUR loc (prodR (prodR fracR lvlUR) (agreeR valC)).
(** The CMRA we need. *)
Class locking_heapG (Σ : gFunctors) := LHeapG {
......@@ -79,25 +79,26 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Definition to_locking_heap (σ : gmap loc lvl) : locking_heapUR :=
fmap (λ x, (1%Qp, x)) σ.
Definition to_locking_heap (σ : gmap loc (lvl*val)) : locking_heapUR :=
fmap (λ '(b,v), (1%Qp, b, to_agree v)) σ.
Definition is_lock_lvl (a : loc * lvl) : bool :=
match a.2 with
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) : 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) :=
own (@lheap_name _ hG) ( (to_locking_heap σ)).
Definition full_locking_heap (σ : gmap loc (lvl*val)) :=
(own (@lheap_name _ hG) ( (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' l {q*(1/2)} v
own (@lheap_name _ hG) ( {[ l := (q, b') ]}))%I.
( b' : lvl, b b'
own (@lheap_name _ hG) ( {[ l := (q, b', to_agree v) ]}))%I.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
......@@ -114,20 +115,21 @@ Notation "l ↦C{ q } v" := (l ↦C[ULvl]{q} v)%I
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) : to_locking_heap σ.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
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 locking_heap_init `{locking_heapPreG Σ} σ :
(|==> _ : locking_heapG Σ, full_locking_heap σ)%I.
Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
(|==> _ : locking_heapG Σ, full_locking_heap )%I.
Proof.
iMod (own_alloc ( to_locking_heap σ)) as (γ) "Hh".
iMod (own_alloc ( to_locking_heap )) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_locking_heap_valid. }
iModIntro. by iExists (LHeapG Σ _ γ).
iModIntro. iExists (LHeapG Σ _ γ).
rewrite /full_locking_heap big_sepM_empty //. by iFrame.
Qed.
Section properties.
Context `{hG : locking_heapG Σ, !heapG Σ}.
Implicit Type σ : gmap loc lvl.
Implicit Type σ : gmap loc (lvl*val).
Implicit Type x y : lvl.
Implicit Type l : loc.
......@@ -137,16 +139,14 @@ Section properties.
Global Instance mapsto_fractional l x v : Fractional (λ q, l C[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.
- iDestruct 1 as (b') "(#Hb & [$ $] & Ho)".
- iDestruct 1 as (b') "(#Hb & Ho)".
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)".
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.
......@@ -159,7 +159,7 @@ Section properties.
Lemma mapsto_downgrade' x y l q v : x y l C[y]{q} v - l C[x]{q} v.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (b' ?) "[$ Ho]".
iDestruct 1 as (b' ?) "Ho".
iExists b'. iSplit; eauto.
iPureIntro. transitivity y; done.
Qed.
......@@ -170,19 +170,22 @@ Section properties.
Lemma mapsto_value_agree x x' l q q' v v' : l C[x]{q} v - l C[x']{q'} v' - v = v'.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (b1 ?) "[Hl1 Ho1]".
iDestruct 1 as (b2 ?) "[Hl2 Ho2]".
iDestruct (mapsto_agree with "Hl1 Hl2") as %->. done.
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'].
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.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (b1 Hb1) "[Hl1 Ho1]".
iDestruct 1 as (b2 Hb2) "[Hl2 Ho2]".
iDestruct 1 as (b1 Hb1) "Ho1".
iDestruct 1 as (b2 Hb2) "Ho2".
iExists (b1 b2). iSplitR.
{ iPureIntro. destruct x,x',b1,b2; eauto. }
iCombine "Hl1 Hl2" as "Hl". rewrite Qp_mult_plus_distr_l.
iCombine "Ho1 Ho2" as "Ho". rewrite frac_op'. iFrame.
Qed.
......@@ -193,70 +196,71 @@ Section properties.
iApply (mapsto_combine with "Hl1 Hl2").
Qed.
Lemma to_locking_heap_insert σ l x :
to_locking_heap (<[l := x]> σ) = <[l := (1%Qp, x)]>(to_locking_heap σ).
Lemma to_locking_heap_insert σ l x v :
to_locking_heap (<[l := (x,v)]> σ) = <[l := (1%Qp, x, to_agree v)]>(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, x).
Lemma to_locking_heap_lookup_Some σ l x v :
σ !! l = Some (x,v) to_locking_heap σ !! l = Some (1%Qp, x, 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.
Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
Lemma locked_locs_lock σ l :
locked_locs (<[l:=LLvl]>σ) = {[l]} locked_locs σ.
Lemma locked_locs_lock σ l v :
locked_locs (<[l:=(LLvl,v)]>σ) = {[l]} locked_locs σ.
Proof.
rewrite /locked_locs -map_filter_lookup_insert; last done.
apply dom_insert_L.
Qed.
Lemma locked_locs_unlock σ l :
σ !! l = Some LLvl
locked_locs (<[l := ULvl]>σ) = locked_locs σ {[l]}.
Lemma locked_locs_unlock σ l v :
σ !! l = Some (LLvl,v)
locked_locs (<[l := (ULvl,v)]>σ) = locked_locs σ {[l]}.
Proof.
intros Hl. rewrite /locked_locs -dom_delete_L. f_equal.
apply map_eq=> j. apply option_eq=> x.
rewrite lookup_delete_Some !map_filter_lookup_Some lookup_insert_Some. naive_solver.
Qed.
Lemma locked_locs_alloc_unlocked σ l :
Lemma locked_locs_alloc_unlocked σ l v :
σ !! l = None
locked_locs (<[l := ULvl]>σ) = locked_locs σ.
locked_locs (<[l := (ULvl,v)]>σ) = locked_locs σ.
Proof.
intros Hl. rewrite /locked_locs. f_equal.
apply map_eq => j. apply option_eq=> x.
rewrite !map_filter_lookup_Some lookup_insert_Some. naive_solver.
Qed.
Lemma heap_singleton_included (σ : gmap loc lvl) l x q :
{[l := (q, x)]} (to_locking_heap σ) y, x y σ !! l = Some y.
Lemma heap_singleton_included σ l x q v :
{[l := (q, x, to_agree v)]} (to_locking_heap σ) y, x y σ !! l = Some (y, v).
Proof.
rewrite singleton_included=> -[[q' av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[y [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] Hxy.
exists y; done.
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'.
Qed.
Lemma locked_locs_unlocked σ l v q :
l C{q} v - full_locking_heap σ - l locked_locs σ⌝.
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iDestruct 1 as (b') "(Hb' & Hl & Hpart)". iIntros "Hfull".
iDestruct 1 as (b') "(Hb' & Hpart)". iIntros "[Hfull Hmap]".
iDestruct "Hb'" as %Hb'%lvl_included.
iDestruct (own_valid_2 with "Hfull Hpart")
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 not_elem_of_dom. apply map_filter_lookup_None.
right. intros. simplify_eq/=. eauto.
right. intros [? ?]. rewrite Hl. intros. simplify_eq/=. eauto.
Qed.
Lemma full_locking_heap_unlocked σ l v q :
l C{q} v - full_locking_heap σ - ⌜σ !! l = Some ULvl.
l C{q} v - full_locking_heap σ - ⌜σ !! l = Some (ULvl,v).
Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iDestruct 1 as (b') "(Hb' & Hl & Hpart)". iIntros "Hfull".
iDestruct 1 as (b') "(Hb' & Hpart)". iIntros "[Hfull Hmap]".
iDestruct "Hb'" as %Hb'%lvl_included.
iDestruct (own_valid_2 with "Hfull Hpart")
as %[[y [Hy%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2.
......@@ -267,7 +271,7 @@ Section properties.
l C[LLvl]{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 1 as (b') "(#Hb & Hpart)". iIntros "[Hfull Hmap]".
iDestruct (own_valid_2 with "Hfull Hpart")
as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2.
eauto.
......@@ -275,49 +279,59 @@ Section properties.
Lemma locking_heap_change_lock (l : loc) (v : val) (x y : lvl) σ :
full_locking_heap σ - l C[x] v
== full_locking_heap (<[l:=y]>σ) l C[y] v.
== full_locking_heap (<[l:=(y,v)]>σ) l C[y] v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def.
iIntros "Hfull". iDestruct 1 as (b') "(#Hb & Hl & Hpart)".
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]>σ)) {[l := (1%Qp, y)]}).
{ apply (auth_update _ _ (to_locking_heap (<[l:=(y,v)]>σ)) {[l := (1%Qp, y, 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. }
iDestruct "Hfull" as "[$ Hpart]". iExists y. eauto with iFrame.
iDestruct "Hfull" as "[$ Hpart]". iModIntro.
iSplitL "Hmap"; last eauto with iFrame.
rewrite -!(big_sepM_fmap (λ bv, bv.2) (λ l v, l v)%I).
rewrite fmap_insert /= insert_id //.
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]>σ) l C{q} v.
== full_locking_heap (<[l:=(ULvl,v)]>σ) l C{q} v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def.
iIntros "Hfull". iDestruct 1 as (b') "(#Hb' & $ & Hpart)".
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:=ULvl]>σ)) {[l := (q, ULvl)]}).
{ apply (auth_update _ _ (to_locking_heap (<[l:=(ULvl,v)]>σ)) {[l := (q, ULvl, to_agree v)]}).
rewrite to_locking_heap_insert.
eapply singleton_local_update; first by eapply to_locking_heap_lookup_Some.
apply prod_local_update_2.
apply prod_local_update_1, prod_local_update_2.
apply local_update_unital_discrete.
intros h Hh. fold_leibniz. intros ->. split; eauto. }
iDestruct "Hfull" as "[$ Hpart]". eauto with iFrame.
iDestruct "Hfull" as "[$ Hpart]". iModIntro.
iSplitL "Hmap"; last eauto with iFrame.
rewrite -!(big_sepM_fmap (λ bv, bv.2) (λ l v, l v)%I).
rewrite fmap_insert /= insert_id //.
rewrite lookup_fmap Hl //.
Qed.
Lemma locking_heap_alloc σ l x v :
σ !! l = None
l {1/2} v - full_locking_heap σ == full_locking_heap (<[l:=x]>σ) l C[ x ] v.
l v - full_locking_heap σ == full_locking_heap (<[l:=(x,v)]>σ) l C[ x ] v.
Proof.
rewrite /full_locking_heap mapsto_eq /mapsto_def Qp_mult_1_l.
iIntros (?) "$ Hauth".
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]> σ)) {[l := (1%Qp, x)]}).
{ eapply (auth_update_alloc _ (to_locking_heap (<[l:=(x,v)]> σ)) {[l := (1%Qp, x, to_agree v)]}).
rewrite to_locking_heap_insert.
apply alloc_singleton_local_update; last done.
by apply to_locking_heap_lookup_None. }
iDestruct "Hauth" as "[$ Hpart]". eauto with iFrame.
iDestruct "Hauth" as "[$ Hpart]". iModIntro.
iSplitR "Hpart"; last eauto with iFrame.
rewrite big_sepM_insert //. 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