From 76ae55406ebe8ca74b27b271397a553b0c1bc8fc Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 5 Sep 2018 00:33:05 +0200
Subject: [PATCH] WIP: atomic gps
---
_CoqProject | 2 +-
theories/lang/lock.v | 20 ++--
theories/{lifetime => logic}/gps.v | 137 ++++++++++++++++++++++------
theories/typing/lib/rwlock/rwlock.v | 33 +++----
4 files changed, 135 insertions(+), 57 deletions(-)
rename theories/{lifetime => logic}/gps.v (54%)
diff --git a/_CoqProject b/_CoqProject
index fa79b28e..be764736 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,7 +15,7 @@ theories/lifetime/lifetime.v
theories/lifetime/at_borrow.v
theories/lifetime/na_borrow.v
theories/lifetime/frac_borrow.v
-theories/lifetime/gps.v
+theories/logic/gps.v
theories/lang/notation.v
theories/lang/memcpy.v
theories/lang/new_delete.v
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index f4a10dec..c6c36d42 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -2,7 +2,8 @@ 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.
-From lrust.lifetime Require Import gps at_borrow.
+From lrust.logic Require Import gps.
+From lrust.lifetime Require Import at_borrow.
Set Default Proof Using "Type".
Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
@@ -36,15 +37,10 @@ Section proof.
if pb then (if b then True else R) else True)%I.
Definition lock_proto N l γ κ (R : vProp): vProp :=
- (∃ R0, □ (R ↔ R0) ∗ ∃ t v, GPS_PP N (lock_interp R0) l κ t () v γ)%I.
+ (∃ R0, □ (R ↔ R0) ∗ ∃ t v, GPS_aPP N (lock_interp R0) l κ t () v γ)%I.
Global Instance lock_proto_ne N l γ κ: NonExpansive (lock_proto N l γ κ).
- Proof.
- rewrite /lock_proto =>????. apply bi.exist_ne => ?.
- apply bi.sep_ne; first solve_proper.
- do 2 (apply bi.exist_ne => ?). apply bi.sep_ne; [done|].
- apply at_bor_ne, GPS_PPInv_ne. solve_proper.
- Qed.
+ Proof. solve_proper. Qed.
Global Instance lock_proto_persistent N l γ κ R:
Persistent (lock_proto N l γ κ R) := _.
@@ -53,7 +49,7 @@ Section proof.
Proof.
iIntros "#Hincl". iDestruct 1 as (R0) "[#Eq Hproto]".
iDestruct "Hproto" as (t v) "Hproto".
- iExists R0. iFrame "Eq". iExists t, v. by iApply GPS_PP_lft_mono.
+ iExists R0. iFrame "Eq". iExists t, v. by iApply GPS_aPP_lft_mono.
Qed.
Lemma lock_proto_iff N l γ κ R R' :
@@ -100,7 +96,7 @@ Section proof.
{ iIntros "!>". iDestruct 1 as (v) "[Hl >Eq]". iDestruct "Eq" as (b) "%".
subst v. by iExists _. }
{ iDestruct "Hl" as (b) "Hl". iExists _. iFrame. by iExists _. }
- iMod (GPS_PP_Init N (lock_interp R) l κ () q (λ v, ∃ b : bool, v = #b)
+ iMod (GPS_aPP_Init N (lock_interp R) l κ () q (λ v, ∃ b : bool, v = #b)
with "LFT Htok HINV Hl [R] []") as "[$ Hproto]"; [done|done|..].
{ iIntros (t γ v [b ?]). subst v. iExists b. iSplit; [done|]. by destruct b. }
{ iIntros "!>" (??? v). iDestruct 1 as (b) "[>? ?]". by iExists _. }
@@ -121,7 +117,7 @@ Section proof.
iDestruct "Hproto" as (R0) "[#Eq Hproto]".
iDestruct "Hproto" as (t v) "PP".
iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
- iApply (GPS_PP_CAS_int_simple N (lock_interp R0) l κ q t () _
+ iApply (GPS_aPP_CAS_int_simple N (lock_interp R0) l κ q t () _
(Z_of_bool false) #true _ _ _ γ True%I (λ _ _, R0)%I
(λ t _, lock_interp R0 false l γ t () #false)
(λ _ _, R0)%I (λ _ _ _, True)%I
@@ -167,7 +163,7 @@ Section proof.
iIntros "#LFT !#" (Φ) "(HR & #Hproto & Htok) HΦ". wp_let.
iDestruct "Hproto" as (R0) "[#Eq Hproto]".
iDestruct "Hproto" as (t v) "PP".
- iApply (GPS_PP_Write N (lock_interp R0) l κ q _ t _ #(Z_of_bool false) _ ()
+ iApply (GPS_aPP_Write N (lock_interp R0) l κ q _ t _ #(Z_of_bool false) _ ()
with "[$LFT $Htok $PP HR]"); [by move => []|done..|by right| |].
{ simpl. iIntros "!>" (t' Ext') "PP' !>". iExists false.
iSplit; [done|by iApply "Eq"]. }
diff --git a/theories/lifetime/gps.v b/theories/logic/gps.v
similarity index 54%
rename from theories/lifetime/gps.v
rename to theories/logic/gps.v
index abb13c8d..6fa5917e 100644
--- a/theories/lifetime/gps.v
+++ b/theories/logic/gps.v
@@ -3,11 +3,11 @@ From lrust.lang Require Import notation.
From lrust.lifetime Require Import at_borrow.
From gpfsl.gps Require Import middleware.
-Section gps_at_bor_SW.
+Section gps_at_bor_SP.
Context `{!noprolG Σ, !gpsG Σ Prtcl, !lftG view_Lat (↑histN) Σ} (N: namespace).
Local Notation vProp := (vProp Σ).
-Implicit Types (IP : interpC Σ Prtcl) (l : loc)
+Implicit Types (IP : interpC Σ Prtcl) (IPC: interpCasC Σ Prtcl) (l : loc)
(s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
(κ : lft) (γ : gname).
@@ -20,7 +20,89 @@ Definition GPS_aSP_SharedReader IP IPC l κ t s v q γ : vProp :=
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.
+Lemma GPS_aSP_Init IP IPC l κ s q P (Q: time → val → gname → vProp) E
+ (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+ ⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
+ &{κ} (∃ v, l ↦ v ∗ ⌜P v⌝) -∗
+ (∀ t γ v, ⌜P v⌝ -∗ GPS_SWWriter l t s v γ -∗ ▷ IP true l γ t s v ∗ Q t v γ) -∗
+ (□ ∀ t γ s v, ▷ IP true l γ t s v ={↑histN}=∗ ⌜P v⌝) ={E}=∗
+ (q).[κ] ∗ ∃ γ t v, GPS_aSP_Reader IP IPC l κ t s v γ ∗ Q t v γ.
+Proof.
+ iIntros "#LFT Htok #HINV Hl HP #HP2".
+ iMod (bor_acc_cons with "LFT Hl Htok") as "[Hl Hclose]"; first done.
+ iDestruct "Hl" as (v) ">[Hl #P]".
+ set Q' : time → gname → vProp :=
+ (λ t γ, Q t v γ ∗ GPS_SWReader l t s v γ)%I.
+ iMod (GPS_SWRaw_Init_vs_strong IP l IPC true _ _ Q' with "Hl [HP]")
+ as (γ t) "[Inv [Q R]]".
+ { iIntros (t γ) "W". iDestruct (GPS_SWWriter_Reader with "W") as "#$".
+ by iApply ("HP" with "P W"). }
+ iMod ("Hclose" with "[] Inv") as "[Hl Htok]".
+ { iIntros "!> Inv".
+ iMod (GPS_INV_dealloc IP l IPC true with "HINV Inv")
+ as (t' s' v') "[Hl IP]"; [done|].
+ iMod ("HP2" with "IP") as "P'".
+ iIntros "!> !>". iExists _. by iFrame. }
+ iMod (bor_share N with "Hl") as "Hl"; [done|].
+ iFrame "Htok". iExists γ, t, v. by iFrame "∗".
+Qed.
+
+Lemma GPS_aSP_Read IP IPC l κ q R (o: memOrder) t s v γ tid E
+ (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
+ (RLX: o = Relaxed ∨ o = AcqRel) :
+ {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Reader IP IPC 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') ∧
+ (IPC l γ t' s' v' ={E ∖ ↑N}=∗
+ IPC l γ t' s' v' ∗ R t' s' v'))) }}}
+ Read o #l in tid @ E
+ {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝
+ ∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ ∗ (q).[κ]
+ ∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
+Proof.
+ iIntros (Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
+ iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
+ iApply (GPS_SWRaw_Read IP l IPC 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_aSP_SWWrite_rel IP IPC l κ q Q Q1 Q2 t s s' v v' γ tid E
+ (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
+ (Exts: s ⊑ s') :
+ let WVS: vProp :=
+ (∀ t', ⌜(t < t')%positive⌝ -∗ GPS_SWWriter l t' s' v' γ -∗ Q2
+ ={E ∖ ↑N}=∗ (<obj> (Q1 ={E ∖ ↑N}=∗ IPC l γ t s v)) ∗
+ |={E ∖ ↑N}=> (IP true l γ t' s' v' ∗ Q t'))%I in
+ {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Writer IP IPC l κ t s v γ
+ ∗ ▷ WVS ∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ Q1 ∗ Q2) }}}
+ Write AcqRel #l v' in tid @ E
+ {{{ t', RET #☠; ⌜(t < t')%positive⌝ ∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ
+ ∗ (q).[κ] ∗ Q t' }}}.
+Proof.
+ iIntros (VS Φ) "(#LFT & Htok & [W #Hshr] & VS) Post".
+ iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
+ iApply (GPS_SWRaw_SWWrite_rel IP l IPC Q Q1 Q2 t s s' v v' γ tid Vb
+ with "[$W $Hproto $VS]"); [done|solve_ndisj|..].
+ iNext. iIntros (t') "(Ext & R' & Hproto & Q)".
+ iMod ("Hclose1" with "Hproto") as "Htok".
+ iApply ("Post" $! t' with "[$Ext $R' $Hshr $Htok $Q]").
+Qed.
+
+(*
+GPS_SWRaw_SharedWriter_CAS_int_weak
+GPS_SWRaw_SharedWriter_revert
+GPS_SWRaw_SharedWriter_CAS_int_strong
+GPS_SWSharedReaders_join
+GPS_SWWriter_shared
+*)
+
+End gps_at_bor_SP.
Section gps_at_bor_PP.
Context `{!noprolG Σ, !gpsG Σ Prtcl, !gpsExAgG Σ, !lftG view_Lat (↑histN) Σ}
@@ -31,23 +113,23 @@ Implicit Types (IP : interpC Σ Prtcl) (l : loc)
(s : pr_stateT Prtcl) (t : time) (v : val) (E : coPset) (q: Qp)
(κ : lft) (γ : gname).
-Definition GPS_PP IP l κ t s v γ : vProp :=
+Definition GPS_aPP IP l κ t s v γ : vProp :=
(GPS_PP_Local l t s v γ ∗ &at{κ, N} (GPS_PPInv IP l γ))%I.
-Global Instance GPS_PP_ne l κ t s v γ: NonExpansive (λ IP, GPS_PP IP l κ t s v γ).
+Global Instance GPS_aPP_ne l κ t s v γ: NonExpansive (λ IP, GPS_aPP IP l κ t s v γ).
Proof. move => ????. apply bi.sep_ne; [done|]. by apply at_bor_ne, GPS_PPInv_ne. Qed.
-Global Instance GPS_PP_ne_persistent: Persistent (GPS_PP IP l κ t s v γ) := _.
+Global Instance GPS_aPP_ne_persistent: Persistent (GPS_aPP IP l κ t s v γ) := _.
-Lemma GPS_PP_lft_mono IP l κ κ' t s v γ :
- κ' ⊑ κ -∗ GPS_PP IP l κ t s v γ -∗ GPS_PP IP l κ' t s v γ.
+Lemma GPS_aPP_lft_mono IP l κ κ' t s v γ :
+ κ' ⊑ κ -∗ GPS_aPP IP l κ t s v γ -∗ GPS_aPP IP l κ' t s v γ.
Proof. iIntros "#Hincl". iDestruct 1 as "[$ Inv]". by iApply at_bor_shorten. Qed.
-Lemma GPS_PP_Init IP l κ s q P E (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
+Lemma GPS_aPP_Init IP l κ s q P E (DISJ: N ## lftN) (SUB: ↑lftN ⊆ E):
⎡ lft_ctx ⎤ -∗ (q).[κ] -∗ ▷ ⎡ hist_inv ⎤ -∗
&{κ} (∃ v, l ↦ v ∗ ⌜P v⌝) -∗
(∀ t γ v, ⌜P v⌝ -∗ ▷ IP true l γ t s v) -∗
(□ ∀ t γ s v, ▷ IP true l γ t s v ={↑histN}=∗ ⌜P v⌝) ={E}=∗
- (q).[κ] ∗ ∃ γ t v, GPS_PP IP l κ t s v γ.
+ (q).[κ] ∗ ∃ γ t v, GPS_aPP IP l κ t s v γ.
Proof.
iIntros "#LFT Htok #HINV Hl HP #HP2".
iMod (bor_acc_cons with "LFT Hl Htok") as "[Hl Hclose]"; first done.
@@ -64,21 +146,20 @@ 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 γ
+Lemma GPS_aPP_Read IP l κ q R (o: memOrder) t s v γ tid E
+ (DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E) (SUB3: ↑N ⊆ E)
+ (RLX: o = Relaxed ∨ o = AcqRel) :
+ {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP 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).[κ]
+ {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝ ∗ GPS_aPP 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".
+ iIntros (Φ) "(#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|..].
@@ -87,19 +168,19 @@ Proof.
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):
- o = Relaxed ∨ o = AcqRel →
+Lemma GPS_aPP_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)
+ (RLX: o = Relaxed ∨ o = AcqRel) :
let VS : vProp :=
(∀ t' : time, ⌜(t < t')%positive⌝ -∗
GPS_PP_Local l t' s' v' γ ={E ∖ ↑N}=∗ IP true l γ t' s' v')%I in
- {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_PP IP l κ t s v γ
+ {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
∗ ▷ if decide (AcqRel ⊑ o)%stdpp then VS else △{tid} VS }}}
Write o #l v' in tid @ E
- {{{ t', RET #☠; GPS_PP IP l κ t' s' v' γ ∗ (q).[κ] }}}.
+ {{{ t', RET #☠; GPS_aPP IP l κ t' s' v' γ ∗ (q).[κ] }}}.
Proof.
- iIntros (RLX VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
+ iIntros (VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
iMod (at_bor_acc with "LFT Hshr Htok") as (Vb) "[Hproto Hclose1]"; [done..|].
iApply (GPS_PPRaw_Local_Write IP l o t v v' s s' γ Vb tid _ FIN
with "[$Hlc $Hproto $VS]"); [solve_ndisj|done|..].
@@ -108,7 +189,7 @@ Proof.
iApply ("Post" $! t' with "[$Hlc' $Hshr $Htok]").
Qed.
-Lemma GPS_PP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
+Lemma GPS_aPP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
P Q Q1 Q2 R tid E
(DISJ: histN ## N) (SUB1: ↑lftN ⊆ E) (SUB2: ↑histN ⊆ E ∖ ↑N) (SUB3: ↑N ⊆ E)
(ORF: orf = Relaxed ∨ orf = AcqRel)
@@ -129,7 +210,7 @@ Lemma GPS_PP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
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))))%I in
- {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_PP IP l κ t s v γ
+ {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
∗ ▷ VSC
∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
∗ (if decide (AcqRel ⊑ ow)%stdpp then P else △{tid} P ) }}}
@@ -137,10 +218,10 @@ Lemma GPS_PP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
{{{ (b: bool) t' s' (v': lit), RET #b;
(q).[κ] ∗ ⌜s ⊑ s'⌝
∗ ( (⌜b = true ∧ v' = LitInt vr ∧ (t < t')%positive⌝
- ∗ GPS_PP IP l κ t' s' vw γ
+ ∗ GPS_aPP IP l κ t' s' vw γ
∗ if decide (AcqRel ⊑ or)%stdpp then Q t' s' else ▽{tid} Q t' s')
∨ (⌜b = false ∧ lit_neq vr v' ∧ (t ≤ t')%positive⌝
- ∗ GPS_PP IP l κ t' s' #v' γ
+ ∗ GPS_aPP IP l κ t' s' #v' γ
∗ (if decide (AcqRel ⊑ orf)%stdpp
then R t' s' v' else ▽{tid} (R t' s' v'))
∗ (if decide (AcqRel ⊑ ow)%stdpp
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 4aa1f9da..cb3ab63c 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -5,6 +5,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From gpfsl.gps Require Import middleware protocols.
+From lrust.logic Require Import gps.
Set Default Proof Using "Type".
Definition rwlock_st := option (() + lft * frac * positive).
@@ -189,12 +190,13 @@ Section rwlock_inv.
Definition rwlock_noCAS : interpCasC Σ unitProtocol :=
(λ _ _ _ _ v, ⌜v = #(-1)⌝)%I.
- Definition rwlock_proto_inv l γ γs α tyO tyS : vProp :=
- GPS_INV (rwlock_interp γs α tyO tyS) l rwlock_noCAS γ.
- Definition rwlock_proto_lc l γ (tyO: vProp) (tyS: lft → vProp) tid ty: vProp :=
+ Definition rwlock_proto' l γ γs κ (tyO: vProp) (tyS: lft → vProp): vProp :=
+ (∃ t v, GPS_aSP_Reader rwlockN (rwlock_interp γs κ tyO tyS)
+ rwlock_noCAS l κ t () v γ)%I.
+ Definition rwlock_proto l γ γs κ tyO tyS tid ty: vProp :=
((▷ □ (tyO ↔ (l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
(▷ □ (∀ α, tyS α ↔ ty.(ty_shr) α tid (l +ₗ 1))) ∗
- (∃ t v, GPS_SWReader l t () v γ))%I.
+ rwlock_proto' l γ γs κ tyO tyS)%I.
Lemma rwlock_interp_comparable γs α tyO tyS l γ t s v (n: Z):
rwlock_interp γs α tyO tyS true l γ t s v ∨
@@ -206,11 +208,11 @@ Section rwlock_inv.
iExists _; iPureIntro ;(split; [done|by constructor]).
Qed.
- Global Instance rwlock_proto_lc_persistent:
- Persistent (rwlock_proto_lc l γ tyO tyS tid ty) := _.
+ Global Instance rwlock_proto_persistent:
+ Persistent (rwlock_proto l γ γs κ tyO tyS tid ty) := _.
- Global Instance rwlock_proto_lc_type_ne n l γ tyO tyS tid :
- Proper (type_dist2 n ==> dist n) (rwlock_proto_lc l γ tyO tyS tid).
+ Global Instance rwlock_proto_type_ne n l γ γs κ tyO tyS tid :
+ Proper (type_dist2 n ==> dist n) (rwlock_proto l γ γs κ tyO tyS tid).
Proof.
move => ???.
apply bi.sep_ne; [|apply bi.sep_ne]; [..|done];
@@ -222,16 +224,16 @@ Section rwlock_inv.
apply bi.iff_ne; [done|apply ty_shr_type_dist]; [by apply type_dist2_S|done..].
Qed.
- Global Instance rwlock_proto_lc_ne l γ tyO tyS tid :
- NonExpansive (rwlock_proto_lc l γ tyO tyS tid).
+ Global Instance rwlock_proto_ne l γ γs κ tyO tyS tid :
+ NonExpansive (rwlock_proto l γ γs κ tyO tyS tid).
Proof.
- intros n ???. eapply rwlock_proto_lc_type_ne, type_dist_dist2. done.
+ intros n ???. by eapply rwlock_proto_type_ne, type_dist_dist2.
Qed.
- Lemma rwlock_proto_lc_proper E L ty1 ty2 q :
+ Lemma rwlock_proto_proper E L ty1 ty2 q :
eqtype E L ty1 ty2 →
- llctx_interp L q -∗ ∀ l γ tyO tyS tid, □ (elctx_interp E -∗
- rwlock_proto_lc l γ tyO tyS tid ty1 -∗ rwlock_proto_lc l γ tyO tyS tid ty2).
+ llctx_interp L q -∗ ∀ l γ γs κ tyO tyS tid, □ (elctx_interp E -∗
+ rwlock_proto l γ γs κ tyO tyS tid ty1 -∗ rwlock_proto l γ γs κ tyO tyS tid ty2).
Proof.
(* TODO : this proof is essentially [solve_proper], but within the logic.
It would easily gain from some automation. *)
@@ -254,8 +256,7 @@ Section rwlock_inv.
(q / 2).[α] -∗
&{α} ((l +ₗ 1) ↦∗{1}: ty_own ty tid)%I -∗
▷ (∃ n : Z, l ↦{1} #n ∗ ⌜-1 ≤ n⌝) ={E}=∗
- (q / 2).[α] ∗ (∃ γ γs tyO tyS, rwlock_proto_lc l γ tyO tyS tid ty
- ∗ ▷ rwlock_proto_inv l γ γs α tyO tyS).
+ (q / 2).[α] ∗ (∃ γ γs tyO tyS, rwlock_proto l γ γs α tyO tyS tid ty).
Proof.
iIntros "#LFT Htok Hvl H".
set tyO : vProp := ((l +ₗ 1) ↦∗{1}: ty.(ty_own) tid)%I.
--
GitLab