complete spawn/join

_CoqProject

@@ -51,6 +51,8 @@ theories/typing/lib/option.v
 theories/typing/lib/panic.v
 theories/typing/lib/swap.v
 theories/typing/lib/take_mut.v
+theories/typing/lib/spawn.v
+theories/typing/lib/join.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
 theories/typing/lib/mutex/mutex.v

theories/lang/spawn.v

@@ -4,8 +4,6 @@ From iris.algebra Require Import excl.
 From lrust.lang Require Import notation.
 From gpfsl.gps Require Import middleware protocols escrows.
 
-From iris.bi Require Import bi.
-
 Lemma monPred_in_elim_vProp `{Σ: gFunctors}  (P : vProp Σ) (V : view):
   (monPred_in V → P) -∗ ⎡ ∃ V', P V' ⎤.
 Proof.

theories/typing/lib/join.v

+From iris.proofmode Require Import tactics.
+From iris.bi Require Import big_op.
+From lrust.lang Require Import spawn.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Definition joinN := lrustN .@ "join".
+
+Section join.
+  Context `{!typeG Σ, !spawnG Σ}.
+
+  (* This model is very far from rayon::join, which uses a persistent
+     work-stealing thread-pool.  Still, the important bits are right:
+     One of the closures is executed in another thread, and the
+     closures can refer to on-stack data (no 'static' bound). *)
+  Definition join (call_once_A call_once_B : val) (R_A R_B : type) : val :=
+    funrec: <> ["fA"; "fB"] :=
+      let: "call_once_A" := call_once_A in
+      let: "call_once_B" := call_once_B in
+      let: "join" := spawn [λ: ["c"],
+                            letcall: "r" := "call_once_A" ["fA"]%E in
+                            finish ["c"; "r"]] in
+      letcall: "retB" := "call_once_B" ["fB"]%E in
+      let: "retA" := join ["join"] in
+      (* Put the results in a pair. *)
+      let: "ret" := new [ #(R_A.(ty_size) + R_B.(ty_size)) ] in
+      "ret" +ₗ #0 <-{R_A.(ty_size)} !"retA";;
+      "ret" +ₗ #R_A.(ty_size) <-{R_B.(ty_size)} !"retB";;
+      delete [ #R_A.(ty_size); "retA"] ;; delete [ #R_B.(ty_size); "retB"] ;;
+      return: ["ret"].
+
+  Lemma join_type A B R_A R_B call_once_A call_once_B
+        `{!TyWf A, !TyWf B, !TyWf R_A, !TyWf R_B}
+        `(!Send A, !Send B, !Send R_A, !Send R_B) :
+    (* A : FnOnce() -> R_A, as witnessed by the impl call_once_A *)
+    typed_val call_once_A (fn(∅; A) → R_A) →
+    (* B : FnOnce() -> R_B, as witnessed by the impl call_once_B *)
+    typed_val call_once_B (fn(∅; B) → R_B) →
+    typed_val (join call_once_A call_once_B R_A R_B) (fn(∅; A, B) → Π[R_A; R_B]).
+  Proof using Type*.
+    intros HfA HfB E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>envA envB. simpl_subst.
+    iApply type_let; [apply HfA|solve_typing|]. iIntros (fA); simpl_subst.
+    iApply type_let; [apply HfB|solve_typing|]. iIntros (fB); simpl_subst.
+    (* Drop to Iris. *)
+    iIntros (tid) "#LFT #HE Hna HL Hk (HfB & HfA & HenvA & HenvB & _)".
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ1) "(Hϝ1 & HL & Hclose1)";
+      [solve_typing..|].
+    (* FIXME: using wp_apply here breaks calling solve_to_val. *)
+    wp_bind (spawn _).
+    iApply ((spawn_spec joinN (λ v, (box R_A).(ty_own) tid [v] ∗ (qϝ1).[ϝ])%I) with "[HfA HenvA Hϝ1]");
+      first solve_to_val; first simpl_subst.
+    { (* The new thread. *)
+      iIntros (γc γe 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.
+      - by rewrite /= (right_id static).
+      - by rewrite bi.big_sepL_singleton tctx_hasty_val send_change_tid.
+      - 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.
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ2) "(Hϝ2 & HL & Hclose2)";
+      [solve_typing..|].
+    rewrite !tctx_hasty_val.
+    iApply (type_call_iris _ [ϝ] () [_] with "LFT HE Hna [Hϝ2] HfB [HenvB]").
+    { rewrite outlives_product. solve_typing. }
+    { by rewrite /= (right_id static). }
+    { by rewrite bi.big_sepL_singleton tctx_hasty_val. }
+    (* The return continuation after calling fB in the main thread. *)
+    iIntros (retB) "Hna Hϝ2 HretB". rewrite /= (right_id static).
+    iMod ("Hclose2" with "Hϝ2 HL") as "HL". wp_rec.
+    wp_apply (join_spec with "Hjoin"); [solve_ndisj..|]. iIntros (retA) "[HretA Hϝ1]".
+    iMod ("Hclose1" with "Hϝ1 HL") as "HL". wp_let.
+    (* Switch back to type system mode. *)
+    iApply (type_type _ _ _ [ retA ◁ box R_A; retB ◁ box R_B ]
+        with "[] LFT HE Hna HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
+    iApply (type_new_subtype (Π[uninit R_A.(ty_size); uninit R_B.(ty_size)]));
+      (* FIXME: solve_typing should handle this without any aid. *)
+      rewrite ?Z_nat_add; [solve_typing..|].
+    iIntros (r); simpl_subst.
+    iApply (type_memcpy R_A); [solve_typing..|].
+    iApply (type_memcpy R_B); [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+End join.

theories/typing/lib/spawn.v

+From iris.proofmode Require Import tactics.
+From iris.bi Require Import big_op.
+From lrust.lang Require Import spawn.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Definition spawnN := lrustN .@ "spawn".
+
+Section join_handle.
+  Context `{!typeG Σ, !spawnG Σ}.
+
+  Definition join_inv tid (ty : type) (v : val) :=
+    (box ty).(ty_own) tid [v].
+
+  Program Definition join_handle (ty : type) :=
+    {| ty_size := 1;
+       ty_own tid vl :=
+         match vl return _ with
+         | [ #(LitLoc l) ] => ∃ γc γe, join_handle spawnN γc γe l (join_inv tid ty)
+         | _ => False
+         end%I;
+       ty_shr κ tid l := True%I |}.
+  Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
+  Next Obligation. iIntros "* _ _ _ $". auto. Qed.
+  Next Obligation. iIntros (?) "**"; auto. Qed.
+
+  Global Instance join_handle_wf ty `{!TyWf ty} : TyWf (join_handle ty) :=
+    { ty_lfts := ty.(ty_lfts); ty_wf_E := ty.(ty_wf_E) }.
+
+  Lemma join_handle_subtype ty1 ty2 :
+    ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
+  Proof.
+    iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
+    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+      simpl. iDestruct "Hvl" as (γc γe) "Hvl". iExists γc, γe.
+      iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hown".
+      iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
+      iApply "Hincl". done.
+    - iIntros "* _". auto.
+  Qed.
+
+  Global Instance join_handle_mono E L :
+    Proper (subtype E L ==> subtype E L) join_handle.
+  Proof.
+    iIntros (ty1 ty2 Hsub ?) "HL". iDestruct (Hsub with "HL") as "#Hsub".
+    iIntros "!# #HE". iApply join_handle_subtype. iApply "Hsub"; done.
+  Qed.
+  Global Instance join_handle_proper E L :
+    Proper (eqtype E L ==> eqtype E L) join_handle.
+  Proof. intros ??[]. by split; apply join_handle_mono. Qed.
+
+  Global Instance join_handle_type_contractive : TypeContractive join_handle.
+  Proof.
+    constructor;
+      solve_proper_core ltac:(fun _ => exact: type_dist2_dist || f_type_equiv || f_contractive || f_equiv).
+  Qed.
+  Global Instance join_handle_ne : NonExpansive join_handle.
+  Proof. apply type_contractive_ne, _. Qed.
+
+  Global Instance join_handle_send ty :
+    Send ty → Send (join_handle ty).
+  Proof.
+    iIntros (??? vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+    simpl. iDestruct "Hvl" as (γc γe) "Hvl". iExists γc, γe.
+    iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hv".
+    unfold join_inv. iApply @send_change_tid. done.
+  Qed.
+
+  Global Instance join_handle_sync ty : Sync (join_handle ty).
+  Proof. iIntros (????) "_ //". Qed.
+End join_handle.
+
+Section spawn.
+  Context `{!typeG Σ, !spawnG Σ}.
+
+  Definition spawn (call_once : val) : val :=
+    funrec: <> ["f"] :=
+      let: "call_once" := call_once in
+      let: "join" := spawn [λ: ["c"],
+                            letcall: "r" := "call_once" ["f":expr] in
+                            finish ["c"; "r"]] in
+      letalloc: "r" <- "join" in
+      return: ["r"].
+
+  Lemma spawn_type fty retty call_once `{!TyWf fty, !TyWf retty}
+        `(!Send fty, !Send retty) :
+    typed_val call_once (fn(∅; fty) → retty) → (* fty : FnOnce() -> retty, as witnessed by the impl call_once *)
+    let E ϝ := fty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
+    typed_val (spawn call_once) (fn(E; fty) → join_handle retty).
+  Proof.
+    intros Hf ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>env. simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]. iIntros (f'). simpl_subst.
+    iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _])
+                     (λ j, [j ◁ join_handle retty])); try solve_typing; [|].
+    { (* The core of the proof: showing that spawn is safe. *)
+      iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]". rewrite !tctx_hasty_val [fn _]lock.
+      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 _,_. by iFrame. }
+      iIntros (γc γe 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. *)
+        [solve_typing|iApply (lft_tok_static 1%Qp)| |].
+      - by rewrite bi.big_sepL_singleton tctx_hasty_val send_change_tid.
+      - iIntros (r) "Htl _ Hret".
+        wp_rec. iApply (finish_spec with "[$Hfin Hret]"); [solve_ndisj..| |auto].
+        by iApply @send_change_tid. }
+    iIntros (v). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply type_jump; solve_typing.
+  Qed.
+
+  Definition join : val :=
+    funrec: <> ["c"] :=
+      let: "c'" := !"c" in
+      let: "r" := join ["c'"] in
+      delete [ #1; "c"];; return: ["r"].
+
+  Lemma join_type retty `{!TyWf retty} :
+    typed_val join (fn(∅; join_handle retty) → retty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>c. simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (c'); simpl_subst.
+    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 (??) "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..|].
+    iApply type_jump; solve_typing.
+  Qed.
+End spawn.