thread_local.v 3.61 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
From iris.algebra Require Export gmap gset coPset.
From iris.proofmode Require Import invariants tactics.
Import uPred.

Definition thread_id := positive.

Class thread_localG Σ := {
  tl_enabled_inG :> inG Σ (gmapUR thread_id coPset_disjR);
  tl_disabled_inG :> inG Σ (gmapUR thread_id (gset_disjR positive));
  tl_enabled_name : gname;
  tl_disabled_name : gname
}.

Definition tlN : namespace := nroot .@ "tl".

Section defs.
  Context `{irisG Λ Σ, thread_localG Σ}.

  Definition tl_tokens (tid : thread_id) (E : coPset) : iProp Σ :=
    own tl_enabled_name {[ tid := CoPset E ]}.

  Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
    ( i,  (i  nclose N) 
          inv tlN (P  own tl_disabled_name {[ tid := GSet {[i]} ]}
                    tl_tokens tid {[i]}))%I.
End defs.

Instance: Params (@tl_tokens) 2.
Instance: Params (@tl_inv) 4.

Section proofs.
  Context `{irisG Λ Σ, thread_localG Σ}.

  Lemma tid_alloc :
    True =r=>  tid, tl_tokens tid .
  Proof.
    iIntros.
    iVs (own_empty (A:=gmapUR thread_id coPset_disjR) tl_enabled_name) as "Hempty".
    iVs (own_updateP with "Hempty") as (m) "[Hm Hown]".
      by apply alloc_updateP' with (x:=CoPset ).
    iDestruct "Hm" as %(tid & -> & _). eauto.
  Qed.

  Lemma tl_tokens_disj tid E1 E2 :
    tl_tokens tid E1  tl_tokens tid E2   (E1  E2).
  Proof.
    by rewrite /tl_tokens -own_op op_singleton own_valid -coPset_disj_valid_op
               discrete_valid singleton_valid.
  Qed.

  Lemma tl_tokens_union tid E1 E2 :
    E1  E2  tl_tokens tid (E1  E2)  tl_tokens tid E1  tl_tokens tid E2.
  Proof.
    intros ?. by rewrite /tl_tokens -own_op op_singleton coPset_disj_union.
  Qed.

  Lemma tl_inv_alloc tid E N P :  P ={E}=> tl_inv tid N P.
  Proof.
    iIntros "HP".
    iVs (own_empty (A:=gmapUR thread_id (gset_disjR positive)) tl_disabled_name)
      as "Hempty".
    iVs (own_updateP with "Hempty") as (m) "[Hm Hown]".
    { eapply alloc_unit_singleton_updateP' with (u:=) (i:=tid). done. apply _.
      apply (gset_alloc_empty_updateP_strong' (λ i, i  nclose N)).
      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. }
    iDestruct "Hm" as %(? & -> & i & -> & ?).
    iVs (inv_alloc tlN with "[-]"). 2:iVsIntro; iExists i; eauto.
    iNext. iLeft. by iFrame.
  Qed.

  Lemma tl_inv_open tid tlE E N P :
    nclose tlN  tlE  nclose N  E 
    tl_inv tid N P  tl_tokens tid E ={tlE}=  P  tl_tokens tid (E  N) 
                       ( P  tl_tokens tid (E  N) ={tlE}= tl_tokens tid E).
  Proof.
    iIntros (??) "#Htlinv Htoks".
    iDestruct "Htlinv" as (i) "[% #Hinv]".
    rewrite {1 4}(union_difference_L (nclose N) E) //.
    rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.    
    iDestruct "Htoks" as "[[Htoki Htoks0] Htoks1]". iFrame "Htoks0 Htoks1".
    iInv tlN as "[[HP >Hdis]|>Htoki2]" "Hclose".
    - iVs ("Hclose" with "[Htoki]") as "_". auto. iFrame.
      iIntros "!==>[HP ?]". iFrame.
      iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
      + iCombine "Hdis" "Hdis2" as "Hdis".
        iDestruct (own_valid with "Hdis") as %Hval.
        revert Hval. rewrite op_singleton singleton_valid gset_disj_valid_op.
        set_solver.
      + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
    - iDestruct (tl_tokens_disj tid {[i]} {[i]} with "[-]") as %?. by iFrame.
      set_solver.
  Qed.

End proofs.