barrier.v 8.4 KB
Newer Older
1
2
From iris_automation.heap_lang Require Import stepping_tacs biabd_instances_heaplang.
From iris_automation.biabd Require Import biabd_local_updates.
3
From iris_automation.steps Require Import local_post.
4
5
From iris.heap_lang Require Import proofmode.
From iris.algebra Require Import frac_auth numbers excl.
6
From iris_automation.lib Require Import ticket_cmra frac_token.
7

8
9
Definition make_barrier : val := 
  λ: <>, ref #0.
10

11
12
13
Definition peek : val :=
  λ: "b", ! "b".

14
Definition sync_up_enter : val := rec: "sync_enter" "b" :=
15
  let: "z" := peek "b" in
16
  if: #0  "z" then
17
18
19
20
    if: CAS "b" "z" ("z" + #1) then 
      "z" 
    else 
      "sync_enter" "b"
21
22
23
  else "sync_enter" "b".

Definition sync_up_exit threads : val := rec: "sync_exit" "b" "v" :=
24
25
26
27
28
29
  let: "w" := 
    if: "v" = #0 then 
      #(Zpos threads) 
    else 
      "v" 
    in
30
  let: "z" := ! "b" in
31
32
33
  if: "z" = "w" then
      "b" <- "z" - #1
  else
34
    "sync_exit" "b" "v".
35
36
37
38
39

Definition sync_up threads : val := λ: "b",
  sync_up_exit threads "b" (sync_up_enter "b").

Definition sync_down_enter : val := rec: "sync_enter" "b" :=
40
  let: "z" := peek "b" in
41
  if: "z"  #0 then
42
43
44
45
46
47
    if: CAS "b" "z" ("z" - #1) then
     - "z" 
    else 
      "sync_enter" "b"
  else 
    "sync_enter" "b".
48
49

Definition sync_down_exit threads : val := rec: "sync_exit" "b" "v" :=
50
51
52
53
54
55
  let: "w" := 
    if: "v" = #0 then 
      #(Zneg threads) 
    else 
      -"v" 
    in
56
  let: "z" := ! "b" in
57
  if: "z" = "w" then 
58
    "b" <- "z" + #1
59
60
  else 
    "sync_exit" "b" "v".
61
62
63
64
65
66
67
68
69
70
71
72
73
74

Definition sync_down threads : val := λ: "b",
  sync_down_exit threads "b" (sync_down_enter "b").

Definition barrierUR := authUR $ optionUR $ exclR $ leibnizO Z.
Class barrierG Σ :=
  BarrierG { 
    barrier_ticketG :> inG Σ ticketUR;
    barrier_tokenG :> fracTokenG Σ;
    barrier_barrierG :> inG Σ barrierUR;
  }.
Definition barrierΣ : gFunctors :=
  #[GFunctor ticketUR; fracTokenΣ; GFunctor barrierUR].

75
76
Local Obligation Tactic := smash_verify_tac.

77
Global Program Instance subG_barrierΣ {Σ} : subG barrierΣ Σ  barrierG Σ.
78
79

Section proof.
80
  Context `{!heapGS Σ, !barrierG Σ} (P1 P2 : Qp  iProp Σ).
81
  Context `{!Fractional P1, !Fractional P2}.
82
83
  Let N := nroot .@ "barrier".
  Set Default Proof Using "heapGS0 barrierG0 P1 P2 Fractional0 Fractional1".
84
85
86
87
88
89

  Definition barrier_inv (threads : positive) γp1 γp2 γt γb (l : loc) : iProp Σ :=
     (z : Z), l  #z  own γt (CoPset $ tickets_geq (S (Z.abs_nat z)))  own γb ( Excl' z)  (
      (0  z%Z  (
          (z < Zpos threads%Z  token_counter P1 γp1 (Z.to_pos (Zpos threads - z))  no_tokens P2 γp2 1%Qp  own γt (CoPset $ ticket (Z.abs_nat z))  own γb ( Excl' z))
                 
90
          (z < Zpos threads%Z  no_tokens P1 γp1 1%Qp  token_counter P2 γp2 (Z.to_pos (Zpos threads - z))  (own γb ( Excl' z)  own γt (CoPset $ ticket (Z.abs_nat z)))  own γt (CoPset $ ticket 0))
91
                
92
          (z = Zpos threads  no_tokens P1 γp1 1%Qp  no_tokens P2 γp2 1%Qp  P1 1  (own γb ( Excl' z)  own γt (CoPset $ ticket 0))  own γt (CoPset $ ticket $ Pos.to_nat threads))))
93
94
95
96
         
      (z  0%Z  (
          (Zneg threads < z%Z  token_counter P2 γp2 (Z.to_pos (Zpos threads + z))  no_tokens P1 γp1 1%Qp  own γt (CoPset $ ticket (Z.abs_nat z))  own γb ( Excl' z))
                 
97
          (Zneg threads < z%Z  no_tokens P2 γp2 1%Qp  token_counter P1 γp1 (Z.to_pos (Zpos threads + z))  (own γb ( Excl' z)  own γt (CoPset $ ticket (Z.abs_nat z)))  own γt (CoPset $ ticket 0))
98
                
99
          (z = Zneg threads  no_tokens P1 γp1 1%Qp  no_tokens P2 γp2 1%Qp  P1 1  (own γb ( Excl' z)  own γt (CoPset $ ticket 0))  own γt (CoPset $ ticket (Pos.to_nat threads)))))).
100
101
102
103

  Definition is_barrier (threads : positive) γp1 γp2 γt γb (v : val) : iProp Σ :=
     (l : loc), v = #l   (P1 1 ={∖↑N}= P2 1)   (P2 1 ={∖↑N}= P1 1)  inv N (barrier_inv threads γp1 γp2 γt γb l).

104
105
  Program Instance p1p2fupd_atom : AtomAndConnective true (P1 1 ={∖↑N}= P2 1).
  Program Instance p2p1fupd_atom : AtomAndConnective true (P2 1 ={∖↑N}= P1 1).
106

Ike Mulder's avatar
Ike Mulder committed
107
108
  Ltac connective_as_atom_shortcut ::= biabd_step_atom_shortcut.

109
110
  Instance newbarrier_spec (threads : positive) :
    SPEC {{ P1 1   (P1 1 ={∖↑N}= P2 1)   (P2 1 ={∖↑N}= P1 1) }} 
111
      make_barrier #()
112
    {{ γp1 γp2 γt γb (v : val), RET v; is_barrier threads γp1 γp2 γt γb v  token_iter P1 (Pos.to_nat threads) γp1 }}.
113
  Proof.
114
115
    iStepsS.
    iLeft; iLeft.
Ike Mulder's avatar
Ike Mulder committed
116
    erewrite (right_id ); last iSolveTC.
117
    iStepsS.
Ike Mulder's avatar
Ike Mulder committed
118
  Qed.
119

120
121
122
123
124
  Program Instance peek_spec threads γp1 γp2 γt γb (v : val) :
    SPEC {{ is_barrier threads γp1 γp2 γt γb v }}
      peek v
    {{ (z : Z), RET #z; Zneg threads  z  Zpos threads%Z }}.

125
126
127
128
  Instance sync_up_enter_spec threads γp1 γp2 γt γb (v : val) :
    SPEC {{ is_barrier threads γp1 γp2 γt γb v  token P1 γp1 }}
      sync_up_enter v
    {{ (z : Z), RET #z; 0  z%Z  own γt (CoPset $ ticket (Z.to_nat z)) }}.
129
  Proof.
130
    iStepsS. iLöb as "IH".
131
    wp_lam. iStepsS; try iSmash. (* iSmash deals with failing CAS's *)
Ike Mulder's avatar
Ike Mulder committed
132
    - destruct (decide (x0 + 1 = Z.pos threads)%Z) as [Heq|Hneq]; iSmash.
133
    - destruct (decide (threads = xH)) as [Heq|Hneq]; iSmash.
134
135
  Qed.

136
  Instance sync_up_exit_spec threads γp1 γp2 γb γt (z : Z) (v : val) :
137
138
139
    SPEC {{ is_barrier threads γp1 γp2 γt γb v  0  z%Z  own γt (CoPset $ ticket $ Z.to_nat z) }}
      sync_up_exit threads v #z
    {{ RET #(); token P2 γp2 }}.
140
  Proof.
141
    iStepsS. iLöb as "IH".
142
    wp_lam. iStepsS; try iSmash.
Ike Mulder's avatar
Ike Mulder committed
143
    - destruct (decide (z = x2)) as [-> | Hneq]; iSmash.
144
    - iRevert "H4"; iSmash.
145
146
  Qed. 
  (* we need reverts in some places to detect extra inequalities: at some places we have 3 tickets and mergablepersist does not get all currently *)
147

148
  Global Program Instance sync_up_spec threads γp1 γp2 γt γb (v : val) :
149
150
151
152
153
154
155
156
    SPEC {{ is_barrier threads γp1 γp2 γt γb v  token P1 γp1 }}
      sync_up threads v
    {{ RET #(); token P2 γp2 }}.

  Instance sync_down_enter_spec threads γp1 γp2 γt γb (v : val) :
    SPEC {{ is_barrier threads γp1 γp2 γt γb v  token P2 γp2 }}
      sync_down_enter v
    {{ (z : Z), RET #z; 0  z%Z  own γt (CoPset $ ticket (Z.to_nat z)) }}.
157
  Proof.
158
    iStepsS. iLöb as "IH".
159
    wp_lam. iStepsS; try iSmash. (* iSmash deals with failing CAS's *)
Ike Mulder's avatar
Ike Mulder committed
160
161
    - destruct (decide (x0 - 1 = Z.neg threads)%Z) as [Heq|Hneq]; iSmash.
    - destruct (decide (x0 - 1 = Z.neg threads)%Z) as [Heq|Hneq]; iSmash.
162
163
164
165
166
167
  Qed.

  Instance sync_down_exit_spec threads γp1 γp2 γb γt (z : Z) (v : val) :
    SPEC {{ is_barrier threads γp1 γp2 γt γb v  0  z%Z  own γt (CoPset $ ticket $ Z.to_nat z) }}
      sync_down_exit threads v #z
    {{ RET #(); token P1 γp1 }}.
168
  Proof.
169
    iStepsS. iLöb as "IH".
170
    wp_lam. iStepsS; try iSmash.
Ike Mulder's avatar
Ike Mulder committed
171
    - destruct (decide (Z.opp z = x2)) as [<- | Hneq]; iSmash.
172
    - iRevert "H4"; iSmash.
173
174
  Qed.

175
  Global Program Instance sync_down_spec threads γp1 γp2 γt γb (v : val) :
176
177
178
179
180
181
    SPEC {{ is_barrier threads γp1 γp2 γt γb v  token P2 γp2 }}
      sync_down threads v
    {{ RET #(); token P1 γp1 }}.
End proof.


182
183
Section barrier_specs2. (* this is currently necessary since otherwise TC search will try to find fractionals :( *)
  Context `{!heapGS Σ, barrierG Σ}. 
184
185
  Context (P1 P2 : Qp  iProp Σ).

186
  Global Program Instance barrier_persistent_reuse threads γp1 γp2 γt γb (v : val) `{!Fractional P1, !Fractional P2} :
187
188
    Persistent (is_barrier P1 P2 threads γp1 γp2 γt γb v).

189
  Global Opaque is_barrier make_barrier sync_up sync_down.
190

191
  Global Instance sync_up_spec_frac_reuse threads γp1 γp2 γt γb (v : val) :
192
    SPEC HP1 HP2, {{ is_barrier P1 P2 (Fractional0 := HP1) (Fractional1 := HP2) threads γp1 γp2 γt γb v  token P1 γp1 }}
193
194
      sync_up threads v
    {{ RET #(); token P2 γp2 }}.
Ike Mulder's avatar
Ike Mulder committed
195
  Proof. do 3 iStepS. assert (H1 := sync_up_spec P1 P2). iStepsS. Qed.
196

197
  Global Instance sync_down_spec_frac_reuse threads γp1 γp2 γt γb (v : val) :
198
    SPEC HP1 HP2, {{ is_barrier P1 P2 (Fractional0 := HP1) (Fractional1 := HP2) threads γp1 γp2 γt γb v  token P2 γp2 }}
199
200
      sync_down threads v
    {{ RET #(); token P1 γp1 }}.
Ike Mulder's avatar
Ike Mulder committed
201
  Proof. do 3 iStepS. assert (H1 := sync_down_spec P1 P2). iStepsS. Qed.
202
End barrier_specs2.
203