Commit 683b7066 authored by Ralf Jung's avatar Ralf Jung

rename thread-local invariants -> non-atomic invariants

parent 124a7d8d
Pipeline #3224 passed with stage
in 10 minutes and 55 seconds
......@@ -80,7 +80,7 @@ base_logic/lib/viewshifts.v
base_logic/lib/auth.v
base_logic/lib/sts.v
base_logic/lib/boxes.v
base_logic/lib/thread_local.v
base_logic/lib/na_invariants.v
base_logic/lib/cancelable_invariants.v
base_logic/lib/counter_examples.v
base_logic/lib/fractional.v
......
......@@ -3,55 +3,57 @@ From iris.algebra Require Export gmap gset coPset.
From iris.proofmode Require Import tactics.
Import uPred.
(* Non-atomic ("thread-local") invariants. *)
Definition thread_id := gname.
Class thread_localG Σ :=
Class na_invG Σ :=
tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
Section defs.
Context `{invG Σ, thread_localG Σ}.
Context `{invG Σ, na_invG Σ}.
Definition tl_own (tid : thread_id) (E : coPset) : iProp Σ :=
Definition na_own (tid : thread_id) (E : coPset) : iProp Σ :=
own tid (CoPset E, ).
Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
Definition na_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i N
inv N (P own tid (, GSet {[i]}) tl_own tid {[i]}))%I.
inv N (P own tid (, GSet {[i]}) na_own tid {[i]}))%I.
End defs.
Instance: Params (@tl_inv) 3.
Typeclasses Opaque tl_own tl_inv.
Instance: Params (@na_inv) 3.
Typeclasses Opaque na_own na_inv.
Section proofs.
Context `{invG Σ, thread_localG Σ}.
Context `{invG Σ, na_invG Σ}.
Global Instance tl_own_timeless tid E : TimelessP (tl_own tid E).
Proof. rewrite /tl_own; apply _. Qed.
Global Instance na_own_timeless tid E : TimelessP (na_own tid E).
Proof. rewrite /na_own; apply _. Qed.
Global Instance tl_inv_ne tid N n : Proper (dist n ==> dist n) (tl_inv tid N).
Proof. rewrite /tl_inv. solve_proper. Qed.
Global Instance tl_inv_proper tid N : Proper (() ==> ()) (tl_inv tid N).
Global Instance na_inv_ne tid N n : Proper (dist n ==> dist n) (na_inv tid N).
Proof. rewrite /na_inv. solve_proper. Qed.
Global Instance na_inv_proper tid N : Proper (() ==> ()) (na_inv tid N).
Proof. apply (ne_proper _). Qed.
Global Instance tl_inv_persistent tid N P : PersistentP (tl_inv tid N P).
Proof. rewrite /tl_inv; apply _. Qed.
Global Instance na_inv_persistent tid N P : PersistentP (na_inv tid N P).
Proof. rewrite /na_inv; apply _. Qed.
Lemma tl_alloc : (|==> tid, tl_own tid )%I.
Lemma na_alloc : (|==> tid, na_own tid )%I.
Proof. by apply own_alloc. Qed.
Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 - tl_own tid E2 - E1 E2.
Lemma na_own_disjoint tid E1 E2 : na_own tid E1 - na_own tid E2 - E1 E2.
Proof.
apply wand_intro_r.
rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
Qed.
Lemma tl_own_union tid E1 E2 :
E1 E2 tl_own tid (E1 E2) ⊣⊢ tl_own tid E1 tl_own tid E2.
Lemma na_own_union tid E1 E2 :
E1 E2 na_own tid (E1 E2) ⊣⊢ na_own tid E1 na_own tid E2.
Proof.
intros ?. by rewrite /tl_own -own_op pair_op left_id coPset_disj_union.
intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
Qed.
Lemma tl_inv_alloc tid E N P : P ={E}= tl_inv tid N P.
Lemma na_inv_alloc tid E N P : P ={E}= na_inv tid N P.
Proof.
iIntros "HP".
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
......@@ -64,20 +66,20 @@ Section proofs.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
apply of_gset_finite. }
simpl. iDestruct "Hm" as %(<- & i & -> & ?).
rewrite /tl_inv.
rewrite /na_inv.
iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
iNext. iLeft. by iFrame.
Qed.
Lemma tl_inv_open tid E N P :
Lemma na_inv_open tid E N P :
N E
tl_inv tid N P - tl_own tid E ={E}= P tl_own tid (E∖↑N)
( P tl_own tid (E∖↑N) ={E}= tl_own tid E).
na_inv tid N P - na_own tid E ={E}= P na_own tid (E∖↑N)
( P na_own tid (E∖↑N) ={E}= na_own tid E).
Proof.
rewrite /tl_inv. iIntros (?) "#Htlinv Htoks".
rewrite /na_inv. iIntros (?) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% Hinv]".
rewrite [E as X in tl_own tid X](union_difference_L (N) E) //.
rewrite [X in (X _)](union_difference_L {[i]} (N)) ?tl_own_union; [|set_solver..].
rewrite [E as X in na_own tid X](union_difference_L (N) E) //.
rewrite [X in (X _)](union_difference_L {[i]} (N)) ?na_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
- iMod ("Hclose" with "[Htoki]") as "_"; first auto.
......@@ -86,6 +88,6 @@ Section proofs.
+ iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
set_solver.
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
- iDestruct (tl_own_disjoint with "Htoki Htoki2") as %?. set_solver.
- iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
Qed.
End proofs.
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