spec for spawn

_CoqProject

@@ -20,6 +20,7 @@ theories/lang/memcpy.v
 theories/lang/new_delete.v
 theories/lang/swap.v
 theories/lang/lock.v
+theories/lang/spawn.v
 theories/typing/base.v
 theories/typing/lft_contexts.v
 theories/typing/type.v

opam

@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2018-05-25.1.99748e8d") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-05-26.1.02e09a65") | (= "dev") }
 ]

theories/lang/lock.v

-From iris.program_logic Require Import weakestpre.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import notation.
@@ -31,7 +30,7 @@ Section proof.
   Local Notation vProp := (vProp Σ).
 
   Definition lock_interp (R : vProp) : interpC Σ unitProtocol :=
-    (λ pb _ _ v, ∃ b : bool, ⌜v = #b⌝ ∗
+    (λ pb _ _ _ v, ∃ b : bool, ⌜v = #b⌝ ∗
                  if pb then (if b then True else R) else True)%I.
 
   Definition lock_proto_inv l γ (R0 : vProp): vProp :=
@@ -64,17 +63,17 @@ Section proof.
     iAlways; iSplit; iIntros; by iApply "HR".
   Qed.
 
-  Lemma lock_interp_comparable l s v R:
-    lock_interp R false l s v
+  Lemma lock_interp_comparable l γ s v R:
+    lock_interp R false l γ s v
     -∗ ⌜∃ vl : lit, v = #vl ∧ lit_comparable (Z_of_bool false) vl⌝.
   Proof.
     iDestruct 1 as (b) "[% _]". subst v. iExists b. iPureIntro.
     split; [done|by constructor].
   Qed.
 
-  Lemma lock_interp_duplicable l s v R:
-    lock_interp R false l s v
-    -∗ lock_interp R false l s v ∗ lock_interp R false l s v.
+  Lemma lock_interp_duplicable l γ s v R:
+    lock_interp R false l γ s v
+    -∗ lock_interp R false l γ s v ∗ lock_interp R false l γ s v.
   Proof. by iIntros "#$". Qed.
 
   (** The main proofs. *)
@@ -83,10 +82,10 @@ Section proof.
       ∃ γ, lock_proto_lc l γ R R ∗ ▷?bl lock_proto_inv l γ R.
   Proof.
     iIntros "Hl R".
-    iMod (GPS_PPRaw_Init_vs (lock_interp R) _ bl _ () with "Hl [R] []")
+    iMod (GPS_PPRaw_Init_vs (lock_interp R) _ bl _ () with "Hl [R]")
       as (γ) "[lc inv]".
-    { rewrite /lock_interp. iExists b. iSplit; [done|]. by destruct b. }
-    { rewrite /lock_interp. by iExists b. }
+    { iIntros (?). rewrite /lock_interp. iSplitL "R"; iExists b; [|done].
+      iSplit; [done|by destruct b]. }
     iExists γ. iFrame "lc inv". iIntros "!> !#". by iApply (bi.iff_refl True%I).
   Qed.
 

theories/lang/spawn.v

-From iris.program_logic Require Import weakestpre.
+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.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.
+  split=> Vx. iIntros "H". iExists (V ⊔ Vx). iApply "H". iPureIntro. solve_lat.
+Qed.
+
 Set Default Proof Using "Type".
 
 Definition spawn : val :=
@@ -39,7 +47,7 @@ Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!noprolG Σ, !spawnG Σ}.
+Context `{!noprolG Σ, !spawnG Σ} (N : namespace).
 Local Notation vProp := (vProp Σ).
 Local Notation tok γ := (own γ (Excl ())).
 Implicit Types (c: loc) (Ψ : val → vProp) (v: val).
@@ -47,95 +55,143 @@ Implicit Types (c: loc) (Ψ : val → vProp) (v: val).
 Definition finishEscrow γc γe γf c Ψ :=
   ([es ⎡ tok γe ⎤ ⇝ (GPS_SWRawWriter c () γc ∗ ⎡ tok γf ⎤ ∗ ∃ v, (c >> 1) ↦ v ∗ Ψ v)])%I.
 
-Definition spawn_interp γc γe γf Ψ : interpC Σ unitProtocol :=
-  (λ pb c _ v, ∃ b : bool, ⌜v = #b⌝ ∗
-               if pb then (if b then finishEscrow γc γe γf c Ψ else True) else True)%I.
+(* GPS protocol interpretation *)
+Definition spawn_interp γe γf Ψ : interpC Σ unitProtocol :=
+  (λ pb c γc _ v, ∃ b : bool, ⌜v = #b⌝ ∗
+               if pb then True else (if b then finishEscrow γc γe γf c Ψ else True))%I.
 
+(* Accessor content for the GPS invariant *)
 Definition spawn_inv γc γe γf γj c Ψ :=
-  (tok γf ∗ tok γj ∨ ∃ V, GPS_INV (spawn_interp γc γe γf Ψ) c γc V)%I.
+  (tok γf ∗ tok γj ∨ (∃ V, GPS_INV (spawn_interp γe γf Ψ) c γc V))%I.
 
-Definition finish_handle γc γe c Ψ N :=
+Definition finish_handle γc γe c Ψ : vProp :=
   (∃ γf γj v, (c >> 1) ↦ v ∗ GPS_SWRawWriter c () γc
-    ∗ ⎡ own γf (Excl ()) ∗ invariants.inv N (spawn_inv γc γe γf γj c Ψ)⎤ )%I.
+    ∗ ⎡ tok γf ∗ inv N (spawn_inv γc γe γf γj c Ψ)⎤ )%I.
 
-Definition join_handle γc γe c Ψ N : vProp :=
+Definition join_handle γc γe c Ψ : vProp :=
   (∃ γf γj (Ψ': val → vProp), GPS_SWRawReader c () γc
-    ∗ ⎡ † c … 2 ∗ own γj (Excl ()) ∗ invariants.inv N (spawn_inv γc γe γf γj c Ψ')⎤
+    ∗ ⎡ † c … 2 ∗ tok γj ∗ tok γe ∗ inv N (spawn_inv γc γe γ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).
+Global Instance spawn_inv_constractive n γc γe γf γj c :
+  Proper (pointwise_relation val (dist_later n) ==> dist n) (spawn_inv γc γe γf γj c).
+Proof.
+  move => ???. apply bi.or_ne; [done|].
+  apply bi.exist_ne => ?. apply GPS_INV_ne.
+  move => b ????. apply bi.exist_ne => b'.
+  apply bi.sep_ne; [done|]. destruct b; [done|]. destruct b'; [|done].
+  solve_contractive.
+Qed.
+
+Global Instance finish_handle_contractive n γc γe c :
+  Proper (pointwise_relation val (dist_later n) ==> dist n) (finish_handle γc γe c).
 Proof. solve_proper. Qed.
-Global Instance finish_handle_ne n c :
-  Proper (pointwise_relation val (dist n) ==> dist n) (finish_handle c).
+Global Instance join_handle_ne n γc γe c :
+  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle γc γe c).
 Proof. solve_proper. Qed.
-Global Instance join_handle_ne n c :
-  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle c).
-Proof. solve_proper. Qed. *)
+
+Lemma spawn_interp_dup γc γe γf c Ψ s v:
+  spawn_interp γe γf Ψ false c γc s v -∗
+  spawn_interp γe γf Ψ false c γc s v ∗ spawn_interp γe γf Ψ false c γc s v.
+Proof.
+  iDestruct 1 as (b) "[#Eq E]". destruct b; iDestruct "E" as "#E";
+  iSplitL""; iExists _; by iFrame "Eq".
+Qed.
 
 (** The main proofs. *)
-Lemma spawn_spec Ψ e (f : val) N tid :
+Lemma spawn_spec Ψ e (f : val) tid :
   to_val e = Some f →
-  {{{ ∀ γc γe c tid',
-        finish_handle γc γe c Ψ N -∗ WP f [ #c] in tid' {{ _, True }} }}}
+  {{{ ∀ γc γe c tid', finish_handle γc γe c Ψ -∗ WP f [ #c] in tid' {{ _, True }} }}}
     spawn [e] in tid
-  {{{ γc γe c, RET #c; join_handle γc γe c Ψ N }}}.
+  {{{ γc γe c, RET #c; join_handle γc γe c Ψ }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=.
   wp_let. wp_alloc l as "Hl" "H†". wp_let.
   iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
   iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
+  iMod (own_alloc (Excl ())) as (γe) "Hγe"; first done.
   rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
   iDestruct "Hl" as "[Hc Hd]". wp_write.
-  iMod (GPS_SWRaw_Init_vs (spawn_interp γc γe γf Ψ)).
-  iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
-  { iNext. iRight. iExists false. auto. }
-  wp_apply (wp_fork with "[Hγf Hf Hd]").
-  - iApply "Hf". iExists _, _, _. iFrame. auto.
-  - iIntros "_". wp_seq. iApply "HΦ". iExists _, _.
-    iFrame. auto.
+  iMod (GPS_SWRaw_Init_vs (spawn_interp γe γf Ψ) _ false _ () with "Hc []")
+    as (γc) "[SW gpsI]".
+  { iIntros (?). rewrite /spawn_interp /=. by iSplit; iExists false. }
+  iDestruct (GPS_SWRawWriter_RawReader with "SW") as "#R". simpl.
+  iMod (inv_alloc N _ (spawn_inv γc γe γf γj l Ψ) with "[gpsI]") as "#Inv".
+  { iNext. iRight. iDestruct (monPred_in_intro with "gpsI") as (V) "[_ gpsI]".
+    by iExists V. }
+  wp_apply (wp_fork with "[SW Hγf Hf Hd]"); [done|..].
+  - iNext. iIntros (tid'). iApply "Hf". iExists _, _, _. by iFrame.
+  - iIntros "_". wp_seq. iApply ("HΦ" $! γc γe). iExists _, _, _.
+    iFrame "Inv R ∗". auto.
 Qed.
 
-Lemma finish_spec (Ψ : val → iProp Σ) c v :
-  {{{ finish_handle c Ψ ∗ Ψ v }}} finish [ #c; v] {{{ RET #☠; True }}}.
+Lemma finish_spec Ψ c v γc γe tid
+  (DISJ1: (↑histN) ## (↑N : coPset)) (DISJ2: (↑escrowN) ## (↑N : coPset)) :
+  {{{ finish_handle γc γe c Ψ ∗ Ψ v }}}
+    finish [ #c; v] in tid
+  {{{ RET #☠; True }}}.
 Proof.
-  iIntros (Φ) "[Hfin HΨ] HΦ". iDestruct "Hfin" as (γf γj v0) "(Hf & Hd & #?)".
-  wp_lam. wp_op. wp_write.
-  wp_bind (_ <-ˢᶜ _)%E. iInv N as "[[>Hf' _]|Hinv]" "Hclose".
+  iIntros (Φ) "[Hfin HΨ] HΦ".
+  iDestruct "Hfin" as (γf γj v0) "(Hd & SW & Hf & #Inv)".
+  wp_lam. wp_op. wp_write. wp_bind (_ <-ʳᵉˡ _)%E.
+  iMod (inv_open _ N with "Inv") as "[[[>Hf' _]|Hinv] Hclose]"; [done|..].
   { iExFalso. iCombine "Hf" "Hf'" as "Hf". iDestruct (own_valid with "Hf") as "%".
     auto. }
-  iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
+  iDestruct "Hinv" as (Vb) "HInv".
+  iApply (GPS_SWRawWriter_rel_write (spawn_interp γe γf Ψ) _ True%I #1 () () _ _ Vb
+            with "[$SW HInv Hf HΨ Hd]"); [done|solve_ndisj|..].
+  { iSplitL "HInv".
+    - iIntros "mb". iNext. by iApply (monPred_in_elim with "mb HInv").
+    - iNext. iIntros "_ SW". iSplitL ""; [done|].
+      iSplitL ""; iExists true; [done|]. iSplitL ""; [done|].
+      iApply escrow_alloc; [solve_ndisj|]. iFrame. iExists _. by iFrame. }
+  iNext. iIntros "(_ & HInv & _)".
   iMod ("Hclose" with "[-HΦ]").
-  - iNext. iRight. iExists true. iFrame. iExists _. iFrame.
+  - iRight. iDestruct (monPred_in_elim_vProp with "HInv") as (V') "HInv".
+    iExists V'. rewrite monPred_at_later. by iFrame "HInv".
   - iModIntro. wp_seq. by iApply "HΦ".
 Qed.
 
-Lemma join_spec (Ψ : val → iProp Σ) c :
-  {{{ join_handle c Ψ }}} join [ #c] {{{ v, RET v; Ψ v }}}.
+Lemma join_spec Ψ c γc γe tid
+  (DISJ1: (↑histN) ## (↑N : coPset)) (DISJ2: (↑escrowN) ## (↑N : coPset)) :
+  {{{ join_handle γc γe c Ψ }}} join [ #c] in tid {{{ v, RET v; Ψ v }}}.
 Proof.
-  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".
+  iIntros (Φ) "H HΦ".
+  iDestruct "H" as (γf γj Ψ') "(R & (H† & Hj & He & #Inv) & #HΨ')".
+  iLöb as "IH". wp_rec. wp_bind (!ᵃᶜ _)%E.
+  iMod (inv_open _ N with "Inv") as "[[[_ >Hj']|Hinv] Hclose]"; [done|..].
   { iExFalso. iCombine "Hj" "Hj'" as "Hj". iDestruct (own_valid with "Hj") as "%".
     auto. }
-  iDestruct "Hinv" as (b) "[>Hc Ho]". wp_read. destruct b; last first.
-  { iMod ("Hclose" with "[Hc]").
-    - iNext. iRight. iExists _. iFrame.
-    - iModIntro. wp_if. iApply ("IH" with "Hj H†"). auto. }
-  iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
-  iMod ("Hclose" with "[Hj Hf]") as "_".
-  { iNext. iLeft. iFrame. }
+  iDestruct "Hinv" as (Vb) "HInv".
+  iApply (GPS_SWRawReader_read (spawn_interp γe γf Ψ') _ _ () _ _ Vb
+            with "[$R HInv]"); [solve_ndisj|by right|..].
+  { iSplitL "HInv".
+    - iIntros "mb". iNext. by iApply (monPred_in_elim with "mb HInv").
+    - iNext. iIntros (? _). iLeft. iIntros "!>" (?). by iApply spawn_interp_dup. }
+  iNext. iIntros ([] v) "(_ & R & HInv & res)".
+  iDestruct "res" as (b) "[% Es]". subst v. destruct b; last first.
+  { iMod ("Hclose" with "[HInv]").
+    - iRight. iDestruct (monPred_in_elim_vProp with "HInv") as (V') "HInv".
+      iExists V'. rewrite monPred_at_later. by iFrame "HInv".
+    - iModIntro. wp_if. iApply ("IH" with "R H† Hj He"). auto. }
+  iMod (escrow_elim with "[] Es [$He]") as "(SW & Hf & Ho)"; [solve_ndisj|..].
+  { iIntros "[He1 He2]". iCombine "He1" "He2" as "He".
+     iDestruct (own_valid with "He") as "%". auto. }
+  iDestruct "Ho" as (v) "[Hd HΨ]".
+  iMod ("Hclose" with "[Hj Hf]") as "_". { iNext. iLeft. iFrame. }
   iModIntro. wp_if. 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. }
+  iApply (wp_hist_inv); [done|]. iIntros "Hist".
+  iMod (GPS_SWRawWriter_dealloc _ _ true with "Hist HInv SW") as (v') "[Hc _]";
+    [done|].
+  iAssert (c ↦∗ [ v'; v])%I with "[Hc Hd]" as "Hc".
+  { rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iFrame. }
   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.
+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.
 Proof.
-  iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H† & #? & #HΨ')".
+  iIntros "#HΨ Hdl". iDestruct "Hdl" as (γf γj Ψ') "(? & (? & ? & ? & ?) & #HΨ')".
   iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?".
   iApply "HΨ". iApply "HΨ'". done.
 Qed.