Skip to content
Snippets Groups Projects
Commit e189f4ad authored by Hai Dang's avatar Hai Dang
Browse files

Use Atomic ptsto and cancelable inv for spawn and join

parent e83da50a
No related branches found
No related tags found
No related merge requests found
Pipeline #62189 passed
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl.
From lrust.lang Require Import notation.
From gpfsl.logic Require Import view_invariants.
From gpfsl.gps Require Import surface protocols escrows.
From gpfsl.logic Require Import proofmode atomics view_invariants.
From iris.prelude Require Import options.
......@@ -16,8 +14,8 @@ Definition spawn : val :=
Definition finish : val :=
λ: ["c"; "v"],
"c" + #1 <- "v";; (* Store data (non-atomically). *)
"c" <-ʳᵉˡ #1;; (* Signal that we finished (atomically!) *)
#☠.
"c" <-ʳᵉˡ #1 (* Signal that we finished (atomically!) *)
.
Definition join : val :=
rec: "join" ["c"] :=
if: !ᵃᶜ"c" then
......@@ -30,148 +28,200 @@ Definition join : val :=
(** The CMRA & functor we need. *)
Class spawnG Σ := SpawnG {
spawn_tokG :> inG Σ (exclR unitO);
spawn_gpsG :> gpsG Σ unitProtocol;
spawn_atomG :> atomicG Σ;
spawn_viewG :> view_invG Σ }.
Definition spawnΣ : gFunctors :=
#[GFunctor (exclR unitO); gpsΣ unitProtocol; atomicΣ; view_invΣ].
Definition spawnΣ : gFunctors := #[atomicΣ; view_invΣ].
Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!noprolG Σ, !spawnG Σ, !view_invG Σ} (N : namespace).
Context `{!noprolG Σ, !spawnG Σ} (N : namespace).
Local Notation vProp := (vProp Σ).
Local Notation tok γ := (own γ (Excl ())).
Implicit Types (c: loc) (Ψ : val vProp) (v: val).
Definition finishEscrow γc γe γi c Ψ :=
([es tok γe (( t, GPS_SWWriter c t () #1 γc) view_tok γi (1/2)%Qp
v, (c >> 1) v Ψ v)])%I.
(* GPS protocol interpretation *)
Definition spawn_interp γe γi Ψ : interpO Σ unitProtocol :=
(λ _ c γc _ _ v, b : bool, v = #b
if b then finishEscrow γc γe γi c Ψ else True)%I.
Let IW : loc gname time unitProtocol val vProp :=
(λ _ _ _ _ v, v = #false)%I.
Definition finish_handle γc γe c Ψ : vProp :=
( γi t v, (c >> 1) v
GPS_vSP_Writer N (spawn_interp γe γi Ψ) IW c t () #0 γc γi
Local Definition mp_inv_reclaim'_def γc γi c Ψ : vProp :=
( ζ (b : bool) t0 V0,
c sw{γc} ζ
let ζ0 : absHist := {[t0 := (#0, V0)]} in
match b with
| false => ζ = ζ0
| true => t1 V1, (t0 < t1)%positive ζ = <[t1 := (#1, V1)]>ζ0
@{V1} ( v, (c >> 1) v Ψ v view_tok γi (1/2))
end
)%I.
Local Definition mp_inv_reclaim'_aux : seal (@mp_inv_reclaim'_def). Proof. by eexists. Qed.
Local Definition mp_inv_reclaim' := unseal (@mp_inv_reclaim'_aux).
Local Definition mp_inv_reclaim'_eq : @mp_inv_reclaim' = _ := seal_eq _.
(* We don't care about objectivity when using view_inv *)
Local Definition mp_inv_reclaim γc γi c Ψ :=
view_inv γi N (mp_inv_reclaim' γc γi c Ψ).
Definition finish_handle γc c Ψ : vProp :=
( γi t V v, (c >> 1) v
c sw{γc} {[t := (#0, V)]}
mp_inv_reclaim γc γi c Ψ
view_tok γi (1/2)%Qp)%I.
Definition join_handle γc γe c Ψ : vProp :=
( γi (Ψ': val vProp) t,
GPS_vSP_Reader N (spawn_interp γe γi Ψ') IW c t () #0 γc γi
c 2 tok γe
Definition join_handle γc c Ψ : vProp :=
( γi (Ψ': val vProp) t V,
c sn{γc} {[t := (#0, V)]}
mp_inv_reclaim γc γi c Ψ'
c 2
view_tok γi (1/2)%Qp
( v, Ψ' v -∗ Ψ v))%I.
Global Instance finish_handle_contractive n γc γe c :
Proper (pointwise_relation val (dist_later n) ==> dist n) (finish_handle γc γe c).
Global Instance finish_handle_contractive n γc c :
Proper (pointwise_relation val (dist_later n) ==> dist n) (finish_handle γc c).
Proof.
move => ???. do 3 (apply bi.exist_ne => ?).
apply bi.sep_ne; [done|]. apply bi.sep_ne; [|done].
apply GPS_vSP_Writer_contractive; [|done]. destruct n; [done|].
simpl => ??????. apply bi.exist_ne => b'.
apply bi.sep_ne; [done|]. destruct b'; [|done]. solve_proper.
rewrite /finish_handle /mp_inv_reclaim mp_inv_reclaim'_eq /mp_inv_reclaim'_def.
solve_contractive.
Qed.
Global Instance join_handle_ne n γc γe c :
Proper (pointwise_relation val (dist n) ==> dist n) (join_handle γc γe c).
Global Instance join_handle_ne n γc c :
Proper (pointwise_relation val (dist n) ==> dist n) (join_handle γc c).
Proof. solve_proper. Qed.
(** The main proofs. *)
Lemma spawn_spec Ψ e (f : val) tid :
IntoVal e f
{{{ γc γe c tid', finish_handle γc γe c Ψ -∗ WP f [ #c] @ tid'; {{ _, True }} }}}
{{{ γc c tid', finish_handle γc c Ψ -∗ WP f [ #c] @ tid'; {{ _, True }} }}}
spawn [e] @ tid;
{{{ γc γe c, RET #c; join_handle γc γe c Ψ }}}.
{{{ γc c, RET #c; join_handle γc c Ψ }}}.
Proof.
iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
wp_let. wp_alloc l as "Hm" "Hl" "H†". wp_let.
iMod (own_alloc (Excl ())) as (γe) "Hγe"; first done.
wp_let. wp_alloc c as "Hm" "Hl" "H†". wp_let.
rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write.
iMod (GPS_vSP_Init N (λ γi, spawn_interp γe γi Ψ) (λ _, IW) _ () with "Hc []")
as (γi γc t) "[[Htok1 Htok2] SW]". { iIntros (???). by iExists false. }
iDestruct (GPS_vSP_SWWriter_Reader with "SW") as "#R".
iMod (AtomicPtsTo_from_na with "Hc") as (γc t Vc) "(sVc & SW & SP)".
iMod (view_inv_alloc N) as (γi) "VS".
iMod ("VS" $! (mp_inv_reclaim' γc γi c Ψ) with "[SP]") as "[#Inv [Htok1 Htok2]]".
{ iNext. rewrite mp_inv_reclaim'_eq. iExists _, false, t, Vc. by iFrame. }
iDestruct (AtomicSWriter_AtomicSeen with "SW") as "#R".
wp_apply (wp_fork with "[SW Htok1 Hf Hd]"); [done|..].
- iNext. iIntros (tid'). iApply "Hf". iExists _, _, _. by iFrame.
- iIntros "_". wp_seq. iApply ("HΦ" $! γc γe). iExists _, _, _.
iFrame "R ∗". auto.
- iNext. iIntros (tid'). iApply "Hf". iExists _, _, _, _. by iFrame.
- iIntros "_". wp_seq. iApply ("HΦ" $! γc). iExists _, _, _, _.
iFrame "Inv R ∗". auto.
Qed.
Lemma finish_spec Ψ c v γc γe tid
(DISJ1: (histN) ## (N : coPset)) (DISJ2: (escrowN) ## (N : coPset)) :
{{{ finish_handle γc γe c Ψ Ψ v }}}
Lemma finish_spec Ψ c v γc tid
(DISJ1: (histN) ## (N : coPset)) :
{{{ finish_handle γc c Ψ Ψ v }}}
finish [ #c; v] @ tid;
{{{ RET #☠; True }}}.
Proof.
iIntros (Φ) "[Hfin HΨ] HΦ".
iDestruct "Hfin" as (γi t v0) "(Hd & SW & Hf)".
wp_lam. wp_op. wp_write. wp_bind (_ <-ʳᵉˡ _)%E.
iApply (GPS_vSP_SWWrite_rel N (spawn_interp γe γi Ψ) IW _ (1 / 2)%Qp
(λ _, True)%I True%I (spawn_interp γe γi Ψ true c γc t tt #0)
t () () _ #1 with "[$Hf $SW HΨ Hd]"); [done..| |].
{ iSplitR "".
- iIntros "!>" (t' Ext') "SW _ tok !>". iSplitL ""; [by iIntros "!> _"|].
iSplitR ""; [|done]. iExists true.
iSplitL ""; [done|]. iApply escrow_alloc; [solve_ndisj|]. iFrame.
iSplitL "SW"; iExists _; by iFrame.
- by iIntros "!> !> $". }
iIntros "!>" (t') "_". wp_seq. by iApply "HΦ".
iDestruct "Hfin" as (γi t v0 V) "(Hd & SW & #Inv & vTok1)".
wp_lam. wp_op. wp_write.
iMod (view_inv_acc_base' with "[$Inv $vTok1]") as "(vTok1 & INV) {Inv}"; [done|].
iDestruct "INV" as (Vb) "[INV Close]".
rewrite {1}mp_inv_reclaim'_eq.
iDestruct "INV" as (ζ' b t0 V0) "[Pts _]".
rewrite view_join_later. iDestruct "Pts" as ">Pts".
iDestruct (monPred_in_bot) as "#sV0".
iDestruct (view_join_elim' with "Pts sV0") as (V') "(#sV' & _ & Pts)".
iDestruct (AtomicPtsTo_AtomicSWriter_agree_1 with "Pts SW") as %->.
iApply (AtomicSWriter_release_write _ _ _ _ V' _ #1
(view_tok γi (1 / 2) (c >> 1) v Ψ v)%I
with "[$SW $Pts $Hd $HΨ $vTok1 $sV']"); [solve_ndisj|..].
iIntros "!>" (t1 V1) "((%MAX & %LeV1 & _) & SeenV1 & [[vTok1 Hm] SW'] & Pts')".
(* reestablishing the invariant *)
rewrite bi.and_elim_r bi.and_elim_l.
iMod ("Close" $! V1 True%I with "vTok1 [-HΦ]").
{ iIntros "vTok1 !>". iSplit; [|done].
rewrite view_at_view_join. iNext. rewrite mp_inv_reclaim'_eq.
iExists _, true, t, _. iSplitL "Pts'"; first by iFrame.
iExists t1, V1. iSplit.
{ iPureIntro. split; [|done]. apply MAX. rewrite lookup_insert. by eexists. }
iExists v. by iFrame. }
iIntros "!>". by iApply "HΦ".
Qed.
Lemma join_spec Ψ c γc γe tid
(DISJ1: (histN) ## (N : coPset)) (DISJ2: (escrowN) ## (N : coPset)) :
{{{ join_handle γc γe c Ψ }}} join [ #c] @ tid; {{{ v, RET v; Ψ v }}}.
Lemma join_spec Ψ c γc tid
(DISJ1: (histN) ## (N : coPset)) :
{{{ join_handle γc c Ψ }}} join [ #c] @ tid; {{{ v, RET v; Ψ v }}}.
Proof.
iIntros (Φ) "H HΦ".
iDestruct "H" as (γi Ψ' t) "(R & (H† & He) & Hj & #HΨ')".
iLöb as "IH" forall (t). wp_rec. wp_bind (!ᵃᶜ _)%E.
set P : vProp := ( tok γe )%I.
iApply (GPS_vSP_SWRead_acq_dealloc N (spawn_interp γe γi Ψ') IW _ P
(λ _ _, v, (c >> 1) {1} v Ψ' v)%I
(spawn_interp γe γi Ψ' false c γc) (1/2)%Qp t () _ #true
with "[$Hj $R $He]"); [done..| |].
{ iSplitL"".
- iIntros "!>" (t' [] v' [_ Ext']) "!>". iSplit; last iSplit.
+ iDestruct 1 as (b) "[#Eq ES]".
destruct b; simpl; [iDestruct "ES" as "#ES"|];
iModIntro; iSplitL ""; iExists _; by iFrame "Eq".
+ iDestruct 1 as (b) "[#Eq ES]".
destruct b; simpl; [iDestruct "ES" as "#ES"|];
iModIntro; iSplitL ""; iExists _; by iFrame "Eq".
+ iDestruct 1 as %?. subst v'. iIntros "!>"; iSplit; [done|by iExists false].
- iIntros "!>" (t' []) "Ext He $".
iDestruct 1 as (b) "[% Es]". destruct b; last done.
iMod (escrow_elim with "[] Es [$He]") as "(SW & >$ & $)"; [solve_ndisj| |done].
iIntros "[He1 He2]". iCombine "He1" "He2" as "He".
iDestruct (own_valid with "He") as "%". auto. }
iIntros "!>" (t' [] v') "(Ext & R & CASE)".
case (decide (v' = #true)) => ?.
- subst v'. iDestruct "CASE" as "[HInv Ho]". iDestruct "Ho" as (v) "[Hd HΨ]".
wp_if. wp_op. wp_read. wp_let. iApply (wp_hist_inv); [done|]. iIntros "Hist".
iMod (GPS_INV_dealloc _ _ _ true with "Hist HInv") as (t1 s1 v1) "[Hc _]"; [done|].
iAssert (c ↦∗ [ v1 ; v])%I with "[Hc Hd]" as "Hc".
iDestruct "H" as (γi Ψ' t V) "(#R & #Inv & H† & vTok2 & #HΨ')".
iLöb as "IH". wp_rec. wp_bind (!ᵃᶜ _)%E.
(* open shared invariant *)
iMod (view_inv_acc_base' with "[$Inv $vTok2]") as "(vTok2 & INV) {Inv}"; [done|].
iDestruct "INV" as (Vb) "[INV Close]".
rewrite {1}mp_inv_reclaim'_eq.
iDestruct "INV" as (ζ' b t0 V0) "[Pts Own]".
(* TODO: IntoLater for view join *)
rewrite view_join_later. iDestruct "Pts" as ">Pts".
iDestruct (monPred_in_bot) as "#sV0".
(* actual read *)
iApply (AtomicSeen_acquire_read_vj with "[$Pts $R $sV0]"); [solve_ndisj|..].
iIntros "!>" (t' v' V' V'' ζ'') "(HF & #SV' & SN' & Pts)".
iDestruct "HF" as %([Sub1 Sub2] & Eqt' & MAX' & LeV'').
case (decide (t' = t0)) => [?|NEqt'].
+ subst t'.
(* we must have read the flag to be 0 (i.e. z = 0). *)
iAssert (v' = #0)%I as %Eq0.
{ destruct b.
- iDestruct "Own" as (t1 V1 [Lt1 Eqζ']) "_".
iPureIntro.
rewrite Eqζ' in Sub2. apply (lookup_weaken _ _ _ _ Eqt') in Sub2.
rewrite lookup_insert_ne in Sub2.
+ rewrite lookup_insert in Sub2. by inversion Sub2.
+ clear -Lt1. intros ?. subst. lia.
- iDestruct "Own" as %Eqζ'. iPureIntro.
rewrite Eqζ' in Sub2. apply (lookup_weaken _ _ _ _ Eqt') in Sub2.
rewrite lookup_insert in Sub2. by inversion Sub2. }
(* then simply keep looping *)
(* first close the invariant *)
rewrite bi.and_elim_l.
iMod ("Close" with "vTok2 [Pts Own]") as "vTok2".
{ iClear "IH". iNext. rewrite mp_inv_reclaim'_eq.
iExists ζ', b, t0, V0. iSplitL "Pts"; by iFrame. }
iIntros "!>". rewrite Eq0. wp_if.
(* then apply the Löb IH *)
by iApply ("IH" with "H† vTok2 HΦ").
+ destruct b; last first.
{ (* b cannot be false *)
iDestruct "Own" as %Eqζ'. exfalso.
rewrite Eqζ' in Sub2.
apply (lookup_weaken _ _ _ _ Eqt'), lookup_singleton_Some in Sub2 as [].
by apply NEqt'. }
iClear "IH".
(* we read 1, the destruct Own to get data. *)
iDestruct "Own" as (t1 V1 [Lt1 Eqζ']) "Own".
rewrite Eqζ' in Sub2. apply (lookup_weaken _ _ _ _ Eqt') in Sub2.
have ? : t' = t1.
{ case (decide (t' = t1)) => [//|NEqt1].
exfalso. by rewrite !lookup_insert_ne // in Sub2. }
subst t'. rewrite lookup_insert in Sub2. inversion Sub2. subst v' V'.
rewrite view_join_view_at.
iDestruct (view_at_elim with "[SV'] Own") as (v) "(Hc1 & HΨ & vTok1)".
{ iApply (monPred_in_mono with "SV'"). simpl. solve_lat. }
(* cancel the invariant *)
iCombine "vTok1" "vTok2" as "vTok".
rewrite 2!bi.and_elim_r.
iDestruct ("Close" with "vTok") as "[#LeVb >_]".
iDestruct (view_join_elim with "Pts LeVb") as "Pts".
iIntros "!>". wp_if. wp_op. wp_read. wp_let.
iApply wp_hist_inv; [done|]. iIntros "HINV".
iMod (AtomicPtsTo_to_na with "HINV Pts") as (t' v') "[Hc _]"; [done|].
iAssert (c ↦∗ [ v' ; v])%I with "[Hc Hc1]" as "Hc".
{ rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iFrame. }
wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
- iDestruct "CASE" as "(Hj & res & He)".
iDestruct "res" as (b) "[% _]". subst v'. destruct b; [done|].
wp_if. iApply ("IH" with "R H† He Hj"). auto.
wp_free; first done. iApply "HΦ". by iApply "HΨ'".
Qed.
Lemma join_handle_impl Ψ1 Ψ2 γc γe c :
( v, Ψ1 v -∗ Ψ2 v) -∗ join_handle γc γe c Ψ1 -∗ join_handle γc γe c Ψ2.
Lemma join_handle_impl Ψ1 Ψ2 γc c :
( v, Ψ1 v -∗ Ψ2 v) -∗ join_handle γc c Ψ1 -∗ join_handle γc c Ψ2.
Proof.
iIntros "#HΨ Hdl". iDestruct "Hdl" as (γi Ψ' t) "(? & (? & ?) & ? & #HΨ')".
iExists γi, Ψ', t. iFrame "#∗". iIntros "!# * ?".
iIntros "#HΨ Hdl". iDestruct "Hdl" as (γi Ψ' t V) "(? & ? & ? & ? & #HΨ')".
iExists γi, Ψ', t, _. iFrame "#∗". iIntros "!# * ?".
iApply "HΨ". iApply "HΨ'". done.
Qed.
End proof.
......
......@@ -51,7 +51,7 @@ Section join.
iApply ((spawn_spec joinN (λ v, (box R_A).(ty_own) tid [v] (qϝ1).[ϝ])%I) with "[HfA HenvA Hϝ1]");
first simpl_subst.
{ (* The new thread. *)
iIntros (γc γe c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
iIntros (γc c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
rewrite !tctx_hasty_val.
iApply (type_call_iris _ [ϝ] () [_] _ (Build_thread_id tid2 tid') with "LFT HE Htl [Hϝ1] HfA [HenvA]").
- rewrite outlives_product. solve_typing.
......@@ -60,7 +60,7 @@ Section join.
- iIntros (r) "Htl Hϝ1 Hret".
wp_rec. iApply (finish_spec with "[$Hfin Hret Hϝ1]"); [solve_ndisj..| |auto].
rewrite right_id. iFrame. by iApply @send_change_tid. }
iNext. iIntros (γc γe c) "Hjoin". wp_let. wp_let.
iNext. iIntros (γc c) "Hjoin". wp_let. wp_let.
iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (qϝ2) "(Hϝ2 & HL & Hclose2)";
[solve_typing..|].
rewrite !tctx_hasty_val.
......
......@@ -16,7 +16,7 @@ Section join_handle.
{| ty_size := 1;
ty_own _ vl :=
match vl return _ with
| [ #(LitLoc l) ] => γc γe, join_handle spawnN γc γe l (join_inv ty)
| [ #(LitLoc l) ] => γc, join_handle spawnN γc l (join_inv ty)
| _ => False
end%I;
ty_shr κ _ l := True%I |}.
......@@ -32,7 +32,7 @@ Section join_handle.
Proof.
iIntros "#Hincl". iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
simpl. iDestruct "Hvl" as (γc γe) "Hvl". iExists γc, γe.
simpl. iDestruct "Hvl" as (γc) "Hvl". iExists γc.
iApply (join_handle_impl with "[] Hvl"). iIntros "!> * Hown" (tid').
iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
iApply "Hincl". done.
......@@ -94,8 +94,8 @@ Section spawn.
iApply (spawn_spec _ (join_inv retty) with "[-]");
last first; last simpl_subst.
{ iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
iIntros "?". iExists _,_. by iFrame. }
iIntros (γc γe c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
iIntros "?". iExists _. by iFrame. }
iIntros (γc c tid') "Hfin". iMod na_alloc as (tid2) "Htl". wp_let. wp_let. unlock.
iApply (type_call_iris _ [] () [_] _ (Build_thread_id tid2 tid') with "LFT HE Htl [] Hf' [Henv]");
(* The `solve_typing` here shows that, because we assume that `fty` and `retty`
outlive `static`, the implicit requirmeents made by `call_once` are satisifed. *)
......@@ -126,7 +126,7 @@ Section spawn.
(λ r, [r box retty])); try solve_typing; [|].
{ iIntros (tid qmax) "#LFT _ $ $".
rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc".
destruct c' as [[|c'|]|]; try done. iDestruct "Hc" as (??) "Hc".
destruct c' as [[|c'|]|]; try done. iDestruct "Hc" as (?) "Hc".
iApply (join_spec with "Hc"); [solve_ndisj..|]. iNext. iIntros "* Hret".
rewrite tctx_interp_singleton tctx_hasty_val. done. }
iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment