From f949325c9680bad9efa18d66ebfdaec35eca2342 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 27 Apr 2017 15:30:16 +0200
Subject: [PATCH] make join_handle Send/Sync
---
theories/lang/lib/spawn.v | 16 +++++++++++++---
theories/typing/lib/spawn.v | 38 ++++++++++++++++++++++++-------------
2 files changed, 38 insertions(+), 16 deletions(-)
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 17d92893..2716c48b 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -47,7 +47,8 @@ Definition finish_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(∃ γf γj v, own γf (Excl ()) ∗ shift_loc c 1 ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
Definition join_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
- (∃ γf γj, own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ))%I.
+ (∃ γf γj Ψ', own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ') ∗
+ □ (∀ v, Ψ' v -∗ Ψ v))%I.
Global Instance spawn_inv_ne n γf γj c :
Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γf γj c).
@@ -96,7 +97,7 @@ Qed.
Lemma join_spec (Ψ : val → iProp Σ) c :
{{{ join_handle c Ψ }}} join [ #c] {{{ v, RET v; Ψ v }}}.
Proof.
- iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj) "(Hj & H† & #?)".
+ iIntros (Φ) "H HΦ". iDestruct "H" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
iLöb as "IH". wp_rec.
wp_bind (!ˢᶜ _)%E. iInv N as "[[_ >Hj']|Hinv]" "Hclose".
{ iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
@@ -112,8 +113,17 @@ Proof.
iModIntro. iApply wp_if. iNext. wp_op. wp_read. wp_let.
iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
- wp_free; first done. iApply "HΦ". done.
+ wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
Qed.
+
+Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
+ □ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
+Proof.
+ iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
+ iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?".
+ iApply "HΨ". iApply "HΨ'". done.
+Qed.
+
End proof.
Typeclasses Opaque finish_handle join_handle.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index aa8eb563..3180013e 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -17,8 +17,7 @@ Section join_handle.
{| ty_size := 1;
ty_own tid vl :=
match vl return _ with
- | [ #(LitLoc l) ] =>
- ∃ ty', ▷ type_incl ty' ty ∗ join_handle spawnN l (join_inv tid ty')
+ | [ #(LitLoc l) ] =>join_handle spawnN l (join_inv tid ty)
| _ => False
end%I;
ty_shr κ tid l := True%I |}.
@@ -34,8 +33,9 @@ Section join_handle.
Proof.
iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
- iDestruct "Hvl" as (ty) "[Hincl' ?]". iExists ty. iFrame.
- iApply (type_incl_trans with "Hincl'"). done.
+ simpl. iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hown".
+ iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
+ iApply "Hincl". done.
- iIntros "* _". auto.
Qed.
@@ -57,8 +57,22 @@ Section join_handle.
Global Instance join_handle_ne : NonExpansive join_handle.
Proof. apply type_contractive_ne, _. Qed.
- (* TODO: Looks like in Rust, we have T: Send -> JoinHandle<T>: Send and
- T:Sync -> JoinHandle<T>: Sync. *)
+ Global Instance join_handle_send ty :
+ Send ty → Send (join_handle ty).
+ Proof.
+ iIntros (??? vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+ simpl. iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hv".
+ unfold join_inv. iApply own_send. (* FIXME: Why does "iApply send_change_tid" not work? *)
+ done.
+ Qed.
+
+ Global Instance join_handle_sync ty :
+ Sync (join_handle ty).
+ Proof.
+ iIntros (????) "**". (* FIXME: Why did it throw away the assumption we should have gotten? *)
+ done.
+ Qed.
+
End join_handle.
Section spawn.
@@ -88,7 +102,7 @@ Section spawn.
iApply (spawn_spec _ (join_inv tid retty) with "[-]");
first solve_to_val; last first; last simpl_subst.
{ iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
- iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
+ iIntros "?". by iFrame. }
iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
(* FIXME this is horrible. *)
refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
@@ -129,12 +143,10 @@ Section spawn.
iApply (type_let _ _ _ _ ([c' ◁ _])
(λ r, [r ◁ box retty])); try solve_typing; [|].
{ iIntros (tid) "#LFT _ $ $".
- rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
- destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
- iApply (join_spec with "Hc'"). iNext. iIntros "* Hret".
- rewrite tctx_interp_singleton tctx_hasty_val.
- iDestruct (box_type_incl with "[$Hsub]") as "(_ & Hincl & _)".
- iApply "Hincl". done. }
+ rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc".
+ destruct c' as [[|c'|]|]; try done.
+ iApply (join_spec with "Hc"). iNext. iIntros "* Hret".
+ rewrite tctx_interp_singleton tctx_hasty_val. done. }
iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
--
GitLab