WIP: mortal SW protocols

theories/lifetime/gps.v

@@ -3,7 +3,26 @@ From lrust.lang Require Import notation.
 From lrust.lifetime Require Import at_borrow.
 From gpfsl.gps Require Import middleware.
 
-Section gps_at_bor.
+Section gps_at_bor_SW.
+Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG view_Lat (↑histN) Σ} (N: namespace).
+Local Notation vProp := (vProp Σ).
+
+Implicit Types (IP : interpC Σ Prtcl) (l : loc)
+               (s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
+               (κ : lft) (γ : gname).
+
+Definition GPS_aSP_Reader IP IPC l κ t s v γ : vProp :=
+  (GPS_SWReader l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
+Definition GPS_aSP_Writer IP IPC l κ t s v γ : vProp :=
+  (GPS_SWWriter l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
+Definition GPS_aSP_SharedReader IP IPC l κ t s v q γ : vProp :=
+  (GPS_SWSharedReader l t s v q γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
+Definition GPS_aSP_SharedWriter IP IPC l κ t s v γ : vProp :=
+  (GPS_SWSharedWriter l t s v γ ∗ &at{κ, N} (GPS_INV IP l IPC γ))%I.
+
+End gps_at_bor_SW.
+
+Section gps_at_bor_PP.
 Context `{!noprolG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG view_Lat (↑histN) Σ}
         (N: namespace).
 Local Notation vProp := (vProp Σ).
@@ -45,6 +64,29 @@ Proof.
   iFrame "Htok". iExists γ, t, v. by iFrame "PP Hl".
 Qed.
 
+
+Lemma GPS_PP_Read IP l κ q R (o: memOrder) t s v γ tid E
+  (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E):
+  o = Relaxed ∨ o = AcqRel →
+  {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_PP IP l κ t s v γ
+      ∗ (▷ ∀ 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'))) }}}
+    Read o #l in tid @ E
+  {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝ ∗ GPS_PP IP l κ t' s' v' γ ∗ (q).[κ]
+      ∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
+Proof.
+  iIntros (RLX Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
+  iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
+  iApply (GPS_PPRaw_Local_Read IP l R o t s v γ tid Vb
+          with "[$Hlc $Hproto $VS]"); [solve_ndisj|done|..].
+  iNext. iIntros (t' s' v') "(Ext & Hlc' & Hproto & R)".
+  iMod ("Hclose1" with "Hproto") as "Htok".
+  iApply ("Post" $! t' s' v' with "[$Ext $Hlc' $Hshr $Htok $R]").
+Qed.
+
 Lemma GPS_PP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
   (FIN: model.final_st s')
   (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E):
@@ -114,4 +156,4 @@ Proof.
   iDestruct "CASE" as "[?|?]"; [iLeft|iRight]; by iFrame "Hshr".
 Qed.
 
-End gps_at_bor.
+End gps_at_bor_PP.