Commit 5ee92991 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove global mask from thread local invariants as suggested by Ralf.

parent d7ee81fd
...@@ -3,7 +3,6 @@ From iris.algebra Require Export gmap gset coPset. ...@@ -3,7 +3,6 @@ From iris.algebra Require Export gmap gset coPset.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
Definition tlN : namespace := nroot .@ "tl".
Definition thread_id := gname. Definition thread_id := gname.
Class thread_localG Σ := Class thread_localG Σ :=
...@@ -17,7 +16,7 @@ Section defs. ...@@ -17,7 +16,7 @@ Section defs.
Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ := Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i N ( i, i N
inv tlN (P own tid (, GSet {[i]}) tl_own tid {[i]}))%I. inv N (P own tid (, GSet {[i]}) tl_own tid {[i]}))%I.
End defs. End defs.
Instance: Params (@tl_inv) 3. Instance: Params (@tl_inv) 3.
...@@ -65,26 +64,25 @@ Section proofs. ...@@ -65,26 +64,25 @@ Section proofs.
apply of_gset_finite. } apply of_gset_finite. }
simpl. iDestruct "Hm" as %(<- & i & -> & ?). simpl. iDestruct "Hm" as %(<- & i & -> & ?).
rewrite /tl_inv. rewrite /tl_inv.
iMod (inv_alloc tlN with "[-]"); last (iModIntro; iExists i; eauto). iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
iNext. iLeft. by iFrame. iNext. iLeft. by iFrame.
Qed. Qed.
Lemma tl_inv_open tid tlE E N P : Lemma tl_inv_open tid E N P :
tlN tlE N E N E
tl_inv tid N P - tl_own tid E ={tlE}= P tl_own tid (E∖↑N) tl_inv tid N P - tl_own tid E ={E}= P tl_own tid (E∖↑N)
( P tl_own tid (E∖↑N) ={tlE}= tl_own tid E). ( P tl_own tid (E∖↑N) ={E}= tl_own tid E).
Proof. Proof.
rewrite /tl_inv. iIntros (??) "#Htlinv Htoks". rewrite /tl_inv. iIntros (?) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% Hinv]". iDestruct "Htlinv" as (i) "[% Hinv]".
rewrite {1 4}(union_difference_L (N) E) //. rewrite {1 8}(union_difference_L (N) E) //.
rewrite {1 5}(union_difference_L {[i]} (N)) ?tl_own_union; [|set_solver..]. rewrite {1 5}(union_difference_L {[i]} (N)) ?tl_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]". iDestruct "Htoks" as "[[Htoki $] $]".
iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose". iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
- iMod ("Hclose" with "[Htoki]") as "_"; first auto. - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
iIntros "!> [HP $]". iIntros "!> [HP $]".
iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose". iInv N as "[[_ >Hdis2]|>Hitok]" "Hclose".
+ iCombine "Hdis" "Hdis2" as "Hdis". + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
iDestruct (own_valid with "Hdis") as %[_ Hval%gset_disj_valid_op].
set_solver. set_solver.
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame. + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
- iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame. - iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame.
......
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