Commit 1db37236 authored by Ralf Jung's avatar Ralf Jung

thread_id -> na_inv_pool_name

parent 46f8eed8
......@@ -5,7 +5,7 @@ Import uPred.
(* Non-atomic ("thread-local") invariants. *)
Definition thread_id := gname.
Definition na_inv_pool_name := gname.
Class na_invG Σ :=
tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
......@@ -13,12 +13,12 @@ Class na_invG Σ :=
Section defs.
Context `{invG Σ, na_invG Σ}.
Definition na_own (tid : thread_id) (E : coPset) : iProp Σ :=
own tid (CoPset E, ).
Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
own p (CoPset E, ).
Definition na_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i N
inv N (P own tid (, GSet {[i]}) na_own tid {[i]}))%I.
inv N (P own p (, GSet {[i]}) na_own p {[i]}))%I.
End defs.
Instance: Params (@na_inv) 3.
......@@ -27,36 +27,36 @@ Typeclasses Opaque na_own na_inv.
Section proofs.
Context `{invG Σ, na_invG Σ}.
Global Instance na_own_timeless tid E : TimelessP (na_own tid E).
Global Instance na_own_timeless p E : TimelessP (na_own p E).
Proof. rewrite /na_own; apply _. Qed.
Global Instance na_inv_ne tid N n : Proper (dist n ==> dist n) (na_inv tid N).
Global Instance na_inv_ne p N n : Proper (dist n ==> dist n) (na_inv p N).
Proof. rewrite /na_inv. solve_proper. Qed.
Global Instance na_inv_proper tid N : Proper (() ==> ()) (na_inv tid N).
Global Instance na_inv_proper p N : Proper (() ==> ()) (na_inv p N).
Proof. apply (ne_proper _). Qed.
Global Instance na_inv_persistent tid N P : PersistentP (na_inv tid N P).
Global Instance na_inv_persistent p N P : PersistentP (na_inv p N P).
Proof. rewrite /na_inv; apply _. Qed.
Lemma na_alloc : (|==> tid, na_own tid )%I.
Lemma na_alloc : (|==> p, na_own p )%I.
Proof. by apply own_alloc. Qed.
Lemma na_own_disjoint tid E1 E2 : na_own tid E1 - na_own tid E2 - E1 E2.
Lemma na_own_disjoint p E1 E2 : na_own p E1 - na_own p E2 - E1 E2.
Proof.
apply wand_intro_r.
rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
Qed.
Lemma na_own_union tid E1 E2 :
E1 E2 na_own tid (E1 E2) na_own tid E1 na_own tid E2.
Lemma na_own_union p E1 E2 :
E1 E2 na_own p (E1 E2) na_own p E1 na_own p E2.
Proof.
intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
Qed.
Lemma na_inv_alloc tid E N P : P ={E}= na_inv tid N P.
Lemma na_inv_alloc p E N P : P ={E}= na_inv p N P.
Proof.
iIntros "HP".
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i N)).
......@@ -71,14 +71,14 @@ Section proofs.
iNext. iLeft. by iFrame.
Qed.
Lemma na_inv_open tid E F N P :
Lemma na_inv_open p E F N P :
N E N F
na_inv tid N P - na_own tid F ={E}= P na_own tid (F∖↑N)
( P na_own tid (F∖↑N) ={E}= na_own tid F).
na_inv p N P - na_own p F ={E}= P na_own p (F∖↑N)
( P na_own p (F∖↑N) ={E}= na_own p F).
Proof.
rewrite /na_inv. iIntros (??) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% Hinv]".
rewrite [F as X in na_own tid X](union_difference_L (N) F) //.
rewrite [F as X in na_own p X](union_difference_L (N) F) //.
rewrite [X in (X _)](union_difference_L {[i]} (N)) ?na_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment