From 2830609bfe4ed1e528b78ba149c3840db68e8868 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sat, 9 Jun 2018 02:25:15 +0200
Subject: [PATCH] finish rwlock, build with iris's fupd_step_wp branch and
gpfsl's step_fupd branch
---
_CoqProject | 1 +
theories/lang/lock.v | 8 +-
theories/typing/lib/rwlock/rwlock_code.v | 152 +++++++-----------
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
.../typing/lib/rwlock/rwlockreadguard_code.v | 88 +++++-----
5 files changed, 98 insertions(+), 153 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 75aca45b..98f2232e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -68,6 +68,7 @@ theories/typing/lib/rwlock/rwlockreadguard.v
theories/typing/lib/rwlock/rwlockwriteguard.v
theories/typing/lib/rwlock/rwlock_code.v
theories/typing/lib/rwlock/rwlockwriteguard_code.v
+theories/typing/lib/rwlock/rwlockreadguard_code.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index fe60fc3d..5071c8ef 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -143,11 +143,11 @@ Section proof.
{ iSplitL ""; [|iSplitL ""]; [iNext; iModIntro..|].
- iIntros (?? _). by iApply lock_interp_comparable.
- by iIntros (??)"_ #$".
- - iFrame "rTrue". iNext. rewrite /= -(bi.True_sep' (∀ _, _)%I).
+ - iFrame "rTrue". rewrite /= -(bi.True_sep' (∀ _, _)%I).
iApply (rel_sep_objectively with "[$rTrue]").
- iModIntro. iIntros ([] _). iSplit; [|by iIntros (?) "??"].
- iIntros "_ F _". iModIntro. rewrite /lock_interp /=.
- iExists (). iSplitL ""; [done|]. iDestruct "F" as (b) "[Eq R0]".
+ iModIntro. iIntros ([] _). iSplit; [|iNext; by iIntros (?) "??"].
+ iIntros "_ F _". iDestruct "F" as (b) "[>Eq R0]".
+ iModIntro. rewrite /lock_interp /=. iExists (). iSplitL ""; [done|].
iDestruct "Eq" as %Eq. destruct b; [by inversion Eq|].
iFrame "R0". iSplit; by iExists true. }
iNext. iIntros (b v' s') "(inv & _ & CASE)"; simpl.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 0e440d8f..fbf3717e 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -206,31 +206,14 @@ Section rwlock_functions.
(∃ qν ν, (qν).[ν] ∗
(□ tyS (β ⊓ ν)) ∗
rwown γs (reading_st qν ν) ∗
- ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+ (□ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν])) ∗
∃ n, GPS_SWSharedReader lx (() : unitProtocol) #n qν γ))%I.
set R : () → lit → vProp Σ := (λ _ _, True)%I.
set P : vProp Σ := (<obj> (qβ / 2).[β])%I.
- set T : () → () → vProp Σ :=
- (λ _ _, (qβ / 2).[β] ∗
- □ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
- ∃ ν q' st2, (q').[ν] ∗
- rwown γs (reading_st (q'/2) ν) ∗
- rwown γs (st_global st2) ∗
- □ tyS (β ⊓ ν) ∗
- □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
- (∃ n', GPS_SWSharedReader lx (() : unitProtocol) #n' q' γ) ∗
- ( (∃ q, ⌜st2 = (Some (inr (ν, (q + q'/2)%Qp,
- (Z.to_pos (Z_of_rwlock_st st') + 1)%positive)))
- ∧ 0 < Z_of_rwlock_st st'
- ∧ (q + q')%Qp = 1%Qp⌝ ∗
- ([†ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO))
- ∨ (⌜st2 = (Some (inr (ν, (1 / 2)%Qp, 1%positive))) ∧ q' = 1%Qp
- ∧ 0 = Z_of_rwlock_st st'⌝ ∗
- ([†β ⊓ ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO))))%I.
iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
iApply (GPS_SWSharedWriter_CAS_int (rwlock_interp γs β tyO tyS) _
rwlock_noCAS _ _ _ (Z_of_rwlock_st st') #(Z_of_rwlock_st st' + 1)
- () _ _ P T Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
+ () _ _ P Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
with "[$R' $INV Hβtok2 rTrue]");
[done|solve_ndisj|by left|done|by right
|by left|iSplitL ""; last iSplitL ""|..].
@@ -239,68 +222,51 @@ Section rwlock_functions.
{ simpl. iSplitL ""; last first.
{ rewrite -{2}(bi.True_sep' P).
iApply (rel_sep_objectively with "[$rTrue Hβtok2]"). by iModIntro. }
- iNext. rewrite -(bi.True_sep' (∀ _ : (), _)%I).
+ rewrite -(bi.True_sep' (∀ _ : (), _)%I).
iApply (rel_sep_objectively with "[$rTrue]"). iModIntro.
- iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
- iSplit.
+ iIntros ([] _). iSplit; [|by iIntros "!>" (?) "_ _"]. iSplit.
{ rewrite /rwlock_noCAS. iIntros "_" (Eq) "_".
inversion Eq as [Eq1]. rewrite Eq1 in Hm1. exfalso. by apply Hm1. }
- iSplitL "".
- - iIntros "Hβtok2". iDestruct 1 as (st2) "[Eqst [g INT]]".
- iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
- iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
- destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
- + exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega.
- + iDestruct 1 as (?) "[_ #Share]". iDestruct "INT" as "[W INT]".
- iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & Hν & Rs)".
- iDestruct "Hqq'" as %Hqq'.
- iMod (rwown_update_read ν n q q' γs Hqq' with "g") as "[g rst]".
- iModIntro. iExists (). iSplitL ""; [done|].
- iSplitR "W"; last by rewrite Eqst2.
- iFrame "Share Hβtok2". iExists ν, q', _. rewrite Eqst2.
- iFrame "Hν g rst Hshr H† Rs". iLeft. iExists q. by iFrame "Hh".
- + iDestruct 1 as (?) "[_ #Share]".
- iDestruct "INT" as "(Hown & W & Rs)".
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
- iMod (rwown_update_write_read ν γs with "g") as "[g rst]".
- iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
- iApply (fupd_mask_mono (↑lftN ∪ ↑histN)).
- { apply union_subseteq; split; solve_ndisj. }
- iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hown") as "[Hst Hh]";
- [apply union_subseteq_l|iApply lft_intersect_incl_l|].
- iMod ("Share" with "[%] Hst Htok") as "[#Hshr Htok]". apply union_subseteq_l.
- iDestruct ("Hclose" with "Htok") as "[Hβtok2 Htok2]".
- iCombine "Htok1" "Htok2" as "Htok".
- iModIntro. iExists (). iSplitL ""; [done|].
- iSplitR "W"; last by rewrite Eqst2.
- iFrame "Share Hβtok2". iExists ν, 1%Qp, _. rewrite Eqst2.
- iFrame "Htok g rst Hshr Hhν Rs". iRight. by iFrame "Hh".
- - iIntros ([] _) "[Hβtok2 [#Share T]] W". iModIntro.
- iDestruct "T" as (ν q' st2)
- "([Htok1 Htok2] & rst & g & #Hshr & #H† & R & [T|T])".
- + iDestruct "R" as (vR') "[R1 R2]".
- iDestruct "T" as (q (? & Post' & Hqq')) "Hh". iFrame "Hβtok2".
- have Eqst: Z_of_rwlock_st st'+1 = Z.pos (Z.to_pos (Z_of_rwlock_st st')+1).
- { by rewrite -Pos2Z.add_pos_pos Z2Pos.id. }
- iSplitL "Htok2 rst R1"; last iSplitR "".
- * iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
- * iExists st2. subst st2. rewrite /= -Eqst. iSplitL ""; [done|].
- iFrame "g W". iExists _. iFrame "H† Hh Hshr Htok1".
- rewrite -Qp_plus_assoc Qp_div_2. iSplitL ""; [done|by iExists _].
- * iExists st2. subst st2. rewrite /= -Eqst. by iFrame "Share".
- + iDestruct "R" as (vR') "[R1 R2]".
- iDestruct "T" as ((Post' & Eq' & Eqst)) "Hh". iFrame "Hβtok2".
- subst q'. rewrite -Eqst /=. iSplitL "Htok2 rst R1"; last iSplitR "".
- * iExists _, _. iFrame "Htok2 Hshr rst H†". simpl. by iExists _.
- * iExists st2. subst st2. simpl. iSplitL ""; [done|].
- iFrame "g W". iExists _. iFrame "H† Hshr Htok1".
- iSplitL "Hh". { iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
- rewrite Qp_div_2. iSplitL ""; [done|by iExists _].
- * iExists st2. subst st2. rewrite /=. by iFrame "Share". }
+ iIntros "Hβtok2". iDestruct 1 as (st2) "[Eqst [g INT]]".
+ iDestruct 1 as (?) "[_ #Share]".
+ iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
+ iDestruct "Eqst" as ">Eqst". iDestruct "Eqst" as %Eqst.
+ inversion Eqst as [Eqst2]. clear Eqst.
+ iModIntro. iExists (). iSplitL ""; [done|].
+ destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
+ - exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega.
+ - rewrite Eqst2. iDestruct "INT" as "[$ INT]". iIntros "W' !> !>".
+ iDestruct "INT" as (q') "(#H† & Hh & #Hshr & Hqq' & [Htok1 Htok2] & R)".
+ iDestruct "Hqq'" as %Hqq'. iDestruct "R" as (vR') "[R1 R2]".
+ iMod (rwown_update_read ν n q q' γs Hqq' with "g") as "[g rst]".
+ iModIntro. iSplitL "Htok2 rst R1 Hβtok2 H†".
+ + iFrame "Hβtok2". iExists _,_. iFrame "Htok2 Hshr rst H†". by iExists _.
+ + iSplitR ""; iExists (Some (inr (ν, (q + q' / 2)%Qp, (n + 1)%positive)));
+ [|by iFrame "Share"]. iSplitL ""; [done|]. iFrame "g W'".
+ iExists _. iFrame "H† Hh Hshr Htok1".
+ rewrite -Qp_plus_assoc Qp_div_2. iSplitL ""; [done|by iExists _].
+ - rewrite Eqst2. iDestruct "INT" as "(Hown & $ & R)". iIntros "W' !> !>".
+ iDestruct "R" as (vR') "[R1 R2]".
+ iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #H†]". solve_ndisj.
+ iMod (rwown_update_write_read ν γs with "g") as "[g rst]".
+ iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+ iApply (fupd_mask_mono (↑lftN ∪ ↑histN)).
+ { apply union_subseteq; split; solve_ndisj. }
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hown") as "[Hst Hh]";
+ [apply union_subseteq_l|iApply lft_intersect_incl_l|].
+ iMod ("Share" with "[%] Hst Htok") as "[#Hshr Htok]". apply union_subseteq_l.
+ iDestruct ("Hclose" with "Htok") as "[Hβtok2 Htok2]".
+ iModIntro. iSplitL "Htok2 rst R1 Hβtok2".
+ + iFrame "Hβtok2". iExists _,_. iFrame "Htok2 Hshr rst H†". by iExists _.
+ + iSplitR ""; iExists (Some (inr (ν, (1 / 2)%Qp, 1%positive)));
+ [|by iFrame "Share"]. iSplitL ""; [done|]. iFrame "g W'".
+ iExists _. iFrame "H† Hshr Htok1".
+ iSplitL "Hh". { iIntros "Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
+ rewrite Qp_div_2. iSplitL ""; [done|by iExists _]. }
iNext. simpl.
- iIntros (b v' []) "(INV & _ &[([%%] & R2 & Hβtok2 & Hβ) | ([% Neq] & R2 & _ & P)])".
- + subst b v'. iDestruct "Hβ" as (q' ν) "(Hν & Hshr & Hreading & H† & R3)".
+ iIntros (b v' []) "(INV&_&[([%%]&_& Hβtok2 & Hβ) | ([% Neq] &_&_& P)])".
+ + subst b v'. iDestruct "Hβ" as (q' ν) "(Hν & Hshr & Hreading & #H† & R3)".
iMod ("Hclose''" with "INV") as "Hβtok1".
iModIntro. wp_case.
iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
@@ -375,14 +341,9 @@ Section rwlock_functions.
(∃ n' : lit, GPS_SWSharedReader lx (() : unitProtocol) #n' 1 γ))%I.
set R : () → lit → vProp Σ := (λ _ _, True)%I.
set P : vProp Σ := True%I.
- set T : () → () → vProp Σ :=
- (λ _ _, rwown γs (st_global None) ∗
- □ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
- &{β} tyO ∗
- (∃ n', GPS_SWSharedReader lx (() : unitProtocol) #n' 1 γ))%I.
iMod (rel_True_intro True%I tid with "[//]") as "#rTrue".
iApply (GPS_SWSharedWriter_CAS_int (rwlock_interp γs β tyO tyS) _
- rwlock_noCAS _ _ _ 0 #(-1) () _ _ P T Q R _ Vb _ (⊤ ∖ ↑rwlockN)
+ rwlock_noCAS _ _ _ 0 #(-1) () _ _ P Q R _ Vb _ (⊤ ∖ ↑rwlockN)
with "[$R $INV rTrue]");
[done|solve_ndisj|by left|done|by right|by left|iSplitL ""; last iSplitL ""|..].
{ iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
@@ -390,26 +351,23 @@ Section rwlock_functions.
{ simpl. iSplitL ""; last first.
{ rewrite -(bi.True_sep' P). iApply (rel_sep_objectively with "[$rTrue]").
by iModIntro. }
- iNext. rewrite -(bi.True_sep' (∀ _ : (), _)%I).
+ rewrite -(bi.True_sep' (∀ _ : (), _)%I).
iApply (rel_sep_objectively with "[$rTrue]"). iModIntro.
- iIntros ([] _). iSplit; [|by iIntros (?) "_ _"].
+ iIntros ([] _). iSplit; [|by iIntros "!>" (?) "_ _"].
iSplit. { rewrite /rwlock_noCAS. iIntros "_" (Eq) "_". by inversion Eq. }
- iSplitL "".
- - iIntros "_". iDestruct 1 as (st2) "[Eqst [g INT]]".
- iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
- destruct st2 as [[[]|[[]]]|]; simpl in Eqst2; [done|done|..].
- iDestruct 1 as (?) "[_ #Share]". iExists (). iSplitL ""; [done|].
- iDestruct "INT" as "(Hown & $ & R)". by iFrame "g Share Hown R".
- - iIntros ([] _) "(g & #Share & Hown & R) W".
- iMod (rwown_update_write with "g") as "[g wst]".
- iModIntro. iSplitR "g"; last iSplitR "".
- + by iFrame "Hown wst W R".
- + iExists (Some (inl ())). by iFrame "g".
- + iExists (Some (inl ())). by iFrame "Share". }
+ iIntros "_". iDestruct 1 as (st2) "[Eqst [g INT]]".
+ iDestruct 1 as (?) "[_ #Share]". iDestruct "Eqst" as ">Eqst".
+ iDestruct "Eqst" as %Eqst. inversion Eqst as [Eqst2]. clear Eqst.
+ iExists (). iSplitL ""; [done|].
+ destruct st2 as [[[]|[[]]]|]; simpl in Eqst2; [done|done|..].
+ iDestruct "INT" as "(Hown & $ & R)". iIntros "!> W' !> !>".
+ iMod (rwown_update_write with "g") as "[g wst]". iModIntro.
+ iFrame "Hown wst W' R".
+ iSplitR""; iExists (Some (inl ())); [by iFrame "g"|by iFrame "Share"]. }
iNext. simpl.
iIntros (b v' [])
- "(INV & _ &[([%%] &_& Hβ & wst & W & R') | ([% Neq] & R' & _ & _)])".
+ "(INV & _ &[([%%] &_& Hβ & wst & W & R') | ([% _] & _)])".
- subst b v'.
iDestruct "R'" as (?) "R'".
iMod (GPS_SWSharedWriter_revert with "W R' INV") as "[W INV]".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 0b18e1b5..6763c1ca 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -23,7 +23,7 @@ Section rwlockreadguard.
| [ #(LitLoc l) ] =>
∃ ν q γs β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
α ⊑ β ∗ q.[ν] ∗ rwown γs (reading_st q ν) ∗
- (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
+ □ (1.[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
(∃ γ tyO tyS, (∃ n, GPS_SWSharedReader l () #n q γ) ∗
rwlock_proto_lc l γ tyO tyS tid ty ∗
&at{β,rwlockN}(rwlock_proto_inv l γ γs β tyO tyS))
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 5c83eb43..a612153f 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -73,8 +73,8 @@ Section rwlockreadguard_functions.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']".
destruct x' as [[|lx'|]|]; try done. simpl.
- iDestruct "Hx'" as (ν q γs β) "(Hx' & #Hαβ & Hν & H◯ & H† & Hinv)".
- iDestruct "Hinv" as (γ tyO tyS) "(R & (EqO & EqS & _) & #Hinv)".
+ iDestruct "Hx'" as (ν q γs β) "(#Hx' & #Hαβ & Hν & H◯ & #H† & Hinv)".
+ iDestruct "Hinv" as (γ tyO tyS) "(R & (#EqO & #EqS & _) & #Hinv)".
iDestruct "R" as (vR) "R".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
@@ -93,60 +93,46 @@ Section rwlockreadguard_functions.
set P : vProp Σ := (rwown γs (reading_st q ν) ∗ (q).[ν])%I.
set Q : () → vProp Σ := (λ _, True)%I.
set R : () → lit → vProp Σ := (λ _ _, True)%I.
- set T : () → () → vProp Σ :=
- (λ _ _, (q).[ν] ∗
- □ (∀ κ q0 E0, ⌜lftE ⊆ E0⌝ -∗ &{κ} tyO -∗ (q0).[κ] ={E0}=∗ □ tyS κ ∗ (q0).[κ]) ∗
- rwown γs (reading_st q ν) ∗
- ∃ q' n,
- ⌜Z_of_rwlock_st st2 = Z.pos n ∧
- (q' = q ∧ n = 1%positive ∨
- (∃ q0 : Qp, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝ ∗
- rwown γs (st_global (Some (inr (ν,q',n)))) ∗
- (∃ qr, □ ((1).[ν] ={↑lftN ∪ ↑histN,↑histN}▷=∗ [†ν]) ∗
- ([†ν] ={↑lftN ∪ ↑histN}=∗ &{β} tyO) ∗
- □ tyS (β ⊓ ν) ∗
- ⌜(q' + qr)%Qp = 1%Qp⌝ ∗
- (qr).[ν] ∗
- (∃ n', GPS_SWSharedReader lx' ((): unitProtocol) #n' qr γ)))%I.
iApply (GPS_SWSharedWriter_CAS_int_strong (rwlock_interp γs β tyO tyS) _
rwlock_noCAS _ _ _ _ #(Z_of_rwlock_st st2 - 1) () _ _ _
- P T Q R _ Vb' _ (⊤ ∖ ↑rwlockN)
- with "[$R $INV H◯ Hν]");
- [done|solve_ndisj|by left|done|by left|by right|iSplitL ""; last iSplitL ""|..].
+ P Q R _ Vb' _ ∅ with "[$R $INV H◯ Hν]");
+ [solve_ndisj|solve_ndisj|by left|done|by left|by right
+ |iSplitL ""; last iSplitL ""|..].
{ iIntros "!> !>" (???). by iApply rwlock_interp_comparable. }
{ iIntros "!> !>" (???). by iApply rwlock_interp_duplicable. }
{ simpl. iSplitR "H◯ Hν"; last iFrame "∗".
- iNext. iIntros ([] _). iSplit; [|by iIntros (?) "_ _"]. iSplitL "".
- - iIntros "(H◯ & Hν)". iDestruct 1 as (st2') "[Eqst [H● INT]]".
- iDestruct "Eqst" as %Eqst.
- iDestruct (rwown_global_reading_st with "H● H◯") as %[q' [n [Eqst2' CASE]]].
- subst st2'. simpl in Eqst. iDestruct 1 as (?) "[_ #Share]". iModIntro.
- iExists (). rewrite Eqst /=. iSplitL ""; [done|].
- iDestruct "INT" as "[$ INT]". rewrite /T. iFrame "Hν Share H◯".
- iExists _,_. iFrame "H●". iSplitL""; [by inversion Eqst|]. iFrame "INT".
- - iIntros ([] _) "(Hν & #Share & H◯ & T) W R". iSplitL ""; [done|].
- iDestruct "T" as (q' n [Eqst Eq']) "[H● T]".
- iDestruct "T" as (qr) "(#H† & Hh & #Hshr & Hqrq' & Hqr & Rm)".
- iDestruct "Hqrq'" as %Hqrq'.
- iDestruct "Rm" as (?) "Rm".
+ iIntros ([] _). iSplit; [|by iIntros "!>" (?) "_ _"].
+ iIntros "(H◯ & Hν) INT". iDestruct 1 as (?) "[_ #Share]".
+ iDestruct "INT" as (st2') "[>Eqst [>H● INT]]". iDestruct "Eqst" as %Eqst.
+ iDestruct (rwown_global_reading_st with "H● H◯") as %[q' [n [Eqst2' CASE]]].
+ subst st2'. simpl in Eqst. iExists (). rewrite Eqst /=. iSplitL ""; [done|].
+ iDestruct "INT" as "[$ INT]".
+ iDestruct "INT" as (qr) "(_ & Hh & #Hshr & >Hqrq' & >Hqr & Rm)".
+ iDestruct "Hqrq'" as %Hqrq'. iCombine "Hν" "Hqr" as "Hν".
+ destruct CASE as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
+ - rewrite Hqrq'. iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●".
+ iIntros "!> W R".
+ iApply (step_fupd_mask_mono (↑lftN ∪ ↑histN) _ _ (↑histN));
+ [solve_ndisj|apply union_least; solve_ndisj|..].
+ iMod ("H†" with "Hν") as "Hν". iIntros "!> !>". iMod "Hν".
+ iMod ("Hh" with "Hν") as "Hb". iModIntro.
+ inversion Eqst as [Eqst1]. rewrite Eqst1 /=. iSplitL""; [done|].
+ iSplitR ""; iExists None; [|by iFrame "Share"]. iSplitL ""; [done|].
+ iFrame "H● Hb W". iDestruct "Rm" as (?) "Rm".
iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R".
- iCombine "Hν" "Hqr" as "Hν".
- destruct Eq' as [[??]|[[q0 ?] Eqn]]; [subst q' n|subst q'].
- + rewrite Hqrq'.
- iMod (rwown_update_read_dealloc_1 with "H● H◯") as "H●". iModIntro.
- rewrite Eqst /=. iSplitR ""; iExists None; [|by iFrame "Share"].
- iSplitL ""; [done|]. iFrame "H● W". iSplitR "R"; [|by iExists _].
- admit.
- (* iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
- iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame. *)
- + rewrite Eqn Qp_plus_comm Eqst.
- iMod (rwown_update_read_dealloc with "H● H◯") as "H●". iModIntro.
- have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
- { rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
- iSplitR ""; iExists (Some (inr (ν, q0, Pos.pred n))); [|by iFrame "Share"].
- iSplitL ""; [done|]. iFrame "H● W".
- iExists (q + qr)%Qp. iFrame "H† Hh Hshr Hν". iSplitR "R"; [|by iExists _].
- by rewrite Qp_plus_assoc (Qp_plus_comm q0). }
+ rewrite Hqrq'. by iExists _.
+ - inversion Eqst as [Eqst1]. rewrite Eqn Qp_plus_comm Eqst1.
+ iMod (rwown_update_read_dealloc with "H● H◯") as "H●".
+ iIntros "!> W R". iApply step_fupd_intro; [solve_ndisj|].
+ iIntros "!>". iSplitL ""; [done|].
+ have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
+ { rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
+ iSplitR ""; iExists (Some (inr (ν, q0, Pos.pred n))); [|by iFrame "Share"].
+ iSplitL ""; [done|]. iFrame "H● W".
+ iExists (q + qr)%Qp. iFrame "H† Hh Hshr Hν".
+ iSplitR "R Rm"; [by rewrite Qp_plus_assoc (Qp_plus_comm q0)|].
+ iDestruct "Rm" as (?) "Rm".
+ iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R". by iExists _. }
iNext. iIntros (b v' []) "(INV & _ & CASE)".
iDestruct "CASE" as "[[[% %] _]|[[% NE] [R' [_ [H◯ Hν]]]]]".
@@ -170,5 +156,5 @@ Section rwlockreadguard_functions.
iExists _,_,_. iSplitL "R'"; [by iExists _|]. iFrame "EqO EqS Hinv".
iExists _. by iFrame "RR". }
iApply type_jump; solve_typing.
- Admitted.
+ Qed.
End rwlockreadguard_functions.
--
GitLab