thread_local.v 3.54 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
2
From iris.algebra Require Export gmap gset coPset.
3
From iris.proofmode Require Import tactics.
4 5
Import uPred.

6
Definition tlN : namespace := nroot .@ "tl".
7
Definition thread_id := gname.
8

9
Class thread_localG Σ :=
10
  tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
11 12

Section defs.
13
  Context `{invG Σ, thread_localG Σ}.
14

15
  Definition tl_own (tid : thread_id) (E : coPset) : iProp Σ :=
16
    own tid (CoPset E, ).
17 18

  Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
19
    ( i, i  nclose N 
20
          inv tlN (P  own tid (, GSet {[i]})  tl_own tid {[i]}))%I.
21 22
End defs.

23
Instance: Params (@tl_inv) 3.
24
Typeclasses Opaque tl_own tl_inv.
25 26

Section proofs.
27
  Context `{invG Σ, thread_localG Σ}.
28

29 30 31 32 33 34 35 36 37 38 39
  Global Instance tl_own_timeless tid E : TimelessP (tl_own tid E).
  Proof. rewrite /tl_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).
  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.

40
  Lemma tl_alloc : True ==  tid, tl_own tid .
41
  Proof. by apply own_alloc. Qed.
42

Ralf Jung's avatar
Ralf Jung committed
43
  Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1  tl_own tid E2  E1  E2.
44
  Proof.
45
    rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
46 47
  Qed.

48
  Lemma tl_own_union tid E1 E2 :
49
    E1  E2  tl_own tid (E1  E2)  tl_own tid E1  tl_own tid E2.
50
  Proof.
51
    intros ?. by rewrite /tl_own -own_op pair_op left_id coPset_disj_union.
52 53
  Qed.

54
  Lemma tl_inv_alloc tid E N P :  P ={E}= tl_inv tid N P.
55 56
  Proof.
    iIntros "HP".
57
    iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
58
    iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
59
    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
60
      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i  nclose N)).
61 62 63 64 65
      intros Ef. exists (coPpick (nclose N  coPset.of_gset Ef)).
      rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
      apply coPpick_elem_of=> Hfin.
      eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
      apply of_gset_finite. }
66
    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
67
    rewrite /tl_inv.
68
    iMod (inv_alloc tlN with "[-]"); last (iModIntro; iExists i; eauto).
69 70 71 72 73
    iNext. iLeft. by iFrame.
  Qed.

  Lemma tl_inv_open tid tlE E N P :
    nclose tlN  tlE  nclose N  E 
74 75
    tl_inv tid N P  tl_own tid E ={tlE}=  P  tl_own tid (E  N) 
                       ( P  tl_own tid (E  N) ={tlE}= tl_own tid E).
76
  Proof.
77 78
    rewrite /tl_inv. iIntros (??) "#Htlinv Htoks".
    iDestruct "Htlinv" as (i) "[% Hinv]".
79
    rewrite {1 4}(union_difference_L (nclose N) E) //.
80
    rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_own_union; [|set_solver..].
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
    iDestruct "Htoks" as "[[Htoki $] $]".
    iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose".
83 84
    - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
      iIntros "!> [HP $]".
85 86
      iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
      + iCombine "Hdis" "Hdis2" as "Hdis".
Robbert Krebbers's avatar
Tweak.  
Robbert Krebbers committed
87 88
        iDestruct (own_valid with "Hdis") as %[_ Hval%gset_disj_valid_op].
        set_solver.
89
      + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
90
    - iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame.
91 92
      set_solver.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
End proofs.