Commit 9ca012d6 authored by Ralf Jung's avatar Ralf Jung

strengthen lifetime logic: make lft_userN disjoint from lftN so it remains...

strengthen lifetime logic: make lft_userN disjoint from lftN so it remains available during atomic accessors
parent 5d384541
Pipeline #31438 passed with stage
in 33 minutes and 25 seconds
......@@ -6,9 +6,9 @@ From iris.bi Require Import fractional.
Set Default Proof Using "Type".
Definition lftN : namespace := nroot .@ "lft".
(** A mask inside the lifetime logic namespace that users may use.
This is still available in the "consequence" view shift of borrow accessors. *)
Definition lft_userN : namespace := nroot .@ "lft" .@ "usr".
(** A (disjoint) mask that is available in the "consequence" view shift of
borrow accessors. *)
Definition lft_userN : namespace := nroot .@ "lft_usr".
Module Type lifetime_sig.
(** CMRAs needed by the lifetime logic *)
......@@ -96,7 +96,7 @@ Module Type lifetime_sig.
Parameter lft_dead_static : [ static] - False.
Parameter lft_create : E, lftN E
lft_ctx ={E}= κ, 1.[κ] (1.[κ] ={lftN}[lft_userN]= [†κ]).
lft_ctx ={E}= κ, 1.[κ] (1.[κ] ={lftN lft_userN}[lft_userN]= [†κ]).
Parameter bor_create : E κ P,
lftN E lft_ctx - P ={E}= &{κ} P ([†κ] ={E}= P).
Parameter bor_fake : E κ P,
......
......@@ -80,7 +80,7 @@ Proof.
iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
- iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hf & HP')".
solve_ndisj.
{ solve_ndisj. }
iDestruct ("HPP'" with "HP'") as "$".
iMod ("Hclose'" with "[-Hf Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
......
......@@ -16,7 +16,7 @@ Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
([ set] κ' K', lft_inv_alive κ'))%I in
( κ', is_Some (I !! κ') κ κ' κ' K)
( κ', is_Some (I !! κ') κ' κ κ' K')
Iinv - lft_inv_alive κ - [†κ] ={lft_userN inhN}= Iinv lft_inv_dead κ.
Iinv - lft_inv_alive κ - [†κ] ={lft_userN borN inhN}= Iinv lft_inv_dead κ.
Proof.
iIntros (Iinv HK HK') "(HI & Hdead & Halive) Hlalive Hκ".
rewrite lft_inv_alive_unfold;
......@@ -34,15 +34,15 @@ Proof.
iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
as %[?%nat_included _]%auth_both_valid; lia. }
iMod (box_empty with "Hbox") as "[HP Hbox]"=>//.
{ (* FIXME [solve_ndisj] fails *)
etrans; last exact: union_subseteq_l. solve_ndisj. }
{ (* FIXME [solve_ndisj] fails *) set_solver-. }
{ intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
iDestruct (big_sepS_filter_acc (. κ) _ _ (dom _ I) with "Halive")
as "[Halive Halive']".
{ intros κ'. rewrite elem_of_dom. eauto. }
iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
iApply fupd_trans. iApply fupd_mask_mono; last
iMod ("Hvs" $! I with "[HI Halive] HP Hκ") as "(Hinv & HQ & Hcnt')".
{ set_solver-. }
{ rewrite lft_vs_inv_unfold. iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(HI&Halive)".
iSpecialize ("Halive'" with "Halive").
......@@ -63,7 +63,7 @@ Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lf
( κ κ', κ K is_Some (I !! κ') κ κ' κ' K)
( κ, lft_alive_in A κ is_Some (I !! κ) κ K κ K')
Iinv K' - ([ set] κ K, lft_inv A κ [†κ])
={lft_userN inhN}= Iinv K' [ set] κ K, lft_inv_dead κ.
={lft_userN borN inhN}= Iinv K' [ set] κ K, lft_inv_dead κ.
Proof.
intros Iinv. revert K'.
induction (set_wf K) as [K _ IH]=> K' HKK' HK HK'.
......@@ -110,7 +110,7 @@ Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
Lemma lft_create E :
lftN E
lft_ctx ={E}= κ, 1.[κ] (1.[κ] ={lftN}[lft_userN]= [†κ]).
lft_ctx ={E}= κ, 1.[κ] (1.[κ] ={lftN lft_userN}[lft_userN]= [†κ]).
Proof.
iIntros (?) "#LFT".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
......@@ -128,8 +128,14 @@ Proof.
iModIntro; iExists {[ Λ ]}.
rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
clear I A HΛ. iIntros "!# HΛ".
iApply (step_fupd_mask_mono (lftN) _ (lftN∖↑mgmtN)); [solve_ndisj..|].
iApply (step_fupd_mask_mono (lftN lft_userN) _ ((lftN lft_userN)∖↑mgmtN)).
{ (* FIXME solve_ndisj should really handle this... *)
assert (lft_userN ## mgmtN) by solve_ndisj.
set_solver. }
{ done. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
{ (* FIXME solve_ndisj should really handle this... *)
assert (mgmtN lftN) by solve_ndisj. set_solver. }
rewrite /lft_tok big_sepMS_singleton.
iDestruct (own_valid_2 with "HA HΛ")
as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid.
......@@ -150,8 +156,16 @@ Proof.
iAssert ([ set] κ K, lft_inv A κ [ κ])%I with "[HinvK]" as "HinvK".
{ iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
iApply fupd_trans. iApply (fupd_mask_mono (lft_userN inhN));
first by apply union_least; solve_ndisj.
iApply fupd_trans.
iApply (fupd_mask_mono (lft_userN borN inhN)).
{ (* FIXME can we make solve_ndisj handle this? *)
clear. rewrite -assoc. apply union_least.
- assert (lft_userN ##@{coPset} mgmtN) by solve_ndisj. set_solver.
- assert (inhN ##@{coPset} mgmtN) by solve_ndisj.
assert (inhN @{coPset} lftN) by solve_ndisj.
assert (borN ##@{coPset} mgmtN) by solve_ndisj.
assert (borN @{coPset} lftN) by solve_ndisj.
set_solver. }
iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
{ done. }
{ intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
......
......@@ -6,9 +6,7 @@ Import uPred.
Definition inhN : namespace := lftN .@ "inh".
Definition mgmtN : namespace := lftN .@ "mgmt".
(** We put borrows into the "user" namespace, so that they are available
in [lft_vs]. *)
Definition borN : namespace := lft_userN .@ "bor".
Definition borN : namespace := lftN .@ "bor".
Definition atomic_lft := positive.
(* HACK : We need to make sure this is not in the top-level context,
......@@ -142,7 +140,7 @@ Section defs.
own_cnt κ ( n)
I : gmap lft lft_names,
lft_vs_inv_go κ lft_inv_alive I - Pb - lft_dead κ
={lft_userN}=
={lft_userN borN}=
lft_vs_inv_go κ lft_inv_alive I Pi own_cnt κ ( n))%I.
Definition lft_inv_alive_go (κ : lft)
......@@ -270,7 +268,7 @@ Lemma lft_vs_unfold κ Pb Pi :
lft_vs κ Pb Pi n : nat,
own_cnt κ ( n)
I : gmap lft lft_names,
lft_vs_inv κ I - Pb - lft_dead κ ={lft_userN}=
lft_vs_inv κ I - Pb - lft_dead κ ={lft_userN borN}=
lft_vs_inv κ I Pi own_cnt κ ( n).
Proof. done. Qed.
......
......@@ -490,7 +490,7 @@ Proof.
Qed.
Lemma lft_vs_cons κ Pb Pb' Pi :
( Pb'- [†κ] ={lft_userN}= Pb) -
( Pb'- [†κ] ={lft_userN borN}= Pb) -
lft_vs κ Pb Pi - lft_vs κ Pb' Pi.
Proof.
iIntros "Hcons Hvs". rewrite !lft_vs_unfold.
......
......@@ -81,7 +81,8 @@ Proof.
(exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iMod (slice_fill _ _ false with "Hislice HP Hbox")
as "Hbox"; first by solve_ndisj.
as "Hbox".
{ set_solver-. }
{ by rewrite lookup_fmap HB. }
iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
rewrite /=. iDestruct "Hcnt" as "[% H1◯]".
......
......@@ -285,8 +285,8 @@ Section typing.
iDestruct "Hϝ" as (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
iSpecialize ("Hinh" with "Htk"). iClear "Hκs".
iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "Hinh"); [solve_ndisj..|]. wp_seq.
iApply (wp_mask_mono _ (lftN lft_userN)); first done.
iApply (wp_step_fupd with "Hinh"); [set_solver-..|]. wp_seq.
iIntros "#Htok !>". wp_seq. iMod ("HκsI" with "Htok") as ">Hκs".
iApply ("Hk" with "Htl HL Hκs"). rewrite tctx_hasty_val. done.
+ rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
......
......@@ -41,7 +41,7 @@ Section lft_contexts.
(* Local lifetime contexts. *)
Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
let κ' := lft_intersect_list (x.2) in
( κ0, x.1 = κ' κ0 q.[κ0] (1.[κ0] ={lftN}[lft_userN]= [†κ0]))%I.
( κ0, x.1 = κ' κ0 q.[κ0] (1.[κ0] ={lftN lft_userN}[lft_userN]= [†κ0]))%I.
Global Instance llctx_elt_interp_fractional x :
Fractional (llctx_elt_interp x).
Proof.
......
......@@ -27,7 +27,7 @@ Section arc.
(* because [weak_new] cannot prove ty_shr, even for a dead *)
(* lifetime. *)
(ty.(ty_shr) ν tid (l + 2) [†ν])
(1.[ν] ={lftN arc_endN}[lft_userN]=
(1.[ν] ={lftN lft_userN arc_endN}[lft_userN]=
[†ν] (l + 2) ↦∗: ty.(ty_own) tid l(2 + ty.(ty_size))))%I.
Global Instance arc_persist_ne tid ν γ l n :
......@@ -88,10 +88,14 @@ Section arc.
iMod (inv_acc with "INV") as "[[H†|[$ Hvs]] Hclose]";
[set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|].
rewrite difference_union_distr_l_L difference_diag_L right_id_L
difference_disjoint_L; last solve_ndisj.
difference_disjoint_L; last first.
{ apply disjoint_union_l. split; solve_ndisj. }
iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
iMod "H" as "#Hν". iMod ("Hvs" with "Hν") as "$". iIntros "{$Hν} !>".
iApply "Hclose". auto.
iMod "H" as "#Hν".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
{ set_solver-. }
iIntros "{$Hν} !>".
iMod "Hclose2" as "_". iApply "Hclose". auto.
Qed.
Program Definition arc (ty : type) :=
......@@ -394,7 +398,7 @@ Section arc.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lft_create with "LFT") as (ν) "[Hν Hν†]"; first done.
wp_bind (_ + _)%E. iSpecialize ("Hν†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hν†"); [solve_ndisj..|].
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hν†"); [set_solver-..|].
wp_op. iIntros "#H† !>". rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_write.
iApply (type_type _ _ _ [ #lrc box (weak ty)]
with "[] LFT HE Hna HL Hk [>-]"); last first.
......@@ -768,8 +772,7 @@ Section arc.
iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
{ (* FIXME [solve_ndisj] fails *)
etrans; last exact: union_subseteq_l. solve_ndisj. }
{ set_solver-. (* FIXME [solve_ndisj] fails *) }
iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
......@@ -873,8 +876,7 @@ Section arc.
iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
{ (* FIXME [solve_ndisj] fails *)
etrans; last exact: union_subseteq_l. solve_ndisj. }
{ (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
......@@ -949,8 +951,7 @@ Section arc.
wp_apply (is_unique_spec with "Hi Htoks"). iIntros ([]) "H"; wp_if.
- iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
{ (* FIXME [solve_ndisj] fails *)
etrans; last exact: union_subseteq_l. solve_ndisj. }
{ (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_seq. iIntros "(#Hν & Hown & H†) !>". wp_seq.
iMod ("Hclose2" with "[Hrc Hrc1 H†] Hown") as "[Hb Hα]".
{ iIntros "!> Hown !>". iLeft. iFrame. }
......@@ -1036,8 +1037,7 @@ Section arc.
- iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ + _)%E.
iSpecialize ("Hc" with "HP1").
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
{ (* FIXME [solve_ndisj] fails *)
etrans; last exact: union_subseteq_l. solve_ndisj. }
{ (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
{ iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
......@@ -1053,8 +1053,7 @@ Section arc.
iApply type_jump; solve_typing.
- iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
{ (* FIXME [solve_ndisj] fails *)
etrans; last exact: union_subseteq_l. solve_ndisj. }
{ (* FIXME [solve_ndisj] fails *) set_solver-. }
wp_apply wp_new=>//. lia. iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>".
rewrite -!lock Nat2Z.id.
wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
......
......@@ -85,7 +85,7 @@ Section rc.
because [weak_new] cannot prove ty_shr, even for a dead
lifetime. *)
(ty.(ty_shr) ν tid (l + 2) [†ν])
(1.[ν] ={lftN}[lft_userN]= [†ν]))%I.
(1.[ν] ={lftN lft_userN}[lft_userN]= [†ν]))%I.
Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
Proof. unfold rc_persist, tc_opaque. apply _. Qed.
......@@ -298,7 +298,10 @@ Section code.
rewrite -[in (1).[ν]%I]Hqq' -[(|={lft_userN,}=>_)%I]fupd_trans.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
iModIntro. iNext. iMod "H†".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
{ set_solver-. }
iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
iModIntro. iNext. iDestruct "Hty" as (vl) "[??]". iExists _. iFrame.
by iApply "Hinclo".
......@@ -310,7 +313,10 @@ Section code.
rewrite -[in (1).[ν]%I]Hqq' -[(|={lft_userN,}=>_)%I]fupd_trans.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
iModIntro. iNext. iMod "H†".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
{ set_solver-. }
iMod "Hclose2" as "_". iModIntro.
iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc, prod_local_update_1,
(cancel_local_update_unit (Some _) None). }
......@@ -328,7 +334,10 @@ Section code.
rewrite -[(|={lft_userN,}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
iModIntro. iNext. iMod "H†".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
{ set_solver-. }
iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
first by iExists _; iFrame; iFrame.
rewrite Hincls. iFrame. iSplitL "Hty".
......
......@@ -466,7 +466,7 @@ Section code.
wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
iPoseProof ("Hν†" with "Hν") as "H†". wp_bind (_ <- _)%E.
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [solve_ndisj..|].
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [set_solver-..|].
wp_write. iIntros "#Hν !>". wp_seq.
iApply (type_type _ _ _ [ #lw box (weak ty)]
with "[] LFT HE Hna HL Hk [> -]"); last first.
......
......@@ -15,7 +15,7 @@ Section ref_functions.
own γ ( reading_stR q ν) -
(q' : Qp) n, l #(Zpos n) (q q')%Qc
own γ ( (refcell_st_to_R $ Some (ν, false, q', n)) reading_stR q ν)
((1).[ν] ={lftN}[lft_userN]= &{α}((l + 1) ↦∗: ty_own ty tid))
((1).[ν] ={lftN lft_userN}[lft_userN]= &{α}((l + 1) ↦∗: ty_own ty tid))
( q'', (q' + q'' = 1)%Qp q''.[ν])
ty.(ty_shr) (α ν) tid (l + 1).
Proof.
......@@ -162,7 +162,7 @@ Section ref_functions.
as (q' n) "(H↦lrc & >% & H●◯ & H† & Hq' & Hshr)".
iDestruct "Hq'" as (q'') ">[% Hν']".
wp_read. wp_let. wp_op. wp_write.
iAssert (|={lftN}[lft_userN]=> refcell_inv tid lrc γ β ty')%I
iAssert (|={lftN lft_userN}[lft_userN]=> refcell_inv tid lrc γ β ty')%I
with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
{ iDestruct (own_valid with "H●◯") as
%[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
......@@ -180,10 +180,10 @@ Section ref_functions.
{ apply auth_update_dealloc.
rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
apply (cancel_local_update_unit (reading_stR q ν)), _. }
iApply step_fupd_intro; first solve_ndisj. iExists (q+q'')%Qp. iFrame.
iApply step_fupd_intro; first set_solver-. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
wp_bind Endlft. iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "INV"); [solve_ndisj..|]. wp_seq.
wp_bind Endlft. iApply (wp_mask_mono _ (lftN lft_userN)); first done.
iApply (wp_step_fupd with "INV"); [set_solver-..|]. wp_seq.
iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ #lx box (uninit 2)] with "[] LFT HE Hna HL Hk");
......
......@@ -49,7 +49,7 @@ Section refcell_inv.
(* Not borrowed. *)
&{α}((l + 1) ↦∗: ty.(ty_own) tid)
| Some (ν, rw, q, _) =>
(1.[ν] ={lftN}[lft_userN]= &{α}((l + 1) ↦∗: ty.(ty_own) tid))
(1.[ν] ={lftN lft_userN}[lft_userN]= &{α}((l + 1) ↦∗: ty.(ty_own) tid))
( q', (q + q')%Qp = 1%Qp q'.[ν])
if rw then (* Mutably borrowed. *) True
else (* Immutably borrowed. *) ty.(ty_shr) (α ν) tid (l + 1)
......@@ -151,11 +151,11 @@ Section refcell.
iExists γ, _. iFrame "Hst Hn Hshr".
iSplitR "Htok2"; last by iExists _; iFrame; rewrite Qp_div_2.
iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
iApply fupd_mask_mono; last iApply "Hh". done. rewrite -lft_dead_or. auto.
iApply fupd_mask_mono; last iApply "Hh". set_solver-. rewrite -lft_dead_or. auto.
- iMod (own_alloc ( (refcell_st_to_R $ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
{ rewrite -step_fupd_intro. auto. solve_ndisj. }
{ rewrite -step_fupd_intro. auto. set_solver-. }
iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
iApply lft_tok_static.
Qed.
......
......@@ -204,7 +204,11 @@ Section refcell_functions.
iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame "∗#".
iSplitR "Htok2".
+ iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto.
iNext. iMod "Hν".
iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
{ set_solver-. }
* rewrite -lft_dead_or. auto.
* done.
+ iExists _. iFrame. by rewrite Qp_div_2. }
iMod ("Hclose''" with "[$INV] Hna") as "[Hβtok1 Hna]".
iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
......@@ -281,7 +285,10 @@ Section refcell_functions.
iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh Htok1] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iNext. iSplitL "Hbh".
- iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
iApply "Hbh". rewrite -lft_dead_or. auto.
iMod fupd_intro_mask' as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
{ set_solver-. }
* rewrite -lft_dead_or. auto.
* done.
- iSplitL; [|done]. iExists _. iFrame. by rewrite Qp_div_2. }
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
......
......@@ -127,7 +127,7 @@ Section refmut_functions.
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_read. wp_let. wp_op. wp_write.
iAssert (|={lftN}[lft_userN]=> refcell_inv tid lrc γ β ty')%I
iAssert (|={lftN lft_userN}[lft_userN]=> refcell_inv tid lrc γ β ty')%I
with "[H↦lrc H● H◯ Hν INV]" as "INV".
{ iDestruct (own_valid_2 with "H● H◯") as
%[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
......@@ -139,7 +139,8 @@ Section refmut_functions.
iMod (own_update_2 with "H● H◯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
apply cancel_local_update_unit, _. }
iDestruct "INV" as "(H† & Hq & _)". iApply "H†".
iDestruct "INV" as "(H† & Hq & _)".
iApply "H†".
iDestruct "Hq" as (q) "(<- & ?)". iFrame.
- simpl in *. setoid_subst. iExists (Some (_, _, _, _)).
iMod (own_update_2 with "H● H◯") as "$".
......@@ -148,11 +149,11 @@ Section refmut_functions.
iDestruct "INV" as "(H† & Hq & _)".
rewrite /= (_:Z.neg (1%positive n') + 1 = Z.neg n');
last (rewrite pos_op_plus; lia). iFrame.
iApply step_fupd_intro; [solve_ndisj|]. iSplitL; [|done].
iApply step_fupd_intro; [set_solver-|]. iSplitL; [|done].
iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
rewrite assoc (comm _ q'' q) //. }
wp_bind Endlft. iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "INV"); [solve_ndisj|]. wp_seq. iIntros "{Hb} Hb !>".
wp_bind Endlft. iApply (wp_mask_mono _ (lftN lft_userN)); first done.
iApply (wp_step_fupd with "INV"); [set_solver-|]. wp_seq. iIntros "{Hb} Hb !>".
iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
iApply (type_type _ _ _ [ #lx box (uninit 2)]
......
......@@ -39,7 +39,7 @@ Section rwlock_inv.
| Some (Cinr (agν, q, n)) =>
(* Locked for read. *)
(ν : lft) q', agν to_agree ν
(1.[ν] ={lftN}[lft_userN]= [†ν])
(1.[ν] ={lftN lft_userN}[lft_userN]= [†ν])
([†ν] ={lftN}= &{α}((l + 1) ↦∗: ty.(ty_own) tid))
ty.(ty_shr) (α ν) tid (l + 1)
(q + q')%Qp = 1%Qp q'.[ν]
......
......@@ -183,7 +183,7 @@ Section rwlock_functions.
iAssert ( qν ν, (qβ / 2).[β] (qν).[ν]
ty_shr ty (β ν) tid (lx + 1)
own γ ( reading_st qν ν) rwlock_inv tid lx γ β ty
((1).[ν] ={lftN}[lft_userN]= [†ν]))%I
((1).[ν] ={lftN lft_userN}[lft_userN]= [†ν]))%I
with "[> Hlx Hownst Hst Hβtok2]"
as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
{ destruct st' as [[|[[agν q] n]|]|]; try done.
......
......@@ -23,7 +23,7 @@ Section rwlockreadguard.
ν q γ β, ty.(ty_shr) (α ν) tid (l + 1)
α β &at{β,rwlockN}(rwlock_inv tid l γ β ty)
q.[ν] own γ ( reading_st q ν)
(1.[ν] ={lftN}[lft_userN]= [†ν])
(1.[ν] ={lftN lft_userN}[lft_userN]= [†ν])
| _ => False
end;
ty_shr κ tid l :=
......
......@@ -83,7 +83,7 @@ Section rwlockreadguard_functions.
iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
iDestruct "INV" as (st') "(Hlx & >H● & Hst)".
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
+ iAssert (|={ rwlockN}[ rwlockN lftN]=>
+ iAssert (|={ rwlockN}[ rwlockN lftN lft_userN]=>
(lx' #(Z_of_rwlock_st st'-1) == rwlock_inv tid lx' γ β ty))%I
with "[H● H◯ Hx' Hν Hst H†]" as "INV".
{ iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
......@@ -94,12 +94,17 @@ Section rwlockreadguard_functions.
iDestruct "Hst" as (ν' q') "(>EQν & _ & Hh & _ & >Hq & >Hν')".
rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
iApply (step_fupd_mask_mono (lftN ( rwlockN lftN)));
last iApply (step_fupd_mask_frame_r _ (lft_userN)); [set_solver+ || solve_ndisj..| |].
iApply (step_fupd_mask_mono ((lftN lft_userN) ( rwlockN lftN lft_userN)));
last iApply (step_fupd_mask_frame_r _ (lft_userN)).
{ set_solver-. }
{ solve_ndisj. }
{ rewrite difference_difference. apply: disjoint_difference_r1. done. }
{ (* FIXME [solve_ndisj] fails. *)
apply: disjoint_difference_r1. solve_ndisj. }
apply: disjoint_difference_r1. done. }
iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
{ set_solver-. }
iMod "Hclose" as "_". iIntros "!> Hlx". iExists None. iFrame.
iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
- iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
......
......@@ -181,8 +181,8 @@ Section typing_rules.
iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_mask_mono _ (lftN)); first done.
iApply (wp_step_fupd with "Hend"); first solve_ndisj. wp_seq.
iApply (wp_mask_mono _ (lftN lft_userN)); first done.
iApply (wp_step_fupd with "Hend"); first set_solver-. wp_seq.
iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
Qed.
......
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