From 3c8a1ed0c8f2e5203db7a61e1c3bae57dfc643b0 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 19 Sep 2018 00:20:00 +0200
Subject: [PATCH] ported spawn

---
 _CoqProject                   |   1 +
 theories/lang/spawn.v         | 121 ++++++++++++++++------------------
 theories/logic/gps_view_inv.v | 101 ++++++++++++++++++++++++++++
 3 files changed, 160 insertions(+), 63 deletions(-)
 create mode 100644 theories/logic/gps_view_inv.v

diff --git a/_CoqProject b/_CoqProject
index be764736..99c06c5d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,6 +16,7 @@ theories/lifetime/at_borrow.v
 theories/lifetime/na_borrow.v
 theories/lifetime/frac_borrow.v
 theories/logic/gps.v
+theories/logic/gps_view_inv.v
 theories/lang/notation.v
 theories/lang/memcpy.v
 theories/lang/new_delete.v
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index d992c232..fa5ca4fd 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import excl.
 From lrust.lang Require Import notation.
 From gpfsl.lang Require Import view_invariants.
 From gpfsl.gps Require Import middleware protocols escrows.
+From lrust.logic Require Import gps_view_inv.
 
 Set Default Proof Using "Type".
 
@@ -58,22 +59,21 @@ Definition spawn_interp γe γi Ψ : interpC Σ unitProtocol :=
 Let IW : loc → gname → time → unitProtocol → val → vProp :=
   (λ _ _ _ _ v, ⌜v = #false⌝)%I.
 
-(* Accessor content for the GPS invariant *)
-Definition spawn_inv γc γe γi c Ψ : vProp :=
-  (GPS_INV (spawn_interp γe γi Ψ) c IW γc)%I.
-
 Definition finish_handle γc γe c Ψ : vProp :=
-  (∃ γi t v, (c >> 1) ↦ v ∗ GPS_SWWriter c t () #0 γc
-    ∗ view_tok γi (1/2)%Qp ∗ view_inv γi N (spawn_inv γc γe γi c Ψ))%I.
+  (∃ γi t v, (c >> 1) ↦ v ∗
+    GPS_vSP_Writer N (spawn_interp γe γi Ψ) IW c t () #0 γc γi ∗
+    view_tok γi (1/2)%Qp)%I.
 
 Definition join_handle γc γe c Ψ : vProp :=
-  (∃ γi (Ψ': val → vProp) t, GPS_SWReader c t () #0 γc
+  (∃ γi (Ψ': val → vProp) t,
+    GPS_vSP_Reader N (spawn_interp γe γi Ψ') IW c t () #0 γc γi
     ∗ ⎡ † c … 2 ∗ tok γe ⎤
-    ∗ view_tok γi (1/2)%Qp ∗ view_inv γi N (spawn_inv γc γe γi c Ψ')
+    ∗ view_tok γi (1/2)%Qp
     ∗ □ (∀ v, Ψ' v -∗ Ψ v))%I.
 
-Global Instance spawn_inv_contractive n γc γe γi c :
-  Proper (pointwise_relation val (dist_later n) ==> dist n) (spawn_inv γc γe γi c).
+Lemma spawn_inv_contractive n γc γe γi c :
+  Proper (pointwise_relation val (dist_later n) ==> dist n)
+         (λ Ψ, GPS_INV (spawn_interp γe γi Ψ) c IW γc).
 Proof.
   move => ???. apply GPS_INV_ne => b ?????. apply bi.exist_ne => b'.
   apply bi.sep_ne; [done|]. destruct b'; [|done].
@@ -82,7 +82,11 @@ 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.
+Proof.
+  move => ???. do 3 (apply bi.exist_ne => ?).
+  apply bi.sep_ne; [done|]. apply bi.sep_ne; [|done].
+  apply bi.sep_ne; [done|]. apply view_inv_ne. by apply spawn_inv_contractive.
+Qed.
 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.
@@ -99,15 +103,13 @@ Proof.
   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 (view_inv_alloc N _) as (γi) "VI".
-  iMod (GPS_SWRaw_Init_vs (spawn_interp γe γi Ψ) _ _ false () with "Hc []")
-    as (γc t) "[SW gpsI]". { iIntros (??). by iExists false. }
-  iDestruct (GPS_SWWriter_Reader with "SW") as "#R". simpl.
-  iMod ("VI" $! (spawn_inv γc γe γi l Ψ) with "[$gpsI]") as "[#Inv [tok1 tok2]]".
-  wp_apply (wp_fork with "[SW tok1 Hf Hd]"); [done|..].
+  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".
+  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 "Inv R ∗". auto.
+    iFrame "R ∗". auto.
 Qed.
 
 Lemma finish_spec Ψ c v γc γe tid
@@ -117,25 +119,18 @@ Lemma finish_spec Ψ c v γc γe tid
   {{{ RET #☠; True }}}.
 Proof.
   iIntros (Φ) "[Hfin HΨ] HΦ".
-  iDestruct "Hfin" as (γi t v0) "(Hd & SW & Hf & #Inv)".
+  iDestruct "Hfin" as (γi t v0) "(Hd & SW & Hf)".
   wp_lam. wp_op. wp_write. wp_bind (_ <-ʳᵉˡ _)%E.
-  iMod (view_inv_acc_base γi N with "[$Inv $Hf]") as "[Hf VI]"; [done|].
-  iDestruct "VI" as (Vb) "[HInv Closed]".
-  iApply (GPS_SWRaw_SWWrite_rel_view (spawn_interp γe γi Ψ) _ IW (λ _, True)%I
-            True%I (spawn_interp γe γi Ψ true c γc t tt #0) (view_tok γi (1 / 2))
-            t () () _ #1  _ _ Vb
-            with "[$SW $HInv $Hf HΨ Hd]"); [done|solve_ndisj|..].
+  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' V') "(_ & _ & In & tok & HInv)".
-  rewrite bi.and_elim_r bi.and_elim_l.
-  iMod ("Closed" $! _ True%I with "tok [HInv]") as "?".
-  { iIntros "tok". by iMod ("HInv" with "tok") as "[$ ?]". }
-  iModIntro. wp_seq. by iApply "HΦ".
+  iIntros "!>" (t') "_". wp_seq. by iApply "HΦ".
 Qed.
 
 Lemma join_spec Ψ c γc γe tid
@@ -143,45 +138,45 @@ Lemma join_spec Ψ c γc γe tid
   {{{ join_handle γc γe c Ψ }}} join [ #c] in tid {{{ v, RET v; Ψ v }}}.
 Proof.
   iIntros (Φ) "H HΦ".
-  iDestruct "H" as (γi Ψ' t) "(R & (H† & He) & Hj & #Inv & #HΨ')".
+  iDestruct "H" as (γi Ψ' t) "(R & (H† & He) & Hj & #HΨ')".
   iLöb as "IH" forall (t). wp_rec. wp_bind (!ᵃᶜ _)%E.
-  iMod (view_inv_acc_base γi N with "[$Inv $Hj]") as "[Hj VI]"; [done|].
-  iDestruct "VI" as (Vb) "[HInv Closed]".
-  iApply (GPS_SWRaw_Read (spawn_interp γe γi Ψ') _ IW
-            (spawn_interp γe γi Ψ' false c γc) _ t () _ _ _ Vb
-            with "[$R $HInv]"); [solve_ndisj|by right|..].
-  { 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]. }
-  iNext. iIntros (t' [] v') "(_ & R & HInv & res)".
-  iDestruct "res" as (b) "[% Es]". subst v'. destruct b; last first.
-  { rewrite bi.and_elim_l.
-    iMod ("Closed" with "Hj HInv") as "Hj".
-    iModIntro. wp_if. iApply ("IH" with "R H† He Hj"). 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Ψ]". iDestruct "SW" as (?) "SW".
-  rewrite bi.and_elim_r bi.and_elim_r.
-  iDestruct ("Closed" with "[$Hj $Hf]") as "[In >_]".
-  iSpecialize ("HInv" with "In").
-  iModIntro. 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".
-  { rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. iFrame. }
-  wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
+  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".
+    { 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.
 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.
 Proof.
-  iIntros "#HΨ Hdl". iDestruct "Hdl" as (γi Ψ' t) "(? & (? & ?) & ? & ? & #HΨ')".
+  iIntros "#HΨ Hdl". iDestruct "Hdl" as (γi Ψ' t) "(? & (? & ?) & ? & #HΨ')".
   iExists γi, Ψ', t. iFrame "#∗". iIntros "!# * ?".
   iApply "HΨ". iApply "HΨ'". done.
 Qed.
diff --git a/theories/logic/gps_view_inv.v b/theories/logic/gps_view_inv.v
new file mode 100644
index 00000000..ffa548f6
--- /dev/null
+++ b/theories/logic/gps_view_inv.v
@@ -0,0 +1,101 @@
+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import notation.
+From gpfsl.lang Require Import view_invariants.
+From gpfsl.gps Require Import middleware.
+
+Section gps_view_SP.
+Context `{!noprolG Σ, !gpsG Σ Prtcl, !view_invG Σ} (N: namespace).
+
+Local Notation vProp := (vProp Σ).
+
+Implicit Types (IP : interpC Σ Prtcl) (IPC: interpCasC Σ Prtcl) (l : loc)
+               (s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
+               (γ : gname).
+
+Definition GPS_vSP_Reader IP IPC l t s v γ γi : vProp :=
+  (GPS_SWReader l t s v γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
+Definition GPS_vSP_Writer IP IPC l t s v γ γi: vProp :=
+  (GPS_SWWriter l t s v γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
+Definition GPS_vSP_SharedReader IP IPC l t s v q γ γi : vProp :=
+  (GPS_SWSharedReader l t s v q γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
+Definition GPS_vSP_SharedWriter IP IPC l t s v γ γi : vProp :=
+  (GPS_SWSharedWriter l t s v γ ∗ view_inv γi N (GPS_INV IP l IPC γ))%I.
+
+Lemma GPS_vSP_SWWriter_Reader IP IPC l t s v γ γi:
+  GPS_vSP_Writer IP IPC l t s v γ γi -∗ GPS_vSP_Reader IP IPC l t s v γ γi.
+Proof.
+  iDestruct 1 as "[W $]". iDestruct (GPS_SWWriter_Reader with "W") as "$".
+Qed.
+
+Lemma GPS_vSP_Init (IP: gname → interpC Σ Prtcl) IPC l s v E:
+  l ↦ v -∗ (∀ γi t γ, ▷ IP γi true l γ t s v) ={E}=∗
+  ∃ γi γ t, view_tok γi 1 ∗ GPS_vSP_Writer (IP γi) IPC l t s v γ γi.
+Proof.
+  iIntros "Hl IP".
+  iMod (view_inv_alloc N _) as (γi) "VI".
+  iMod (GPS_SWRaw_Init_vs (IP γi) _ IPC true s with "Hl IP") as (γ t) "[SW gpsI]".
+  iMod ("VI" $! (GPS_INV (IP γi) l IPC γ) with "gpsI") as "[#Inv tok]".
+  iIntros "!>". iExists γi, γ, t. by iFrame.
+Qed.
+
+Lemma GPS_vSP_SWWrite_rel IP IPC l q Q Q1 Q2 t s s' v v' γ γi tid E
+  (Exts: s ⊑ s') (DISJ: histN ## N) (SUB1: ↑histN ⊆ E) (SUB2: ↑N ⊆ E):
+  let WVS: vProp :=
+  (∀ t', ⌜(t < t')%positive⌝ -∗ GPS_SWWriter l t' s' v' γ -∗ Q2 -∗ view_tok γi q
+              ={E ∖ ↑N}=∗ (<obj> (Q1 ={E ∖ ↑N}=∗ IPC l γ t s v)) ∗
+                     |={E ∖ ↑N}=> (IP true l γ t' s' v' ∗ Q t'))%I in
+  {{{ view_tok γi q ∗ GPS_vSP_Writer IP IPC l t s v γ γi
+      ∗ ▷ WVS ∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ Q1 ∗ Q2) }}}
+    #l <-ʳᵉˡ v' in tid @ E
+  {{{ t', RET #☠; ⌜(t < t')%positive⌝ ∗ GPS_vSP_Reader IP IPC l t' s' v' γ γi
+      ∗ Q t' }}}.
+Proof.
+  iIntros (WVS Φ) "(Htok & [W #Inv] & WVS & IP) Post".
+  iMod (view_inv_acc_base γi N with "[$Inv $Htok]") as "[Htok VI]"; [done|].
+  iDestruct "VI" as (Vb) "[HInv Closed]".
+  iApply (GPS_SWRaw_SWWrite_rel_view IP _ IPC Q Q1 Q2 (view_tok γi q)%I t s s'
+           v v' γ tid Vb with "[$W $HInv $Htok $WVS $IP]"); [done|solve_ndisj|..].
+  iIntros "!>" (t' V') "(Ext & R & In & tok & HInv)".
+  rewrite bi.and_elim_r bi.and_elim_l.
+  iMod ("Closed" $! _ (Q t') with "tok HInv") as "Q".
+  by iApply ("Post" $! t' with "[$Ext $R $Q $Inv]").
+Qed.
+
+Lemma GPS_vSP_SWRead_acq_dealloc IP IPC l P Q R q t s v vd γ γi tid E
+  (DISJ: histN ## N) (SUB1: ↑histN ⊆ E) (SUB2: ↑N ⊆ E):
+  let RVS: vProp :=
+    (∀ t' s' v', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗
+         <obj> ((IP false l γ t' s' v' ={E ∖ ↑N}=∗ IP false l γ t' s' v' ∗ R t' s' v') ∧
+                (IP true l γ t' s' v' ={E ∖ ↑N}=∗ IP true l γ t' s' v' ∗ R t' s' v') ∧
+                (IPC l γ t' s' v' ={E ∖ ↑N}=∗ IPC l γ t' s' v' ∗ R t' s' v')))%I in
+  let DVS: vProp :=
+    (∀ t' s', ⌜s ⊑ s' ∧ t ⊑ t'⌝ -∗ P -∗ view_tok γi q -∗ R t' s' vd ={E ∖ ↑N}=∗
+      view_tok γi 1 ∗ Q t' s')%I in
+  {{{ view_tok γi q ∗ GPS_vSP_Reader IP IPC l t s v γ γi
+      ∗ ▷ RVS ∗ ▷ DVS ∗ P }}}
+    !ᵃᶜ#l in tid @ E
+  {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝ ∗
+      GPS_vSP_Reader IP IPC l t' s' v' γ γi ∗
+      if (decide (v' = vd)) then ▷ GPS_INV IP l IPC γ ∗ Q t' s'
+      else view_tok γi q ∗ R t' s' v' ∗ P }}}.
+Proof.
+  iIntros (RVS DVS Φ) "(Htok & [R #Inv] & RVS & DVS & P) Post".
+  iMod (view_inv_acc_base γi N with "[$Inv $Htok]") as "[Htok VI]"; [done|].
+  iDestruct "VI" as (Vb) "[HInv Closed]".
+  iApply (GPS_SWRaw_Read IP _ IPC R _ t s v _ _ Vb with "[$R $HInv $RVS]");
+    [solve_ndisj|by right|..].
+  iIntros "!>" (t' s' v') "(#Ext & R & HInv & HR)".
+  case (decide (v' = vd)) as [Eq|NEq]; last first.
+  - rewrite bi.and_elim_l. iMod ("Closed" with "Htok HInv") as "Htok".
+    iIntros "!>". iApply ("Post" with "[$Ext $R $Inv HR Htok P]").
+    rewrite (decide_False _ _ NEq). by iFrame.
+  - subst v'. iMod ("DVS" $! t' s' with "Ext P Htok HR") as "[Htok Q]".
+    rewrite bi.and_elim_r bi.and_elim_r.
+    iDestruct ("Closed" with "Htok") as "[In >_]".
+    iSpecialize ("HInv" with "In"). iModIntro.
+    iApply ("Post" $! t' s' vd with "[$Ext $R $Inv HInv Q]").
+    rewrite decide_True; [by iFrame|done].
+Qed.
+
+End gps_view_SP.
-- 
GitLab