Commit 2e7d222c authored by George Pîrlea's avatar George Pîrlea Committed by Michael Sammler

Add pinning to model of types

parent 9f72ef66
Pipeline #44023 passed with stage
in 22 minutes and 7 seconds
......@@ -29,7 +29,7 @@ Section borrow.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
rewrite !tctx_interp_singleton /=.
iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
iMod (ty.(ty_share) with "LFT Huniq Htok") as "[Hown Htok]"; [solve_ndisj|].
iMod (ty.(ty_share) NotPinned with "LFT Huniq Htok") as "[Hown Htok]"; [solve_ndisj| ].
iMod ("Hclose" with "Htok") as "[$ $]". iExists _. by iFrame "%∗".
Qed.
......
......@@ -58,7 +58,7 @@ Section fixpoint.
use limit_preserving_and directly. However, on the Coq side, it is
more convenient as a record -- so this is where we pay. *)
eapply (limit_preserving_ext (λ _, _ _)).
{ split; (intros [H1 H2]; split; [apply H1|apply H2]). }
{ split; (intros [Hc1 Hc2]; split; [apply Hc1|apply Hc2]). }
apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
+ apply bi.limit_preserving_Persistent; solve_proper.
+ apply limit_preserving_impl, bi.limit_preserving_entails;
......@@ -73,8 +73,10 @@ Section fixpoint.
- apply send_equiv.
- exists bool. apply _.
- done.
- repeat (apply limit_preserving_forall=> ?).
apply bi.limit_preserving_entails; solve_proper.
- eapply (limit_preserving_ext (λ _, _ _)).
{ split; (intros [Hs1 Hs2]; split; [apply Hs1|apply Hs2]). }
apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
all: apply bi.limit_preserving_entails; solve_proper_core ltac:(fun _ => f_equiv).
Qed.
Global Instance fixpoint_sync :
......@@ -86,14 +88,14 @@ Section fixpoint.
- exists bool. apply _.
- done.
- repeat (apply limit_preserving_forall=> ?).
apply bi.limit_preserving_entails; solve_proper.
apply bi.limit_preserving_entails; solve_proper_core ltac:(fun _ => f_equiv).
Qed.
Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
Proof.
unfold eqtype, subtype, type_incl.
setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
split; iIntros (qmax qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
split; iIntros (qmax qL) "_ !# _"; (iSplit; first done); (iSplit; [|iSplit]); iIntros "!#*$".
Qed.
End fixpoint.
......
......@@ -44,7 +44,7 @@ Section fn.
{ ty_lfts := []; ty_wf_E := [] }.
Global Instance fn_send fp : Send (fn fp).
Proof. iIntros (tid1 tid2 vl). done. Qed.
Proof. apply: ty_of_st_send. iIntros (tid1 tid2 vl). done. Qed.
Definition fn_params_rel (ty_rel : relation type) : relation fn_params :=
λ fp1 fp2,
......@@ -77,7 +77,7 @@ Section fn.
type_dist2 n') fn.
Proof.
intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
constructor; unfold ty_own; simpl.
constructor; unfold ty_own_val; simpl.
(* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
(* The clean way to do this would be to have a metric on type contexts. Oh well. *)
intros tid vl. unfold typed_body.
......@@ -246,7 +246,7 @@ Section typing.
([ list] y zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)),
tctx_elt_interp tid y) -
( ret, na_own tid top - llctx_interp_noend qmax L qL - qκs.[lft_intersect_list κs] -
(box (fp x).(fp_ty)).(ty_own) tid [ret] -
(box (fp x).(fp_ty)).(ty_own_val) tid [ret] -
WP k [of_val ret] {{ _, cont_postcondition }}) -
WP (call: p ps k) {{ _, cont_postcondition }}.
Proof.
......@@ -310,11 +310,11 @@ Section typing.
AsVal k
lft_ctx - elctx_interp E - na_own tid -
qκs.[lft_intersect_list κs] -
(fn fp).(ty_own) tid [f] -
(fn fp).(ty_own_val) tid [f] -
([ list] y zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)),
tctx_elt_interp tid y) -
( ret, na_own tid top - qκs.[lft_intersect_list κs] -
(box (fp x).(fp_ty)).(ty_own) tid [ret] -
(box (fp x).(fp_ty)).(ty_own_val) tid [ret] -
WP k [of_val ret] {{ _, cont_postcondition }}) -
WP (call: f ps k) {{ _, cont_postcondition }}.
Proof.
......
......@@ -25,9 +25,9 @@ Section arc.
(* We use this disjunction, and not simply [ty_shr] here, *)
(* because [weak_new] cannot prove ty_shr, even for a dead *)
(* lifetime. *)
(ty.(ty_shr) ν tid (l + 2) [†ν])
(ty.(ty_shr) ν tid NotPinned (l + 2) [†ν])
(1.[ν] ={lftN lft_userN arc_endN}[lft_userN]=
[†ν] (l + 2) ↦∗: ty.(ty_own) tid l(2 + ty.(ty_size))))%I.
[†ν] (l + 2) ↦∗: ty.(ty_own_val) tid l(2 + ty.(ty_size))))%I.
Global Instance arc_persist_ne tid ν γ l n :
Proper (type_dist2 n ==> dist n) (arc_persist tid ν γ l).
......@@ -40,7 +40,7 @@ Section arc.
Lemma arc_persist_type_incl tid ν γ l ty1 ty2:
type_incl ty1 ty2 - arc_persist tid ν γ l ty1 - arc_persist tid ν γ l ty2.
Proof.
iIntros "#(Heqsz & Hinclo & Hincls) #(?& Hs & Hvs)".
iIntros "#(Heqsz & Hinclo & Hinclp & Hincls) #(?& Hs & Hvs)".
iDestruct "Heqsz" as %->. iFrame "#". iSplit.
- iDestruct "Hs" as "[?|?]"; last auto. iLeft. by iApply "Hincls".
- iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
......@@ -54,7 +54,7 @@ Section arc.
iIntros "#($ & ? & Hvs)". rewrite sync_change_tid. iFrame "#".
iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "?". iExists _.
by rewrite send_change_tid.
by rewrite send_val_change_tid.
Qed.
(* Model of arc *)
......@@ -64,7 +64,7 @@ Section arc.
masks to rebuild the invariants. *)
Definition full_arc_own l ty tid : iProp Σ:=
(l #1 (l + 1) #1 l(2 + ty.(ty_size))
(l + 2) ↦∗: ty.(ty_own) tid)%I.
(l + 2) ↦∗: ty.(ty_own_val) tid)%I.
Definition shared_arc_own l ty tid : iProp Σ:=
( γ ν q, arc_persist tid ν γ l ty arc_tok γ q q.[ν])%I.
Lemma arc_own_share E l ty tid :
......@@ -78,7 +78,7 @@ Section arc.
longer necessary. *)
iApply fupd_trans. iApply (fupd_mask_mono (lftN))=>//.
iMod (bor_create _ ν with "LFT Hown") as "[HP HPend]"=>//. iModIntro.
iMod (ty_share with "LFT HP Hν") as "[#? Hν]"; first solve_ndisj.
iMod (ty_share _ NotPinned with "LFT HP Hν") as "[#? Hν]"; first solve_ndisj.
iMod (create_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN with "Hl1 Hl2 Hν")
as (γ q') "(#? & ? & ?)".
iExists _, _, _. iFrame "∗#". iCombine "H†" "HPend" as "H".
......@@ -97,13 +97,13 @@ Section arc.
iMod "Hclose2" as "_". iApply "Hclose". auto.
Qed.
Program Definition arc (ty : type) :=
{| ty_size := 1;
ty_own tid vl :=
Program Definition arc (ty : type) : type :=
{| ut_size := 1;
ut_own tid vl :=
match vl return _ with
| [ #(LitLoc l) ] => full_arc_own l ty tid shared_arc_own l ty tid
| _ => False end;
ty_shr κ tid l :=
ut_shr κ tid l :=
(l' : loc), &frac{κ} (λ q, l {q} #l')
F q, ⌜↑shrN lftE F - q.[κ]
={F}[F∖↑shrN]= q.[κ] γ ν q', κ ν
......@@ -176,8 +176,8 @@ Section arc.
Lemma arc_subtype ty1 ty2 :
type_incl ty1 ty2 - type_incl (arc ty1) (arc ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
iSplit; first done. iSplit; iModIntro.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hpincl & #Hsincl)".
iApply type_incl_unpin_type; simpl; [done | iModIntro..].
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
{ iLeft. iFrame. iDestruct "Hsz" as %->.
......@@ -204,9 +204,10 @@ Section arc.
Global Instance arc_send ty :
Send ty Sync ty Send (arc ty).
Proof.
intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
move => ??. apply: ty_of_ut_send => /=.
intros tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
unfold full_arc_own, shared_arc_own.
repeat (apply send_change_tid || apply bi.exist_mono ||
repeat (apply send_val_change_tid || apply bi.exist_mono ||
(apply arc_persist_send; apply _) || f_equiv || intros ?).
Qed.
......@@ -219,13 +220,13 @@ Section arc.
Qed.
(* Model of weak *)
Program Definition weak (ty : type) :=
{| ty_size := 1;
ty_own tid vl :=
Program Definition weak (ty : type) : type :=
{| ut_size := 1;
ut_own tid vl :=
match vl return _ with
| [ #(LitLoc l) ] => γ ν, arc_persist tid ν γ l ty weak_tok γ
| _ => False end;
ty_shr κ tid l :=
ut_shr κ tid l :=
(l' : loc), &frac{κ} (λ q, l {q} #l')
F q, ⌜↑shrN lftE F - q.[κ]
={F}[F∖↑shrN]= q.[κ] γ ν,
......@@ -289,8 +290,8 @@ Section arc.
Lemma weak_subtype ty1 ty2 :
type_incl ty1 ty2 - type_incl (weak ty1) (weak ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
iSplit; first done. iSplit; iModIntro.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hpincl & #Hsincl)".
iApply type_incl_unpin_type; simpl; [done|iModIntro..].
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as (γ ν) "(#Hpersist & Htk)".
iExists _, _. iFrame "#∗". by iApply arc_persist_type_incl.
......@@ -313,8 +314,9 @@ Section arc.
Global Instance weak_send ty :
Send ty Sync ty Send (weak ty).
Proof.
intros Hse Hsy tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
repeat (apply send_change_tid || apply bi.exist_mono ||
move => ??. apply: ty_of_ut_send => /=.
intros tid tid' vl. destruct vl as [|[[|l|]|] []]=>//=.
repeat (apply send_val_change_tid || apply bi.exist_mono ||
(apply arc_persist_send; apply _) || f_equiv || intros ?).
Qed.
......@@ -761,7 +763,7 @@ Section arc.
wp_bind (drop_arc _). iApply (drop_arc_spec with "[] [$Htok Hν]");
[by iDestruct "Hpersist" as "[$?]"|done|].
iNext. iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
iApply (wp_wand _ _ _ (λ _, ty_own_val (box (option ty)) tid [r])%I with "[Hdrop Hr]").
{ destruct b; wp_if=>//. destruct r as [[]|]; try done.
(* FIXME: 'simpl' reveals a match here. Didn't we forbid that for ty_own? *)
rewrite {3}[option]lock. simpl. rewrite -{2 3}lock. (* FIXME: Tried using contextual pattern, did not work. *)
......@@ -1050,7 +1052,7 @@ Section arc.
iApply type_assign; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
- iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
- 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 *) set_solver-. }
wp_apply wp_new=>//. lia. iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>".
......@@ -1062,7 +1064,7 @@ Section arc.
wp_apply (wp_memcpy with "[$Hrc2 $H↦]").
{ by rewrite repeat_length. } { by rewrite Hsz. }
iIntros "[H↦ H↦']". wp_seq. wp_write.
iMod ("Hclose2" $! ((l + 2) ↦∗: ty_own ty tid)%I
iMod ("Hclose2" $! ((l + 2) ↦∗: ty_own_val ty tid)%I
with "[Hrc'↦ Hrc0 Hrc1 H†] [H↦ Hown]") as "[Hb Hα1]"; [|by auto with iFrame|].
{ iIntros "!> H↦". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//. }
......@@ -1104,7 +1106,7 @@ Section arc.
wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
[lia|by replace (length vl) with (ty.(ty_size))|].
iIntros "_". wp_seq. wp_write.
iMod ("Hclose2" $! ((l' + 2) ↦∗: ty_own ty tid)%I with
iMod ("Hclose2" $! ((l' + 2) ↦∗: ty_own_val ty tid)%I with
"[Hrc'↦ Hl' Hl'1 Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
{ iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
......
......@@ -29,10 +29,10 @@ Section brandedvec.
( γ, lft_meta α γ own γ ( MaxNat n))%I.
Program Definition brandvec (α : lft) : type :=
{| ty_size := int.(ty_size);
ty_own tid vl :=
{| ut_size := int.(ty_size);
ut_own tid vl :=
( n, brandvec_inv α n vl = [ #n ])%I;
ty_shr κ tid l :=
ut_shr κ tid l :=
( n, &at{κ,brandvecN}(brandvec_inv α n) &frac{κ}(λ q, l ↦∗{q} [ #n ]))%I;
|}.
Next Obligation. iIntros "* H". iDestruct "H" as (?) "[_ %]". by subst. Qed.
......@@ -68,7 +68,7 @@ Section brandedvec.
Global Instance brandvec_send α :
Send (brandvec α).
Proof. by unfold brandvec, Send. Qed.
Proof. by apply ty_of_ut_send. Qed.
Global Instance brandvec_sync α :
Sync (brandvec α).
......@@ -79,10 +79,10 @@ Section brandedvec.
Definition brandidx_inv α m : iProp :=
( γ, lft_meta α γ own γ ( MaxNat (m+1)%nat))%I.
Program Definition brandidx α :=
{| ty_size := int.(ty_size);
ty_own tid vl := ( m, brandidx_inv α m vl = [ #m])%I;
ty_shr κ tid l := ( m, &frac{κ}(λ q, l ↦∗{q} [ #m]) brandidx_inv α m)%I;
Program Definition brandidx α : type :=
{| ut_size := int.(ty_size);
ut_own tid vl := ( m, brandidx_inv α m vl = [ #m])%I;
ut_shr κ tid l := ( m, &frac{κ}(λ q, l ↦∗{q} [ #m]) brandidx_inv α m)%I;
|}.
Next Obligation. iIntros "* H". iDestruct "H" as (?) "[_ %]". by subst. Qed.
Next Obligation.
......@@ -114,7 +114,7 @@ Section brandedvec.
Global Instance brandidx_send α :
Send (brandidx α).
Proof. by unfold brandidx, Send. Qed.
Proof. by apply: ty_of_ut_send. Qed.
Global Instance brandidx_sync α :
Sync (brandidx α).
......@@ -150,7 +150,7 @@ Section brandedvec.
iIntros "Hn Hm".
iDestruct "Hn" as (γn) "(Hidx1 & Hn)".
iDestruct "Hm" as (γm) "(Hidx2 & Hm)".
iDestruct (lft_meta_agree with "Hidx1 Hidx2") as %<-.
iDestruct (lft_meta_agree with "Hidx1 Hidx2") as %<-.
iDestruct (own_valid_2 with "Hn Hm") as %[?%max_nat_included ?]%auth_both_valid_discrete.
iPureIntro. simpl in *. lia.
Qed.
......
......@@ -8,10 +8,10 @@ Set Default Proof Using "Type".
Section cell.
Context `{!typeG Σ}.
Program Definition cell (ty : type) :=
{| ty_size := ty.(ty_size);
ty_own := ty.(ty_own);
ty_shr κ tid l := (&na{κ, tid, shrN.@l}(l ↦∗: ty.(ty_own) tid))%I |}.
Program Definition cell (ty : type) : type :=
{| ut_size := ty.(ty_size);
ut_own := ty.(ty_own_val);
ut_shr κ tid l := (&na{κ, tid, shrN.@l}(l ↦∗: ty.(ty_own_val) tid))%I |}.
Next Obligation. apply ty_size_eq. Qed.
Next Obligation.
iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
......@@ -36,8 +36,8 @@ Section cell.
Proof.
move=>?? /eqtype_unfold EQ. iIntros (??) "HL".
iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE".
iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
iSplit; [done|iSplit; iIntros "!# * H"].
iDestruct ("EQ" with "HE") as "(% & #Hown & #Hpin & #Hshr)".
iApply type_incl_unpin_type; [done|iIntros "/=!# * H"..].
- iApply ("Hown" with "H").
- iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H";
iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
......@@ -52,7 +52,7 @@ Section cell.
Global Instance cell_copy ty :
Copy ty Copy (cell ty).
Proof.
intros Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
intros Hcopy. split; first by intros; simpl; unfold ty_own_val; apply _.
iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
(* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
......@@ -75,7 +75,7 @@ Section cell.
Global Instance cell_send ty :
Send ty Send (cell ty).
Proof. by unfold cell, Send. Qed.
Proof. move => ?. apply: ty_of_ut_send => /=. apply: send_val_change_tid. Qed.
End cell.
Section typing.
......
......@@ -17,7 +17,7 @@ Section fake_shared.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
rewrite tctx_interp_singleton tctx_hasty_val.
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "%"; [solve_typing..|].
iAssert ( ty_own (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
iAssert ( ty_own_val (own_ptr 1 (&shr{α}(box ty))) tid [x])%I with "[HT]" as "HT".
{ destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
......@@ -48,7 +48,7 @@ Section fake_shared.
rewrite tctx_interp_singleton tctx_hasty_val.
iDestruct (lctx_lft_incl_incl α β with "HL HE") as "%"; [solve_typing..|].
(* FIXME: WTF, using &uniq{β} here does not work. *)
iAssert ( ty_own (own_ptr 1 (&shr{α} (uniq_bor β ty))) tid [x])%I with "[HT]" as "HT".
iAssert ( ty_own_val (own_ptr 1 (&shr{α} (uniq_bor β ty))) tid [x])%I with "[HT]" as "HT".
{ destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
......
......@@ -60,13 +60,13 @@ Section ghostcell.
rewrite agree_idemp. done.
Qed.
Program Definition ghosttoken α :=
Program Definition ghosttoken α : type :=
tc_opaque
{| ty_size := 0;
ty_own tid vl :=
{| ut_size := 0;
ut_own tid vl :=
(vl = [] γ, lft_meta α γ
own γ (ghosttoken_st_to_R None))%I;
ty_shr κ tid l :=
ut_shr κ tid l :=
( γ, lft_meta α γ
κ', κ κ'
&frac{κ'}(λ q, own γ (ghosttoken_st_to_R (Some (κ',q)))))%I;
......@@ -101,7 +101,7 @@ Section ghostcell.
iExists κ''.
by iSplit; first iApply lft_incl_trans.
Qed.
Global Instance ghosttoken_wf α : TyWf (ghosttoken α) :=
{ ty_lfts := [α]; ty_wf_E := [] }.
......@@ -126,10 +126,8 @@ Section ghostcell.
iIntros "!# #HE".
iDestruct ("EQ1'" with "HE") as %EQ1'.
iDestruct ("EQ2'" with "HE") as %EQ2'.
iSplit; [|iSplit; iIntros "!# * H"]; simpl.
- iPureIntro; congruence.
- solve_proper_prepare.
iDestruct "H" as "[$ H]".
iApply type_incl_unpin_type; simpl; [done |iIntros "!# * H"..].
- iDestruct "H" as "[$ H]".
iDestruct "H" as (γ) "H".
iExists γ; iDestruct "H" as "[H $]".
by rewrite (lft_incl_syn_anti_symm _ _ EQ1' EQ2').
......@@ -150,7 +148,7 @@ Section ghostcell.
Definition ghostcell_inv tid l β α ty : iProp Σ :=
( st',
match st' with
| None => &{β}(l ↦∗: ty.(ty_own) tid) (* ghostcell is not currently being accessed *)
| None => &{β}(l ↦∗: ty.(ty_own_val) tid) (* ghostcell is not currently being accessed *)
| Some rw => γ, lft_meta α γ
match rw with
| true => (* ghostcell is currently being write-accessed *)
......@@ -161,7 +159,7 @@ Section ghostcell.
here) or we can run the inheritance to get back the full
borrow. *)
κ', &{κ'} (own γ (ghosttoken_st_to_R None))
([†κ'] ={lftN}= &{β} (l ↦∗: ty_own ty tid))
([†κ'] ={lftN}= &{β} (l ↦∗: ty_own_val ty tid))
| false => (* ghostcell is currently being read-accessed *)
(* The κ' will be set to the total lifetime for which the token is
shared. If we own the ghost token fragment in [None] state, then
......@@ -172,8 +170,8 @@ Section ghostcell.
means it lives long enough to return it to the caller at that
lifetime. *)
κ', &frac{κ'} (λ q', own γ (ghosttoken_st_to_R (Some (κ', q'))))
([†κ'] ={lftN}= &{β}(l ↦∗: ty.(ty_own) tid))
ty.(ty_shr) (β κ') tid l
([†κ'] ={lftN}= &{β}(l ↦∗: ty.(ty_own_val) tid))
ty.(ty_shr) (β κ') tid NotPinned l
end
end)%I.
......@@ -202,11 +200,11 @@ Section ghostcell.
iDestruct (Hlft1 with "HL") as "#Hlft1".
iDestruct (Hlft2 with "HL") as "#Hlft2".
iIntros (tid l β) "!# #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hpin & #Hshr)".
iDestruct ("Hlft1" with "HE") as %Hκ1.
iDestruct ("Hlft2" with "HE") as %Hκ2.
iAssert ( (&{β}(l ↦∗: ty_own ty1 tid) -
&{β}(l ↦∗: ty_own ty2 tid)))%I as "#Hb".
iAssert ( (&{β}(l ↦∗: ty_own_val ty1 tid) -
&{β}(l ↦∗: ty_own_val ty2 tid)))%I as "#Hb".
{ iIntros "!# H". iApply bor_iff; last done.
iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
......@@ -247,11 +245,11 @@ Section ghostcell.
(when the lifetime is dead it can
be removed from the track set).
*)
Program Definition ghostcell (α : lft) (ty : type) :=
Program Definition ghostcell (α : lft) (ty : type) : type :=
tc_opaque
{| ty_size := ty.(ty_size);
ty_own tid vl := ty.(ty_own) tid vl;
ty_shr κ tid l :=
{| ut_size := ty.(ty_size);
ut_own tid vl := ty.(ty_own_val) tid vl;
ut_shr κ tid l :=
( β, κ β &at{β, ghostcellN}(ghostcell_inv tid l β α ty))%I |}.
Next Obligation.
iIntros (????) "H". by rewrite ty_size_eq.
......@@ -303,8 +301,8 @@ Section ghostcell.
iDestruct (EQ'2 with "HL") as "#EQ'".
iDestruct (ghostcell_inv_proper _ _ κ κ' with "HL") as "#Hty1ty2"; [done|done|].
iDestruct (ghostcell_inv_proper _ _ κ' κ with "HL") as "#Hty2ty1"; [done|by symmetry|].
iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
iSplit; [|iSplit; iIntros "!# * H"]; simpl.
iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hpin & #Hshr)".
iApply type_incl_unpin_type; simpl; [|iIntros "!# * H"..].
- iPureIntro; congruence.
- by iApply "Hown".
- iDestruct "H" as (a) "H".
......@@ -333,7 +331,7 @@ Section ghostcell.
Global Instance ghostcell_send α ty :
Send ty Send (ghostcell α ty).
Proof. by unfold ghostcell, Send. Qed.
Proof. move => ?. apply ty_of_ut_send. by apply: send_val_change_tid. Qed.
Global Instance ghostcell_sync α ty :
Send ty Sync ty Sync (ghostcell α ty).
......@@ -416,7 +414,7 @@ Section ghostcell.
iIntros (α ϝ ret args). inv_vec args=>n. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk Hn".
rewrite tctx_interp_singleton tctx_hasty_val.
iAssert (ty_own (box (ghostcell α ty)) tid [n])%I with "[Hn]" as "Hn".
iAssert (ty_own_val (box (ghostcell α ty)) tid [n])%I with "[Hn]" as "Hn".
{ rewrite !ownptr_own.
iDestruct "Hn" as (l vl) "(% & Hl & Hown & Hfree)".
by iExists l, vl; simpl; iFrame "Hl Hown Hfree". }
......@@ -439,19 +437,19 @@ Section ghostcell.
&frac{κ'} (λ q : Qp, own γ (ghosttoken_st_to_R (Some (κ', q)))) -
(qβ).[β] -
lft_meta α γ -
&{κ} (lc ↦∗: ty_own ty tid) ={E}=
&{κ} (lc ↦∗: ty_own_val ty tid) ={E}=
ghostcell_inv tid lc κ α ty
ty_shr ty β tid lc (qβ).[β]).
ty_shr ty β tid NotPinned lc (qβ).[β]).
Proof.
iIntros (HE) "#LFT #Hκ #Hβκ' #Hfractok [Hβ1 Hβ2] Hsing Hst'".
iMod (fupd_mask_subseteq (lftN)) as "Hclose"; first solve_ndisj.
iMod (lft_incl_acc with "Hκ Hβ1") as (q''2) "[Hq'' Hcloseq'']"; first solve_ndisj.
iMod (lft_incl_acc with "Hβκ' Hβ2") as (q''2_2) "[Hq''_2 Hcloseq''_2]";
first solve_ndisj.
iMod (rebor _ _ (κ κ') (lc ↦∗: ty_own ty tid)%I with "LFT [] [Hst']")
iMod (rebor _ _ (κ κ') (lc ↦∗: ty_own_val ty tid)%I with "LFT [] [Hst']")
as "[Hvl Hh]"; [done|iApply lft_intersect_incl_l|done|].
iDestruct (lft_intersect_acc with "Hq'' Hq''_2") as (q''3) "[Hq'' Hcloseq''2]".
iMod (ty_share with "LFT Hvl Hq''") as "[#Hshr Hq'']"; first solve_ndisj.
iMod (ty_share _ NotPinned with "LFT Hvl Hq''") as "[#Hshr Hq'']"; first solve_ndisj.
iDestruct ("Hcloseq''2" with "Hq''") as "[Hq'' Hq''_2]".
iMod ("Hcloseq''" with "Hq''") as "$".
iMod ("Hcloseq''_2" with "Hq''_2") as "$".
......@@ -473,7 +471,7 @@ Section ghostcell.
rewrite !tctx_hasty_val.
iMod (lctx_lft_alive_tok β with "HE HL")
as (qβ) "([Hβ1 [Hβ2 Hβ3]] & HL & Hclose)"; [solve_typing..|].
iAssert ( |={}[∖↑ghostcellN]=> (ty_own (box (&shr{β} ty)) tid [c] (qβ).[β]))%I
iAssert ( |={}[∖↑ghostcellN]=> (ty_own_val (box (&shr{β} ty)) tid [c] (qβ).[β]))%I
with "[Hβ1 Hβ2 Hβ3 Hs Hc]"as "Hc".
{ iClear "HE".
rewrite (ownptr_own (_ (_ (ghostcell _ _))))
......@@ -599,7 +597,7 @@ Section ghostcell.
rewrite !tctx_hasty_val.