Commit e35004b0 authored by Robbert Krebbers's avatar Robbert Krebbers

Some thread_local tweaks.

parent be24297e
Pipeline #2624 passed with stage
in 8 minutes and 52 seconds
...@@ -26,15 +26,14 @@ Instance: Params (@tl_inv) 4. ...@@ -26,15 +26,14 @@ Instance: Params (@tl_inv) 4.
Section proofs. Section proofs.
Context `{irisG Λ Σ, thread_localG Σ}. Context `{irisG Λ Σ, thread_localG Σ}.
Lemma tid_alloc : Lemma tid_alloc : True =r=> tid, tl_tokens tid .
True =r=> tid, tl_tokens tid .
Proof. by apply own_alloc. Qed. Proof. by apply own_alloc. Qed.
Lemma tl_tokens_disj tid E1 E2 : Lemma tl_tokens_disj tid E1 E2 :
tl_tokens tid E1 tl_tokens tid E2 (E1 E2). tl_tokens tid E1 tl_tokens tid E2 (E1 E2).
Proof. Proof.
rewrite /tl_tokens -own_op own_valid -coPset_disj_valid_op discrete_valid. rewrite /tl_tokens -own_op own_valid -coPset_disj_valid_op discrete_valid.
by iIntros ([? _])"!%". by iIntros ([? _]).
Qed. Qed.
Lemma tl_tokens_union tid E1 E2 : Lemma tl_tokens_union tid E1 E2 :
...@@ -43,8 +42,7 @@ Section proofs. ...@@ -43,8 +42,7 @@ Section proofs.
intros ?. by rewrite /tl_tokens -own_op pair_op left_id coPset_disj_union. intros ?. by rewrite /tl_tokens -own_op pair_op left_id coPset_disj_union.
Qed. Qed.
Lemma tl_inv_alloc tid E N P : Lemma tl_inv_alloc tid E N P : P ={E}=> tl_inv tid N P.
P ={E}=> tl_inv tid N P.
Proof. Proof.
iIntros "HP". iIntros "HP".
iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty". iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
...@@ -70,17 +68,16 @@ Section proofs. ...@@ -70,17 +68,16 @@ Section proofs.
iDestruct "Htlinv" as (i) "[% #Hinv]". iDestruct "Htlinv" as (i) "[% #Hinv]".
rewrite {1 4}(union_difference_L (nclose N) E) //. rewrite {1 4}(union_difference_L (nclose N) E) //.
rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver. rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.
iDestruct "Htoks" as "[[Htoki Htoks0] Htoks1]". iFrame "Htoks0 Htoks1". iDestruct "Htoks" as "[[Htoki $] $]".
iInv tlN as "[[HP >Hdis]|>Htoki2]" "Hclose". iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose".
- iVs ("Hclose" with "[Htoki]") as "_". auto. iFrame. - iVs ("Hclose" with "[Htoki]") as "_"; first auto.
iIntros "!==>[HP ?]". iFrame. iIntros "!==>[HP $]".
iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose". iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
+ iCombine "Hdis" "Hdis2" as "Hdis". + iCombine "Hdis" "Hdis2" as "Hdis".
iDestruct (own_valid with "Hdis") as %[_ Hval]. revert Hval. iDestruct (own_valid with "Hdis") as %[_ Hval].
rewrite gset_disj_valid_op. set_solver. revert Hval. rewrite gset_disj_valid_op. set_solver.
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame. + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
- iDestruct (tl_tokens_disj tid {[i]} {[i]} with "[-]") as %?. by iFrame. - iDestruct (tl_tokens_disj tid {[i]} {[i]} with "[-]") as %?. by iFrame.
set_solver. set_solver.
Qed. Qed.
End proofs.
End proofs.
\ No newline at end of file
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