Commit 2ad6aa98 authored by Dan Frumin's avatar Dan Frumin

More consistent names and a bit of cleanup

in locking_heap
parent aebd2dce
...@@ -191,7 +191,7 @@ Section proofs. ...@@ -191,7 +191,7 @@ Section proofs.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let. iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_let.
wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll). wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
iApply wp_fupd. wp_alloc l as "Hl". iApply wp_fupd. wp_alloc l as "Hl".
iMod (locking_heap_alloc with "Hσ Hl") as (?) "[Hσ Hl]"; first done. iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
iIntros "!> !>". rewrite cloc_to_val_eq. iIntros "!> !>". rewrite cloc_to_val_eq.
iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (MkCloc l 0))]. iSplitL "Hlocks Hσ"; [|by iApply ("HΦ" $! (MkCloc l 0))].
iExists X, _. iFrame. iExists X, _. iFrame.
...@@ -214,11 +214,11 @@ Section proofs. ...@@ -214,11 +214,11 @@ Section proofs.
iDestruct ("HΦ" with "H1 H2") as (cl w ->) "[Hl HΦ]". iDestruct ("HΦ" with "H1 H2") as (cl w ->) "[Hl HΦ]".
iApply awp_atomic_env. iApply awp_atomic_env.
iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR". iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR".
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hw1. iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1.
assert (cloc_to_val cl X) as HclX. assert (cloc_to_val cl X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. } { intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
rewrite cloc_to_val_eq in HclX. rewrite cloc_to_val_eq in HclX.
iMod (locking_heap_store with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]". iMod (full_locking_heap_store_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
wp_let. rewrite cloc_to_val_eq. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let. wp_let. rewrite cloc_to_val_eq. do 2 wp_proj; wp_let. do 2 wp_proj; wp_let. wp_proj; wp_let.
wp_apply (mset_add_spec with "[$]"); first done. wp_apply (mset_add_spec with "[$]"); first done.
iIntros "Hlocks /="; wp_seq. iIntros "Hlocks /="; wp_seq.
...@@ -244,11 +244,11 @@ Section proofs. ...@@ -244,11 +244,11 @@ Section proofs.
iIntros (v). iDestruct 1 as (cl q w ->) "[Hl HΦ]". awp_lam. iIntros (v). iDestruct 1 as (cl q w ->) "[Hl HΦ]". awp_lam.
iApply awp_atomic_env. iIntros (env) "Henv HR". iApply awp_atomic_env. iIntros (env) "Henv HR".
iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]". iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
iDestruct (locked_locs_unlocked with "Hl Hσ") as %Hv. iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv.
assert (cloc_to_val cl X) as HclX. assert (cloc_to_val cl X) as HclX.
{ intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. } { intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
rewrite cloc_to_val_eq in HclX. rewrite cloc_to_val_eq in HclX.
iMod (locking_heap_load with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]". iMod (full_locking_heap_load_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]".
wp_let. rewrite cloc_to_val_eq. wp_proj; wp_let. wp_proj; wp_let. wp_let. rewrite cloc_to_val_eq. wp_proj; wp_let. wp_proj; wp_let.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=". wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=".
rewrite bool_decide_false //. rewrite bool_decide_false //.
...@@ -296,8 +296,9 @@ Section proofs. ...@@ -296,8 +296,9 @@ Section proofs.
+ iExists , σ. by iFrame. + iExists , σ. by iFrame.
+ by iApply "HΦ". + by iApply "HΦ".
- iDestruct "Hus" as "[Hu Hus]". - iDestruct "Hus" as "[Hu Hus]".
iDestruct (full_locking_heap_present with "Hu Hσ") as %[z Hz]. iDestruct (full_locking_heap_locked_present with "Hu Hσ")
iMod (locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]". as %[z Hz].
iMod (full_locking_heap_unlock with "Hσ Hu") as "[Hσ Hu]".
iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks"). iApply ("IH" with "Hus [HΦ Hu] Hσ Hlocks").
iIntros "Hus". iApply "HΦ". by iFrame. iIntros "Hus". iApply "HΦ". by iFrame.
Qed. Qed.
......
...@@ -310,29 +310,27 @@ Section properties. ...@@ -310,29 +310,27 @@ Section properties.
move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''. move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''.
Qed. Qed.
Lemma locked_locs_unlocked σ cl v q : Lemma full_locking_heap_unlocked_value σ cl v q :
cl C{q} v - full_locking_heap σ - cl locked_locs σ. cl C{q} v - full_locking_heap σ - σ !! cl = Some (ULvl,v).
Proof. Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap. rewrite mapsto_eq /mapsto_def /full_locking_heap.
iDestruct 1 as (lv ?%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]". iDestruct 1 as ([] []%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
iDestruct (own_valid_2 with "Hfull Hl") iDestruct (own_valid_2 with "Hfull Hl")
as %[[lv' [?%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2. as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2; auto.
assert (lv' = ULvl) as -> by (by destruct lv', lv).
iPureIntro. rewrite /locked_locs.
apply not_elem_of_dom, map_filter_lookup_None.
right. intros [??]. by rewrite Hl=>[= <- <-].
Qed. Qed.
Lemma full_locking_heap_unlocked σ cl v q : Lemma full_locking_heap_unlocked σ cl v q :
cl C{q} v - full_locking_heap σ - σ !! cl = Some (ULvl,v). cl C{q} v - full_locking_heap σ - cl locked_locs σ.
Proof. Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap. iIntros "Hcl Hσ".
iDestruct 1 as ([] []%lvl_included) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]". iDestruct (full_locking_heap_unlocked_value with "Hcl Hσ") as %Hcl.
iDestruct (own_valid_2 with "Hfull Hl") iPureIntro.
as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2; auto. rewrite /locked_locs.
apply not_elem_of_dom, map_filter_lookup_None.
right. intros [??]. by rewrite Hcl=>[= <- <-].
Qed. Qed.
Lemma full_locking_heap_present σ cl v q : Lemma full_locking_heap_locked_present σ cl v q :
cl C[LLvl]{q} v - full_locking_heap σ - is_Some (σ !! cl). cl C[LLvl]{q} v - full_locking_heap σ - is_Some (σ !! cl).
Proof. Proof.
rewrite mapsto_eq /mapsto_def /full_locking_heap. rewrite mapsto_eq /mapsto_def /full_locking_heap.
...@@ -341,7 +339,7 @@ Section properties. ...@@ -341,7 +339,7 @@ Section properties.
as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2; eauto. as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2; eauto.
Qed. Qed.
Lemma locking_heap_load cl lv q v σ : Lemma full_locking_heap_load_upd cl lv q v σ :
full_locking_heap σ - cl C[lv]{q} v == ll vs, full_locking_heap σ - cl C[lv]{q} v == ll vs,
is_list ll vs vs !! (cloc_offset cl) = Some v is_list ll vs vs !! (cloc_offset cl) = Some v
(cloc_loc cl) SOMEV ll (cloc_loc cl) SOMEV ll
...@@ -361,7 +359,7 @@ Section properties. ...@@ -361,7 +359,7 @@ Section properties.
iExists lv'. auto. iExists lv'. auto.
Qed. Qed.
Lemma locking_heap_store cl lv v σ : Lemma full_locking_heap_store_upd cl lv v σ :
full_locking_heap σ - cl C[lv] v == ll vs, full_locking_heap σ - cl C[lv] v == ll vs,
is_list ll vs vs !! (cloc_offset cl) = Some v is_list ll vs vs !! (cloc_offset cl) = Some v
(cloc_loc cl) SOMEV ll (cloc_loc cl) SOMEV ll
...@@ -441,7 +439,7 @@ Section properties. ...@@ -441,7 +439,7 @@ Section properties.
rewrite locked_locs_alloc_unlocked // alloc_heap_None //; lia. rewrite locked_locs_alloc_unlocked // alloc_heap_None //; lia.
Qed. Qed.
Lemma locking_heap_alloc l ll vs σ : Lemma full_locking_heap_alloc_upd l ll vs σ :
is_list ll vs is_list ll vs
full_locking_heap σ - l SOMEV ll == full_locking_heap σ - l SOMEV ll ==
i, σ !! MkCloc l i = None i, σ !! MkCloc l i = None
...@@ -482,7 +480,7 @@ Section properties. ...@@ -482,7 +480,7 @@ Section properties.
rewrite mapsto_eq /mapsto_def. eauto. rewrite mapsto_eq /mapsto_def. eauto.
Qed. Qed.
Lemma locking_heap_unlock cl v lv q σ : Lemma full_locking_heap_unlock cl v lv q σ :
full_locking_heap σ - cl C[lv]{q} v == full_locking_heap σ - cl C[lv]{q} v ==
full_locking_heap (<[cl:=(ULvl,v)]>σ) cl C{q} v. full_locking_heap (<[cl:=(ULvl,v)]>σ) cl C{q} v.
Proof. Proof.
......
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