barrier.v 12.7 KB
Newer Older
1
From algebra Require Export upred_big_op.
2
From program_logic Require Export sts saved_prop.
3
From program_logic Require Import hoare.
4
From heap_lang Require Export derived heap wp_tactics notation.
Ralf Jung's avatar
Ralf Jung committed
5
Import uPred.
6
7
8

Definition newchan := (λ: "", ref '0)%L.
Definition signal := (λ: "x", "x" <- '1)%L.
9
Definition wait := (rec: "wait" "x" :=if: !"x" = '1 then '() else "wait" "x")%L.
10

11
12
13
(** The STS describing the main barrier protocol. Every state has an index-set
    associated with it. These indices are actually [gname], because we use them
    with saved propositions. *)
14
Module barrier_proto.
15
16
  Inductive phase := Low | High.
  Record stateT := State { state_phase : phase; state_I : gset gname }.
17
18
  Inductive token := Change (i : gname) | Send.

19
20
21
  Global Instance stateT_inhabited: Inhabited stateT.
  Proof. split. exact (State Low ). Qed.

22
  Definition change_tokens (I : gset gname) : set token :=
Ralf Jung's avatar
Ralf Jung committed
23
    mkSet (λ t, match t with Change i => i  I | Send => False end).
24

25
26
27
  Inductive trans : relation stateT :=
  | ChangeI p I2 I1 : trans (State p I1) (State p I2)
  | ChangePhase I : trans (State Low I) (State High I).
28

29
30
31
  Definition tok (s : stateT) : set token :=
      change_tokens (state_I s)
     match state_phase s with Low =>  | High => {[ Send ]} end.
32

Robbert Krebbers's avatar
Robbert Krebbers committed
33
  Canonical Structure sts := sts.STS trans tok.
34

35
  (* The set of states containing some particular i *)
36
37
38
39
  Definition i_states (i : gname) : set stateT :=
    mkSet (λ s, i  state_I s).

  Lemma i_states_closed i :
Robbert Krebbers's avatar
Robbert Krebbers committed
40
    sts.closed (i_states i) {[ Change i ]}.
41
42
  Proof.
    split.
43
    - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
Ralf Jung's avatar
Ralf Jung committed
44
45
46
47
48
      apply lookup_singleton.
    - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
      move=>s' /elem_of_intersection. rewrite !mkSet_elem_of /=.
      move=>[[Htok|Htok] ? ]; subst s'; first done.
      destruct p; done.
49
50
51
52
53
    - (* If we do the destruct of the states early, and then inversion
         on the proof of a transition, it doesn't work - we do not obtain
         the equalities we need. So we destruct the states late, because this
         means we can use "destruct" instead of "inversion". *)
      move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
Ralf Jung's avatar
Ralf Jung committed
54
55
      (* We probably want some helper lemmas for this... *)
      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
56
57
      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
      destruct Htrans; last done; move:Hs1 Hdisj Htok.
Ralf Jung's avatar
Ralf Jung committed
58
59
60
      rewrite /= /tok /=.
      intros. apply dec_stable. 
      assert (Change i  change_tokens I1) as HI1
61
        by (rewrite mkSet_not_elem_of; set_solver +Hs1).
Ralf Jung's avatar
Ralf Jung committed
62
63
      assert (Change i  change_tokens I2) as HI2.
      { destruct p.
64
65
        - set_solver +Htok Hdisj HI1.
        - set_solver +Htok Hdisj HI1 / discriminate. }
Ralf Jung's avatar
Ralf Jung committed
66
67
      done.
  Qed.
68
69
70
71

  (* The set of low states *)
  Definition low_states : set stateT :=
    mkSet (λ s, if state_phase s is Low then True else False).
72
73

  Lemma low_states_closed : sts.closed low_states {[ Send ]}.
74
75
76
77
  Proof.
    split.
    - apply (non_empty_inhabited(State Low )). by rewrite !mkSet_elem_of /=.
    - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
78
      destruct p; last done. set_solver.
79
80
81
82
83
    - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
      destruct Htrans; move:Hs1 Hdisj Htok =>/=;
                                first by destruct p.
84
      rewrite /= /tok /=. intros. set_solver +Hdisj Htok.
85
86
  Qed.

87
End barrier_proto.
88
89
90
91
92
93
(* I am too lazy to type the full module name all the time. But then
   why did we even put this into a module? Because some of the names 
   are so general.
   What we'd really like here is to import *some* of the names from
   the module into our namespaces. But Coq doesn't seem to support that...?? *)
Import barrier_proto.
94

95
96
97
(** Now we come to the Iris part of the proof. *)
Section proof.
  Context {Σ : iFunctorG} (N : namespace).
Ralf Jung's avatar
Ralf Jung committed
98
  Context `{heapG Σ} (heapN : namespace).
99
100
  Context `{stsG heap_lang Σ sts}.
  Context `{savedPropG heap_lang Σ}.
Ralf Jung's avatar
Ralf Jung committed
101

Ralf Jung's avatar
Ralf Jung committed
102
103
  Local Hint Immediate i_states_closed low_states_closed.

104
  Local Notation iProp := (iPropG heap_lang Σ).
105
106

  Definition waiting (P : iProp) (I : gset gname) : iProp :=
107
108
    ( Ψ : gname  iProp, (P - Π★{set I} (λ i, Ψ i)) 
                             Π★{set I} (λ i, saved_prop_own i (Ψ i)))%I.
109
110

  Definition ress (I : gset gname) : iProp :=
111
    (Π★{set I} (λ i,  R, saved_prop_own i R  R))%I.
112

113
114
  Local Notation state_to_val s :=
    (match s with State Low _ => 0 | State High _ => 1 end).
115
  Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
116
    (l  '(state_to_val s) 
117
118
     match s with State Low I' => waiting P I' | State High I' => ress I' end
    )%I.
119
120

  Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
Ralf Jung's avatar
Ralf Jung committed
121
    (heap_ctx heapN  sts_ctx γ N (barrier_inv l P))%I.
122

123
124
125
126
127
128
129
  Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
  Proof.
    move=>? ? EQ. rewrite /barrier_ctx. apply sep_ne; first done. apply sts_ctx_ne.
    move=>[p I]. rewrite /barrier_inv. destruct p; last done.
    rewrite /waiting. by setoid_rewrite EQ.
  Qed.

130
  Definition send (l : loc) (P : iProp) : iProp :=
131
    ( γ, barrier_ctx γ l P  sts_ownS γ low_states {[ Send ]})%I.
132

133
134
135
136
137
  Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
  Proof. (* TODO: This really ought to be doable by an automatic tactic. it is just application of already regostered congruence lemmas. *)
    move=>? ? EQ. rewrite /send. apply exist_ne=>γ. by rewrite EQ.
  Qed.

138
  Definition recv (l : loc) (R : iProp) : iProp :=
139
    ( γ P Q i, barrier_ctx γ l P  sts_ownS γ (i_states i) {[ Change i ]} 
140
141
        saved_prop_own i Q  (Q - R))%I.

142
143
144
145
146
  Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
  Proof.
    move=>? ? EQ. rewrite /send. do 4 apply exist_ne=>?. by rewrite EQ.
  Qed.

147
148
149
  Lemma newchan_spec (P : iProp) (Φ : val  iProp) :
    (heap_ctx heapN   l, recv l P  send l P - Φ (LocV l))
     wp  (newchan '()) Φ.
Ralf Jung's avatar
Ralf Jung committed
150
  Proof.
Ralf Jung's avatar
Ralf Jung committed
151
    rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
152
    rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj.
Ralf Jung's avatar
Ralf Jung committed
153
154
155
156
157
158
159
160
161
162
163
164
165
166
    apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
    rewrite !assoc. apply pvs_wand_r.
    (* The core of this proof: Allocating the STS and the saved prop. *)
    eapply sep_elim_True_r.
    { by eapply (saved_prop_alloc _ P). }
    rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
    apply exist_elim=>i.
    transitivity (pvs   (heap_ctx heapN   (barrier_inv l P (State Low {[ i ]}))   saved_prop_own i P)).
    - rewrite -pvs_intro. rewrite [(_  heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
      rewrite {1}[saved_prop_own _ _]always_sep_dup !assoc. apply sep_mono_l.
      rewrite /barrier_inv /waiting -later_intro. apply sep_mono_r.
      rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I ()%I).
      apply sep_mono.
      + rewrite -later_intro. apply wand_intro_l. rewrite right_id.
Ralf Jung's avatar
Ralf Jung committed
167
168
        by rewrite big_sepS_singleton.
      + by rewrite big_sepS_singleton.
Ralf Jung's avatar
Ralf Jung committed
169
    - rewrite (sts_alloc (barrier_inv l P)  N); last by eauto. rewrite !pvs_frame_r !pvs_frame_l. 
Ralf Jung's avatar
Ralf Jung committed
170
      rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l. apply exist_elim=>γ.
Ralf Jung's avatar
Ralf Jung committed
171
172
173
174
175
176
      (* TODO: The record notation is rather annoying here *)
      rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P).
      rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ).
      (* This is even more annoying than usually, since rewrite sometimes unfolds stuff... *)
      rewrite [barrier_ctx _ _ _]lock !assoc [(_  locked _)%I]comm !assoc -lock.
      rewrite -always_sep_dup.
Ralf Jung's avatar
Ralf Jung committed
177
178
179
180
181
182
183
      rewrite [barrier_ctx _ _ _]lock always_and_sep_l -!assoc assoc -lock.
      rewrite -pvs_frame_l. apply sep_mono_r.
      rewrite [(saved_prop_own _ _  _)%I]comm !assoc. rewrite -pvs_frame_r. apply sep_mono_l.
      rewrite -assoc [( _  _)%I]comm assoc -pvs_frame_r.
      eapply sep_elim_True_r; last eapply sep_mono_l.
      { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
      rewrite (sts_own_weaken  _ _ (i_states i  low_states) _ ({[ Change i ]}  {[ Send ]})).
Ralf Jung's avatar
Ralf Jung committed
184
      + apply pvs_mono. rewrite sts_ownS_op; eauto; []. set_solver.
Ralf Jung's avatar
Ralf Jung committed
185
186
      + rewrite /= /tok /=. apply elem_of_equiv=>t. rewrite elem_of_difference elem_of_union.
        rewrite !mkSet_elem_of /change_tokens.
187
        (* TODO: destruct t; set_solver does not work. What is the best way to do on? *)
Ralf Jung's avatar
Ralf Jung committed
188
189
        destruct t as [i'|]; last by naive_solver. split.
        * move=>[_ Hn]. left. destruct (decide (i = i')); first by subst i.
190
191
192
          exfalso. apply Hn. left. set_solver.
        * move=>[[EQ]|?]; last discriminate. set_solver. 
      + apply elem_of_intersection. rewrite !mkSet_elem_of /=. set_solver.
Ralf Jung's avatar
Ralf Jung committed
193
194
195
      + apply sts.closed_op; eauto; first set_solver; [].
        apply (non_empty_inhabited (State Low {[ i ]})). apply elem_of_intersection.
        rewrite !mkSet_elem_of /=. set_solver.
Ralf Jung's avatar
Ralf Jung committed
196
  Qed.
Ralf Jung's avatar
Ralf Jung committed
197

198
199
  Lemma signal_spec l P (Φ : val  iProp) :
    heapN  N  (send l P  P  Φ '())  wp  (signal (LocV l)) Φ.
Ralf Jung's avatar
Ralf Jung committed
200
  Proof.
201
    intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
Ralf Jung's avatar
Ralf Jung committed
202
203
    apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
    (* I think some evars here are better than repeating *everything* *)
204
205
    eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
      eauto with I ndisj.
206
    rewrite [(_  sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
Ralf Jung's avatar
Ralf Jung committed
207
208
209
    apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
    apply const_elim_sep_l=>Hs. destruct p; last done.
    rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
210
    eapply wp_store; eauto with I ndisj.
Ralf Jung's avatar
Ralf Jung committed
211
212
213
214
215
    rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono.
    { (* Is this really the best way to strip the later? *)
      erewrite later_sep. apply sep_mono_r. apply later_intro. }
    apply wand_intro_l. rewrite -(exist_intro (State High I)).
    rewrite -(exist_intro ). rewrite const_equiv /=; last first.
216
    { constructor; first constructor; rewrite /= /tok /=; set_solver. }
Ralf Jung's avatar
Ralf Jung committed
217
218
219
220
    rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
    rewrite !assoc [(_  P)%I]comm !assoc -2!assoc.
    apply sep_mono; last first.
    { apply wand_intro_l. eauto with I. }
Ralf Jung's avatar
Ralf Jung committed
221
    (* Now we come to the core of the proof: Updating from waiting to ress. *)
222
    rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Φ} Φ.
Ralf Jung's avatar
Ralf Jung committed
223
    rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
    rewrite big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
225
    rewrite -(exist_intro (Φ i)) comm. done.
Ralf Jung's avatar
Ralf Jung committed
226
  Qed.
Ralf Jung's avatar
Ralf Jung committed
227

228
229
  Lemma wait_spec l P (Φ : val  iProp) :
    heapN  N  (recv l P  (P - Φ '()))  wp  (wait (LocV l)) Φ.
Ralf Jung's avatar
Ralf Jung committed
230
231
232
  Proof.
  Abort.

233
234
  Lemma split_spec l P1 P2 Φ :
    (recv l (P1  P2)  (recv l P1  recv l P2 - Φ '()))  wp  Skip Φ.
Ralf Jung's avatar
Ralf Jung committed
235
236
237
238
239
240
  Proof.
  Abort.

  Lemma recv_strengthen l P1 P2 :
    (P1 - P2)  (recv l P1 - recv l P2).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
241
242
243
244
245
246
247
    apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
    rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r.
    apply exist_mono=>Q. rewrite sep_exist_r. apply exist_mono=>i.
    rewrite -!assoc. apply sep_mono_r, sep_mono_r, sep_mono_r, sep_mono_r.
    rewrite (later_intro (P1 - _)%I) -later_sep. apply later_mono.
    apply wand_intro_l. rewrite !assoc wand_elim_r wand_elim_r. done.
  Qed.
248
249

End proof.
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269

Section spec.
  Context {Σ : iFunctorG}.
  Context `{heapG Σ}.
  Context `{stsG heap_lang Σ barrier_proto.sts}.
  Context `{savedPropG heap_lang Σ}.

  Local Notation iProp := (iPropG heap_lang Σ).

  (* TODO: Maybe notation for LocV (and Loc)? *)
  Lemma barrier_spec (heapN N : namespace) :
    heapN  N 
     (recv send : loc -> iProp -n> iProp),
      ( P, heap_ctx heapN  ({{ True }} newchan '() @  {{ λ v,  l, v = LocV l  recv l P  send l P }})) 
      ( l P, {{ send l P  P }} signal (LocV l) @  {{ λ _, True }}) 
      ( l P, {{ recv l P }} wait (LocV l) @  {{ λ _, P }}) 
      ( l P Q, {{ recv l (P  Q) }} Skip @  {{ λ _, recv l P  recv l Q }}) 
      ( l P Q, (P - Q)  (recv l P - recv l Q)).
  Proof.
    intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)).
270
    split_and?; cbn.
271
272
273
274
275
276
277
278
279
280
281
    - intros. apply: always_intro. apply impl_intro_l. rewrite -newchan_spec.
      rewrite comm always_and_sep_r. apply sep_mono_r. apply forall_intro=>l.
      apply wand_intro_l. rewrite right_id -(exist_intro l) const_equiv // left_id.
      done.
    - intros. apply ht_alt. rewrite -signal_spec; first by rewrite right_id. done.
    - admit.
    - admit.
    - intros. apply recv_strengthen.
  Abort.

End spec.