From 83c446d0cf8654b9bec2db1b4a87974779367e5e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 20 Jun 2017 18:02:39 +0200
Subject: [PATCH] Lifetime logic: rename shared borrows to atomic (persistent)
borrows
---
_CoqProject | 4 +-
.../lifetime/{shr_borrow.v => at_borrow.v} | 54 +++++++++----------
theories/lifetime/frac_borrow.v | 14 ++---
theories/typing/lib/arc.v | 26 ++++-----
theories/typing/lib/mutex/mutex.v | 8 +--
theories/typing/lib/mutex/mutexguard.v | 10 ++--
theories/typing/lib/rwlock/rwlock.v | 8 +--
theories/typing/lib/rwlock/rwlock_code.v | 6 +--
theories/typing/lib/rwlock/rwlockreadguard.v | 4 +-
.../typing/lib/rwlock/rwlockreadguard_code.v | 4 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 4 +-
.../typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
12 files changed, 72 insertions(+), 72 deletions(-)
rename theories/lifetime/{shr_borrow.v => at_borrow.v} (65%)
diff --git a/_CoqProject b/_CoqProject
index 451dd506..1e60dbb9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,9 +10,9 @@ theories/lifetime/model/borrow.v
theories/lifetime/model/reborrow.v
theories/lifetime/lifetime_sig.v
theories/lifetime/lifetime.v
-theories/lifetime/shr_borrow.v
-theories/lifetime/frac_borrow.v
+theories/lifetime/at_borrow.v
theories/lifetime/na_borrow.v
+theories/lifetime/frac_borrow.v
theories/lang/adequacy.v
theories/lang/heap.v
theories/lang/lang.v
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/at_borrow.v
similarity index 65%
rename from theories/lifetime/shr_borrow.v
rename to theories/lifetime/at_borrow.v
index 863295a5..01e19df6 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -3,35 +3,35 @@ From iris.proofmode Require Import tactics.
From lrust.lifetime Require Export lifetime.
Set Default Proof Using "Type".
-(** Shared bors *)
+(** Atomic persistent bors *)
(* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition shr_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
+Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
(∃ i, &{κ,i}P ∗
(⌜N ⊥ lftN⌠∗ inv N (idx_bor_own 1 i) ∨
⌜N = lftN⌠∗ inv N (∃ q, idx_bor_own q i)))%I.
-Notation "&shr{ κ , N } P" := (shr_bor κ N P)
- (format "&shr{ κ , N } P", at level 20, right associativity) : uPred_scope.
+Notation "&at{ κ , N } P" := (at_bor κ N P)
+ (format "&at{ κ , N } P", at level 20, right associativity) : uPred_scope.
-Section shared_bors.
+Section atomic_bors.
Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
- Global Instance shr_bor_ne κ n : Proper (dist n ==> dist n) (shr_bor κ N).
+ Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
Proof. solve_proper. Qed.
- Global Instance shr_bor_contractive κ : Contractive (shr_bor κ N).
+ Global Instance at_bor_contractive κ : Contractive (at_bor κ N).
Proof. solve_contractive. Qed.
- Global Instance shr_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ N).
+ Global Instance at_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (at_bor κ N).
Proof. solve_proper. Qed.
- Lemma shr_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &shr{κ, N} P -∗ &shr{κ, N} P'.
+ Lemma at_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &at{κ, N} P -∗ &at{κ, N} P'.
Proof.
iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
iApply (idx_bor_iff with "HPP' HP").
Qed.
- Global Instance shr_bor_persistent : PersistentP (&shr{κ, N} P) := _.
+ Global Instance at_bor_persistent : PersistentP (&at{κ, N} P) := _.
Lemma bor_share E κ :
- ↑lftN ⊆ E → N ⊥ lftN → &{κ}P ={E}=∗ &shr{κ, N}P.
+ ↑lftN ⊆ E → N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
Proof.
iIntros (? HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
iExists i. iFrame "#".
@@ -39,16 +39,16 @@ Section shared_bors.
Qed.
Lemma bor_share_lftN E κ :
- ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ, lftN}P.
+ ↑lftN ⊆ E → &{κ}P ={E}=∗ &at{κ, lftN}P.
Proof.
iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
iExists i. iFrame "#". subst.
iRight. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
Qed.
- Lemma shr_bor_acc E κ :
+ Lemma at_bor_acc E κ :
↑lftN ⊆ E → ↑N ⊆ E →
- lft_ctx -∗ &shr{κ,N}P ={E,E∖↑N∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑N∖↑lftN,E}=∗ True) ∨
+ lft_ctx -∗ &at{κ,N}P ={E,E∖↑N∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑N∖↑lftN,E}=∗ True) ∨
[†κ] ∗ |={E∖↑N∖↑lftN,E}=> True.
Proof.
iIntros (??) "#LFT #HP". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
@@ -63,45 +63,45 @@ Section shared_bors.
+ iRight. iFrame. iIntros "!>". by iMod "Hclose".
Qed.
- Lemma shr_bor_acc_tok E q κ :
+ Lemma at_bor_acc_tok E q κ :
↑lftN ⊆ E → ↑N ⊆ E →
- lft_ctx -∗ &shr{κ,N}P -∗ q.[κ] ={E,E∖↑N}=∗ ▷P ∗ (▷P ={E∖↑N,E}=∗ q.[κ]).
+ lft_ctx -∗ &at{κ,N}P -∗ q.[κ] ={E,E∖↑N}=∗ ▷P ∗ (▷P ={E∖↑N,E}=∗ q.[κ]).
Proof.
iIntros (??) "#LFT #HP Hκ". iDestruct "HP" as (i) "#[Hidx [[% Hinv]|[% Hinv]]]".
- iInv N as ">Hi" "Hclose".
iMod (idx_bor_acc with "LFT Hidx Hi Hκ") as "[$ Hclose']". solve_ndisj.
iIntros "!> H". iMod ("Hclose'" with "H") as "[? $]". by iApply "Hclose".
- - iMod (shr_bor_acc with "LFT []") as "[[$ Hclose]|[H†_]]"; try done.
+ - iMod (at_bor_acc with "LFT []") as "[[$ Hclose]|[H†_]]"; try done.
+ iExists i. auto.
+ subst. rewrite difference_twice_L. iIntros "!>HP". by iMod ("Hclose" with "HP").
+ iDestruct (lft_tok_dead with "Hκ H†") as "[]".
Qed.
- Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ',N}P -∗ &shr{κ,N}P.
+ Lemma at_bor_shorten κ κ': κ ⊑ κ' -∗ &at{κ',N}P -∗ &at{κ,N}P.
Proof.
iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
by iApply (idx_bor_shorten with "H⊑").
Qed.
- Lemma shr_bor_fake E κ:
- ↑lftN ⊆ E → N ⊥ lftN → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,N}P.
+ Lemma at_bor_fake E κ:
+ ↑lftN ⊆ E → N ⊥ lftN → lft_ctx -∗ [†κ] ={E}=∗ &at{κ,N}P.
Proof.
iIntros (??) "#LFT#H†". iApply (bor_share with "[>]"); try done.
by iApply (bor_fake with "LFT H†").
Qed.
- Lemma shr_bor_fake_lftN E κ:
- ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,lftN}P.
+ Lemma at_bor_fake_lftN E κ:
+ ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &at{κ,lftN}P.
Proof.
iIntros (?) "#LFT#H†". iApply (bor_share_lftN with "[>]"); try done.
by iApply (bor_fake with "LFT H†").
Qed.
-End shared_bors.
+End atomic_bors.
-Lemma shr_bor_acc_lftN `{invG Σ, lftG Σ} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{invG Σ, lftG Σ} (P : iProp Σ) E κ :
↑lftN ⊆ E →
- lft_ctx -∗ &shr{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
+ lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
-Proof. intros. by rewrite (shr_bor_acc _ lftN) // difference_twice_L. Qed.
+Proof. intros. by rewrite (at_bor_acc _ lftN) // difference_twice_L. Qed.
-Typeclasses Opaque shr_bor.
+Typeclasses Opaque at_bor.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index ad0124a1..6ff33ee6 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -2,13 +2,13 @@ From Coq Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import lib.fractional.
From iris.algebra Require Import frac.
-From lrust.lifetime Require Export shr_borrow.
+From lrust.lifetime Require Export at_borrow.
Set Default Proof Using "Type".
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
- (∃ γ κ', κ ⊑ κ' ∗ &shr{κ',lftN} ∃ q, φ q ∗ own γ q ∗
+ (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} ∃ q, φ q ∗ own γ q ∗
(⌜q = 1%Qp⌠∨ ∃ q', ⌜(q + q' = 1)%Qp⌠∗ q'.[κ']))%I.
Notation "&frac{ κ } P" := (frac_bor κ P)
(format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
@@ -31,7 +31,7 @@ Section frac_bor.
▷ □ (∀ q, φ q ↔ φ' q) -∗ &frac{κ} φ -∗ &frac{κ} φ'.
Proof.
iIntros "#Hφφ' H". iDestruct "H" as (γ κ') "[? Hφ]". iExists γ, κ'. iFrame.
- iApply (shr_bor_iff with "[Hφφ'] Hφ"). iNext. iAlways.
+ iApply (at_bor_iff with "[Hφφ'] Hφ"). iNext. iAlways.
iSplit; iIntros "H"; iDestruct "H" as (q) "[H ?]"; iExists q; iFrame; by iApply "Hφφ'".
Qed.
@@ -51,7 +51,7 @@ Section frac_bor.
iDestruct (lft_tok_dead with "Hκ H†") as "[]".
- iMod "Hclose" as "_"; last first.
iExists γ, κ. iSplitR. by iApply lft_incl_refl.
- by iApply shr_bor_fake_lftN.
+ by iApply at_bor_fake_lftN.
Qed.
Lemma frac_bor_atomic_acc E κ :
@@ -60,7 +60,7 @@ Section frac_bor.
∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
Proof.
iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
- iMod (shr_bor_acc_lftN with "LFT Hshr") as "[[Hφ Hclose]|[H†Hclose]]"; try done.
+ iMod (at_bor_acc_lftN with "LFT Hshr") as "[[Hφ Hclose]|[H†Hclose]]"; try done.
- iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
- iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
@@ -75,7 +75,7 @@ Section frac_bor.
iIntros (?) "#LFT #Hφ Hfrac Hκ". unfold frac_bor.
iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
- iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try done.
+ iMod (at_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try done.
iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
iExists qq.
@@ -90,7 +90,7 @@ Section frac_bor.
- iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. }
clear Hqφ qφ qφ0. iIntros "!>Hqφ".
- iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try done.
+ iMod (at_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try done.
iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])".
{ subst. iCombine "Hown" "Hownq" as "Hown".
by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 84099dd9..0e4bb55b 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op fractional.
From lrust.lang.lib Require Import memcpy arc.
-From lrust.lifetime Require Import shr_borrow.
+From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
Set Default Proof Using "Type".
@@ -105,7 +105,7 @@ Section arc.
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ]
={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
arc_persist tid ν γ l' ty ∗
- &shr{κ, arc_shrN}(arc_tok γ q')
+ &at{κ, arc_shrN}(arc_tok γ q')
|}%I.
Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
@@ -120,7 +120,7 @@ Section arc.
setoid_rewrite heap_mapsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
- set (C := (∃ _ _ _, _ ∗ _ ∗ &shr{_,_} _)%I).
+ set (C := (∃ _ _ _, _ ∗ _ ∗ &at{_,_} _)%I).
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
with "[Hpbown]") as "#Hinv"; first by iLeft.
iIntros "!> !# * % Htok".
@@ -154,7 +154,7 @@ Section arc.
iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν ?) "(? & ? & ?)".
iExists _, _, _. iModIntro. iFrame. iSplit.
- by iApply lft_incl_trans.
- - by iApply shr_bor_shorten.
+ - by iApply at_bor_shorten.
Qed.
Global Instance arc_wf ty `{!TyWf ty} : TyWf (arc ty) :=
@@ -226,7 +226,7 @@ Section arc.
∃ (l' : loc), &frac{κ} (λ q, l ↦{q} #l') ∗
□ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ]
={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν,
- arc_persist tid ν γ l' ty ∗ &shr{κ, arc_shrN}(weak_tok γ)
+ arc_persist tid ν γ l' ty ∗ &at{κ, arc_shrN}(weak_tok γ)
|}%I.
Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
@@ -241,7 +241,7 @@ Section arc.
setoid_rewrite heap_mapsto_vec_singleton.
iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
- set (C := (∃ _ _, _ ∗ &shr{_,_} _)%I).
+ set (C := (∃ _ _, _ ∗ &at{_,_} _)%I).
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
with "[Hpbown]") as "#Hinv"; first by iLeft.
iIntros "!> !# * % Htok".
@@ -267,7 +267,7 @@ Section arc.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν) "[??]".
- iExists _, _. iModIntro. iFrame. by iApply shr_bor_shorten.
+ iExists _, _. iModIntro. iFrame. by iApply at_bor_shorten.
Qed.
Global Instance weak_wf ty `{!TyWf ty} : TyWf (weak ty) :=
@@ -482,7 +482,7 @@ Section arc.
wp_apply (strong_count_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
- iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
+ iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
@@ -525,7 +525,7 @@ Section arc.
wp_apply (weak_count_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
- iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
+ iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
@@ -570,7 +570,7 @@ Section arc.
wp_apply (clone_arc_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
- iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
+ iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
@@ -614,7 +614,7 @@ Section arc.
wp_apply (clone_weak_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
- iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
+ iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
@@ -658,7 +658,7 @@ Section arc.
wp_apply (downgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
- iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
+ iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
@@ -705,7 +705,7 @@ Section arc.
wp_apply (upgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
- iMod (shr_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
+ iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 8d86ce50..dda30446 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -35,7 +35,7 @@ Section mutex.
| _ => False end;
ty_shr κ tid l :=
∃ γ κ',
- &shr{κ, mutexN} (lock_proto γ l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗ κ ⊑ κ'
+ &at{κ, mutexN} (lock_proto γ l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗ κ ⊑ κ'
|}%I.
Next Obligation.
iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
@@ -71,7 +71,7 @@ Section mutex.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H".
iDestruct "H" as (γ κ'') "(#Hlck & #Hlft)".
- iExists _, _. iSplit; first by iApply shr_bor_shorten.
+ iExists _, _. iSplit; first by iApply at_bor_shorten.
iApply lft_incl_trans; done.
Qed.
@@ -100,7 +100,7 @@ Section mutex.
- iIntros "!# * Hvl". destruct vl as [|[[| |n]|]vl]; try done.
simpl. iDestruct "Hvl" as "[$ Hvl]". by iApply "Howni".
- iIntros "!# * Hshr". iDestruct "Hshr" as (γ κ') "[Hshr Hincl]".
- iExists _, _. iFrame "Hincl". iApply (shr_bor_iff with "[] Hshr"). iNext.
+ iExists _, _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
@@ -121,7 +121,7 @@ Section mutex.
Send ty → Sync (mutex ty).
Proof.
iIntros (???? l) "Hshr". iDestruct "Hshr" as (γ κ') "[Hshr Hincl]".
- iExists _, _. iFrame "Hincl". iApply (shr_bor_iff with "[] Hshr"). iNext.
+ iExists _, _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 17ac49c0..c0c68d79 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -35,7 +35,7 @@ Section mguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ γ β, locked γ ∗ α ⊑ β ∗
- &shr{α, mutexN} (lock_proto γ l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+ &at{α, mutexN} (lock_proto γ l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
&{β} (shift_loc l 1 ↦∗: ty.(ty_own) tid)
| _ => False end;
ty_shr κ tid l :=
@@ -99,8 +99,8 @@ Section mguard.
iDestruct "H" as (γ β) "(Hcl & #H⊑ & #Hinv & Hown)".
iExists γ, β. iFrame. iSplit; last iSplit.
+ by iApply lft_incl_trans.
- + iApply (shr_bor_shorten with "Hα").
- iApply (shr_bor_iff with "[] Hinv"). iNext.
+ + iApply (at_bor_shorten with "Hα").
+ iApply (at_bor_iff with "[] Hinv"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
@@ -139,12 +139,12 @@ Section code.
Lemma mutex_acc E γ l ty tid q α κ :
↑lftN ⊆ E → ↑mutexN ⊆ E →
let R := (&{κ} shift_loc l 1 ↦∗: ty_own ty tid)%I in
- lft_ctx -∗ &shr{α,mutexN} lock_proto γ l R -∗ α ⊑ κ -∗
+ lft_ctx -∗ &at{α,mutexN} lock_proto γ l R -∗ α ⊑ κ -∗
□ ((q).[α] ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ (q).[α])).
Proof.
(* FIXME: This should work: iIntros (?? R). *) intros ?? R.
iIntros "#LFT #Hshr #Hlincl !# Htok".
- iMod (shr_bor_acc_tok with "LFT Hshr Htok") as "[Hproto Hclose1]"; [done..|].
+ iMod (at_bor_acc_tok with "LFT Hshr Htok") as "[Hproto Hclose1]"; [done..|].
iMod (fupd_intro_mask') as "Hclose2"; last iModIntro; first solve_ndisj.
iFrame. iIntros "Hproto". iMod "Hclose2" as "_".
iMod ("Hclose1" with "Hproto") as "$". done.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index fd500488..7b68f992 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
From iris.base_logic Require Import big_op fractional.
-From lrust.lifetime Require Import shr_borrow.
+From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
Set Default Proof Using "Type".
@@ -100,7 +100,7 @@ Section rwlock.
| #(LitInt z) :: vl' => ⌜-1 ≤ z⌠∗ ty.(ty_own) tid vl'
| _ => False
end%I;
- ty_shr κ tid l := (∃ α γ, κ ⊑ α ∗ &shr{α,rwlockN}(rwlock_inv tid l γ α ty))%I |}.
+ ty_shr κ tid l := (∃ α γ, κ ⊑ α ∗ &at{α,rwlockN}(rwlock_inv tid l γ α ty))%I |}.
Next Obligation.
iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
iIntros "[_ %] !% /=". congruence.
@@ -177,7 +177,7 @@ Section rwlock.
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
- iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
- iApply shr_bor_iff; last done. iSplit; iIntros "!>!# H".
+ iApply at_bor_iff; last done. iSplit; iIntros "!>!# H".
by iApply "Hty1ty2". by iApply "Hty2ty1".
Qed.
Lemma rwlock_mono' E L ty1 ty2 :
@@ -199,7 +199,7 @@ Section rwlock.
Send ty → Sync ty → Sync (rwlock ty).
Proof.
move=>???????/=. do 2 apply uPred.exist_mono=>?. apply uPred.sep_mono_r.
- iApply shr_bor_iff. iIntros "!> !#". iApply uPred.equiv_iff.
+ iApply at_bor_iff. iIntros "!> !#". iApply uPred.equiv_iff.
apply uPred.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
- do 5 f_equiv. apply uPred.equiv_spec; split; iApply send_change_tid.
- apply uPred.equiv_spec; split; iApply sync_change_tid.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 2fa0c52e..1df9e471 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -163,7 +163,7 @@ Section rwlock_functions.
[solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". done.
wp_bind (!ˢᶜ(LitV lx))%E.
- iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
+ iMod (at_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & INV)". wp_read.
iMod ("Hclose''" with "[Hlx INV]") as "Hβtok1"; first by iExists _; iFrame.
iModIntro. wp_let. wp_op=>Hm1; wp_if.
@@ -176,7 +176,7 @@ Section rwlock_functions.
[solve_typing..|]; first last.
simpl. iApply type_jump; solve_typing.
- wp_op. wp_bind (CAS _ _ _).
- iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
+ iMod (at_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
+ iApply (wp_cas_int_suc with "Hlx"); first done. iNext. iIntros "Hlx".
@@ -271,7 +271,7 @@ Section rwlock_functions.
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βtok Hclose']". done.
wp_bind (CAS _ _ _).
- iMod (shr_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
+ iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
- iApply (wp_cas_int_fail with "Hlx"). done. by destruct c as [|[[]]|].
iNext. iIntros "Hlx".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 74bee0c8..6bbcfe1d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -21,7 +21,7 @@ Section rwlockreadguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
- α ⊑ β ∗ &shr{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
+ α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
q.[ν] ∗ own γ (◯ reading_st q ν) ∗
(1.[ν] ={↑lftN,∅}▷=∗ [†ν])
| _ => False
@@ -91,7 +91,7 @@ Section rwlockreadguard.
+ iApply ty_shr_mono; last by iApply "Hs".
iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
- + iApply (shr_bor_iff with "[] Hinv").
+ + iApply (at_bor_iff with "[] Hinv").
iIntros "!> !#"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
iFrame. iApply ty_shr_mono; last by iApply "Hs".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 7267fbf5..a746c7a1 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -76,11 +76,11 @@ Section rwlockreadguard_functions.
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.
wp_bind (!ˢᶜ#lx')%E.
- iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
+ iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
iDestruct "INV" as (st) "[H↦ INV]". wp_read.
iMod ("Hcloseβ" with "[H↦ INV]") as "Hβ"; first by iExists _; iFrame.
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _).
- iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
+ iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
iDestruct "INV" as (st') "(Hlx & >Hâ— & Hst)".
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?].
+ iAssert (|={⊤ ∖ ↑rwlockN,⊤ ∖ ↑rwlockN ∖ ↑lftN}▷=>
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 22521426..fcad43ba 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -22,7 +22,7 @@ Section rwlockwriteguard.
match vl return _ with
| [ #(LitLoc l) ] =>
∃ γ β, &{β}(shift_loc l 1 ↦∗: ty.(ty_own) tid) ∗
- α ⊑ β ∗ &shr{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
+ α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
own γ (◯ writing_st)
| _ => False
end;
@@ -90,7 +90,7 @@ Section rwlockwriteguard.
iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
- + iApply shr_bor_iff; try done.
+ + iApply at_bor_iff; try done.
iIntros "!>!#"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 234c671e..27828ee3 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -123,7 +123,7 @@ Section rwlockwriteguard_functions.
[solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
wp_bind (#lx' <-ˢᶜ #0)%E.
- iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
+ iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
iDestruct "INV" as (st) "(H↦ & H◠& INV)". wp_write.
iMod ("Hcloseβ" with "[> H↦ H◠H◯ INV Hx']") as "Hβ".
{ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[[[=]| (? & st0 & [=<-] & -> &
--
GitLab