concurrent_runners.v 16.4 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
2
3
4
5
(** Concurrent Runner example from
    "Modular Reasoning about Separation of Concurrent Data Structures"
    <http://www.kasv.dk/articles/hocap-ext.pdf>
*)
From iris.heap_lang Require Import proofmode notation.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.bi.lib Require Import fractional.
Dan Frumin's avatar
Dan Frumin committed
7
From iris.algebra Require Import cmra agree frac csum excl.
8
From iris.heap_lang.lib Require Import assert.
9
From iris_examples.hocap Require Export abstract_bag shared_bag lib.oneshot.
Dan Frumin's avatar
Dan Frumin committed
10
11
Set Default Proof Using "Type".

12
13
14
15
16
(** RA describing the evolution of a task *)
(** INIT = task has been initiated
    SET_RES v = the result of the task has been computed and it is v
    FIN v = the task has been completed with the result v *)
(* We use this RA to verify the Task.run() method *)
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Definition saR := csumR fracR (csumR (prodR fracR (agreeR valO)) (agreeR valO)).
Dan Frumin's avatar
Dan Frumin committed
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
Class saG Σ := { sa_inG :> inG Σ saR }.
Definition INIT `{saG Σ} γ (q: Qp) := own γ (Cinl q%Qp).
Definition SET_RES `{saG Σ} γ (q: Qp) (v: val) := own γ (Cinr (Cinl (q%Qp, to_agree v))).
Definition FIN `{saG Σ} γ (v: val) := own γ (Cinr (Cinr (to_agree v))).
Global Instance INIT_fractional `{saG Σ} γ : Fractional (INIT γ)%I.
Proof.
  intros p q. rewrite /INIT.
  rewrite -own_op. f_equiv.
Qed.
Global Instance INIT_as_fractional `{saG Σ} γ q:
  AsFractional (INIT γ q) (INIT γ)%I q.
Proof.
  split; [done | apply _].
Qed.
Global Instance SET_RES_fractional `{saG Σ} γ v : Fractional (fun q => SET_RES γ q v)%I.
Proof.
  intros p q. rewrite /SET_RES.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  rewrite -own_op -Cinr_op -Cinl_op -pair_op agree_idemp. f_equiv.
Dan Frumin's avatar
Dan Frumin committed
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
Qed.
Global Instance SET_RES_as_fractional `{saG Σ} γ q v:
  AsFractional (SET_RES γ q v) (fun q => SET_RES γ q v)%I q.
Proof.
  split; [done | apply _].
Qed.

Lemma new_INIT `{saG Σ} : (|==>  γ, INIT γ 1%Qp)%I.
Proof. by apply own_alloc. Qed.
Lemma INIT_not_SET_RES `{saG Σ} γ q q' v :
  (INIT γ q - SET_RES γ q' v - False)%I.
Proof.
  iIntros "Hs Hp".
  iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma INIT_not_FIN `{saG Σ} γ q v :
  (INIT γ q - FIN γ v - False)%I.
Proof.
  iIntros "Hs Hp".
  iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma SET_RES_not_FIN `{saG Σ} γ q v v' :
  (SET_RES γ q v - FIN γ v' - False)%I.
Proof.
  iIntros "Hs Hp".
  iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma SET_RES_agree `{saG Σ} (γ: gname) (q q': Qp) (v w: val) :
  SET_RES γ q v - SET_RES γ q' w - v = w.
Proof.
  iIntros "Hs1 Hs2".
  iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  iPureIntro. rewrite -Cinr_op -Cinl_op -pair_op in Hfoo.
Dan Frumin's avatar
Dan Frumin committed
69
70
71
72
73
74
75
  by destruct Hfoo as [_ ?%agree_op_invL'].
Qed.
Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) :
  FIN γ v - FIN γ w - v = w.
Proof.
  iIntros "Hs1 Hs2".
  iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  iPureIntro. rewrite -Cinr_op -Cinr_op in Hfoo.
Dan Frumin's avatar
Dan Frumin committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
  by apply agree_op_invL'.
Qed.
Lemma INIT_SET_RES `{saG Σ} (v: val) γ :
  INIT γ 1%Qp == SET_RES γ 1%Qp v.
Proof.
  apply own_update.
  by apply cmra_update_exclusive.
Qed.
Lemma SET_RES_FIN `{saG Σ} (v w: val) γ :
  SET_RES γ 1%Qp v == FIN γ w.
Proof.
  apply own_update.
  by apply cmra_update_exclusive.
Qed.

Section contents.
  Context `{heapG Σ, !oneshotG Σ, !saG Σ}.
  Variable b : bag Σ.
  Variable N : namespace.

  (* new Task : Runner<A,B> -> A -> Task<A,B> *)
  Definition newTask : val := λ: "r" "a", ("r", "a", ref #0, ref NONEV).
  (* task_runner == Fst Fst Fst *)
  (* task_arg    == Snd Fst Fst *)
  (* task_state  == Snd Fst *)
  (* task_res    == Snd *)
  (* Task.Run : Task<A,B> -> () *)
  Definition task_Run : val := λ: "t",
    let: "runner" := Fst (Fst (Fst "t")) in
    let: "arg"    := Snd (Fst (Fst "t")) in
    let: "state"  := Snd (Fst "t") in
    let: "res"    := Snd "t" in
    let: "tmp" := (Fst "runner") "runner" "arg"
                  (* runner.body(runner,arg)*) in
    "res" <- (SOME "tmp");;
    "state" <- #1.

  (* Task.Join : Task<A,B> -> B *)
  Definition task_Join : val := rec: "join" "t" :=
    let: "runner" := Fst (Fst (Fst "t")) in
    let: "arg"    := Snd (Fst (Fst "t")) in
    let: "state"  := Snd (Fst "t") in
    let: "res"    := Snd "t" in
120
121
122
123
124
125
    if: (!"state" = #1)
    then match: !"res" with
           NONE => assert #false
         | SOME "v" => "v"
         end
    else "join" "t".
Dan Frumin's avatar
Dan Frumin committed
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164

  (* runner_body == Fst *)
  (* runner_bag  == Snd *)

  (* Runner.Fork : Runner<A,B> -> A -> Task<A,B> *)
  Definition runner_Fork : val := λ: "r" "a",
    let: "bag" := Snd "r" in
    let: "t" := newTask "r" "a" in
    pushBag b "bag" "t";;
    "t".

  (* Runner.runTask : Runner<A,B> -> () *)
  Definition runner_runTask : val := λ: "r",
    let: "bag" := Snd "r" in
    match: popBag b "bag" with
      NONE => #()
    | SOME "t" => task_Run "t"
    end.

  (* Runner.runTasks : Runner<A,B> -> () *)
  Definition runner_runTasks : val := rec: "runTasks" "r" :=
    runner_runTask "r";; "runTasks" "r".

  (* newRunner : (Runner<A,B> -> A -> B) -> nat -> Runner<A,B> *)
  Definition newRunner : val := λ: "body" "n",
    let: "bag" := newBag b #() in
    let: "r" := ("body", "bag") in
    let: "loop" :=
       (rec: "loop" "i" :=
          if: ("i" < "n")
          then Fork (runner_runTasks "r");; "loop" ("i"+#1)
          else "r"
       ) in
    "loop" #0.

  Definition task_inv (γ γ': gname) (state res: loc) (Q: val  iProp Σ) : iProp Σ :=
    ((state  #0  res  NONEV  pending γ (1/2)%Qp  INIT γ' (1/2)%Qp)
    ( v, state  #0  res  SOMEV v  pending γ (1/2)%Qp  SET_RES γ' (1/2)%Qp v)
    ( v, state  #1  res  SOMEV v  FIN γ' v  (Q v  pending γ (1/2)%Qp  shot γ v)))%I.
165
  Definition isTask (r: val) (γ γ': gname) (t: val) (P: val  iProp Σ) (Q: val  val  iProp Σ) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
166
167
168
    ( (arg : val) (state res : loc),
     t = (r, arg, #state, #res)%V
      P arg  INIT γ' (1/2)%Qp
169
170
171
      inv (N.@"task") (task_inv γ γ' state res (Q arg)))%I.
  Definition task (γ γ': gname) (t arg: val) (P: val  iProp Σ) (Q: val  val  iProp Σ) : iProp Σ :=
    ( (r: val) (state res : loc),
Dan Frumin's avatar
Dan Frumin committed
172
173
     t = (r, arg, #state, #res)%V
      pending γ (1/2)%Qp
174
      inv (N.@"task") (task_inv γ γ' state res (Q arg)))%I.
Dan Frumin's avatar
Dan Frumin committed
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190

  Ltac auto_equiv :=
    (* Deal with "pointwise_relation" *)
    repeat lazymatch goal with
           | |- pointwise_relation _ _ _ _ => intros ?
           end;
    (* Normalize away equalities. *)
    repeat match goal with
           | H : _ {_} _ |-  _ => apply (discrete_iff _ _) in H
           | _ => progress simplify_eq
           end;
    (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
    try (f_equiv; fast_done || auto_equiv).

  Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).

Dan Frumin's avatar
Dan Frumin committed
191
  Program Definition pre_runner (γ : name Σ b) (P: val  iProp Σ) (Q: val  val  iProp Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
192
    (valO -n> iPropO Σ) -n> (valO -n> iPropO Σ) := λne R r,
Dan Frumin's avatar
Dan Frumin committed
193
194
    ( (body bag : val), r = (body, bag)%V
      bagS b (N.@"bag") (λ x y,  γ γ', isTask (body,x) γ γ' y P Q) γ bag
195
        r a: val,  (R r  P a - WP body r a {{ v, Q a v }}))%I.
Dan Frumin's avatar
Dan Frumin committed
196
197
  Solve Obligations with solve_proper.

Dan Frumin's avatar
Dan Frumin committed
198
199
200
  Global Instance pre_runner_contractive (γ : name Σ b) P Q :
    Contractive (pre_runner γ P Q).
  Proof. unfold pre_runner. solve_contractive. Qed.
Dan Frumin's avatar
Dan Frumin committed
201

Dan Frumin's avatar
Dan Frumin committed
202
  Definition runner (γ: name Σ b) (P: val  iProp Σ) (Q: val  val  iProp Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
203
    valO -n> iPropO Σ :=
Dan Frumin's avatar
Dan Frumin committed
204
    (fixpoint (pre_runner γ P Q))%I.
Dan Frumin's avatar
Dan Frumin committed
205

Dan Frumin's avatar
Dan Frumin committed
206
207
  Lemma runner_unfold γ r P Q :
    runner γ P Q r 
Dan Frumin's avatar
Dan Frumin committed
208
209
      ( (body bag : val), r = (body, bag)%V
        bagS b (N.@"bag") (λ x y,  γ γ', isTask (body,x) γ γ' y P Q) γ bag
Dan Frumin's avatar
Dan Frumin committed
210
          r a: val,  (runner γ P Q r  P a - WP body r a {{ v, Q a v }}))%I.
Ralf Jung's avatar
Ralf Jung committed
211
  Proof. rewrite /runner. by rewrite {1}(fixpoint_unfold (pre_runner _ _ _) r). Qed.
Dan Frumin's avatar
Dan Frumin committed
212

Dan Frumin's avatar
Dan Frumin committed
213
214
  Global Instance runner_persistent γ r P Q :
    Persistent (runner γ P Q r).
Ralf Jung's avatar
Ralf Jung committed
215
  Proof. rewrite /runner (fixpoint_unfold (pre_runner _ _ _) r). apply _. Qed.
Dan Frumin's avatar
Dan Frumin committed
216

217
  Lemma newTask_spec γb (r a : val) P (Q : val  val  iProp Σ) :
Dan Frumin's avatar
Dan Frumin committed
218
    {{{ runner γb P Q r  P a }}}
Dan Frumin's avatar
Dan Frumin committed
219
      newTask r a
220
    {{{ γ γ' t, RET t; isTask r γ γ' t P Q  task γ γ' t a P Q }}}.
Dan Frumin's avatar
Dan Frumin committed
221
222
  Proof.
    iIntros (Φ) "[#Hrunner HP] HΦ".
223
    wp_rec. wp_pures. iApply wp_fupd.
Dan Frumin's avatar
Dan Frumin committed
224
    wp_alloc res as "Hres".
Robbert Krebbers's avatar
Robbert Krebbers committed
225
    wp_alloc status as "Hstatus".
Dan Frumin's avatar
Dan Frumin committed
226
227
    iMod (new_pending) as (γ) "[Htoken Htask]".
    iMod (new_INIT) as (γ') "[Hinit Hinit']".
228
    iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
Dan Frumin's avatar
Dan Frumin committed
229
    { iNext. iLeft. iFrame. }
230
    wp_pures. iModIntro. iApply "HΦ".
231
    iFrame. iSplitL; iExists _,_,_; iFrame "Hinv"; eauto.
Dan Frumin's avatar
Dan Frumin committed
232
233
  Qed.

234
  Lemma task_Join_spec γb γ γ' (r t a : val) P Q :
Dan Frumin's avatar
Dan Frumin committed
235
    {{{ runner γb P Q r  task γ γ' t a P Q }}}
236
       task_Join t
237
    {{{ res, RET res; Q a res }}}.
Dan Frumin's avatar
Dan Frumin committed
238
  Proof.
239
    iIntros (Φ) "[#Hrunner Htask] HΦ".
Dan Frumin's avatar
Dan Frumin committed
240
241
    iLöb as "IH".
    rewrite {2}/task_Join.
242
    iDestruct "Htask" as (r' state res) "(% & Htoken & #Htask)". simplify_eq.
243
    wp_rec. wp_pures.
244
    wp_bind (! #state)%E. iInv (N.@"task") as "Hstatus" "Hcl".
Dan Frumin's avatar
Dan Frumin committed
245
    rewrite {2}/task_inv.
246
    iDestruct "Hstatus" as "[>(Hstate & Hres)|[Hstatus|Hstatus]]".
Dan Frumin's avatar
Dan Frumin committed
247
248
249
250
251
    - wp_load.
      iMod ("Hcl" with "[Hstate Hres]") as "_".
      { iNext; iLeft; iFrame. }
      iModIntro. wp_op. wp_if.
      rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
252
253
      iExists _,_,_; iFrame "Htask"; eauto.
    - iDestruct "Hstatus" as (v) "(>Hstate & >Hres & HQ)".
Dan Frumin's avatar
Dan Frumin committed
254
255
256
257
258
      wp_load.
      iMod ("Hcl" with "[Hstate Hres HQ]") as "_".
      { iNext; iRight; iLeft. iExists _; iFrame. }
      iModIntro. wp_op. wp_if.
      rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
259
260
      iExists _,_,_; iFrame "Htask"; eauto.
    - iDestruct "Hstatus" as (v) "(>Hstate & >Hres & #HFIN & HQ)".
Dan Frumin's avatar
Dan Frumin committed
261
262
263
264
265
266
267
268
269
270
      wp_load.
      iDestruct "HQ" as "[[HQ Htoken2]|Hshot]"; last first.
      { iExFalso. iApply (shot_not_pending with "Hshot Htoken"). }
      iMod (shoot v γ with "[Htoken Htoken2]") as "#Hshot".
      { iApply (fractional_split_2 with "Htoken Htoken2").
        assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
        apply _. }
      iMod ("Hcl" with "[Hstate Hres]") as "_".
      { iNext. iRight. iRight. iExists _. iFrame. iFrame "HFIN".
        iRight. eauto. }
271
272
      iModIntro. wp_op. wp_if. wp_bind (!#res)%E.
      iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT)|[Hstatus|Hstatus]]" "Hcl".
Dan Frumin's avatar
Dan Frumin committed
273
      { iExFalso. iApply (shot_not_pending with "Hshot Hpending"). }
274
      { iDestruct "Hstatus" as (v') "(Hstate & Hres & Hpending & >HSETRES)".
Dan Frumin's avatar
Dan Frumin committed
275
276
        iExFalso. iApply (SET_RES_not_FIN with "HSETRES HFIN"). }
      iDestruct "Hstatus" as (v') "(Hstate & Hres & _ & HQ')".
277
278
279
280
      iDestruct "HQ'" as "[[? >Hpending]|>Hshot']".
      { iExFalso. iApply (shot_not_pending with "Hshot Hpending"). }
      iDestruct (shot_agree with "Hshot Hshot'") as %->.
      wp_load.
Dan Frumin's avatar
Dan Frumin committed
281
282
      iMod ("Hcl" with "[Hres Hstate]") as "_".
      { iNext. iRight. iRight. iExists _; iFrame. iFrame "HFIN". by iRight. }
283
      iModIntro. wp_match. iApply "HΦ"; eauto.
Dan Frumin's avatar
Dan Frumin committed
284
285
  Qed.

286
  Lemma task_Run_spec γb γ γ' r t P Q :
Dan Frumin's avatar
Dan Frumin committed
287
    {{{ runner γb P Q r  isTask r γ γ' t P Q }}}
Dan Frumin's avatar
Dan Frumin committed
288
289
290
291
       task_Run t
    {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "[#Hrunner Htask] HΦ".
Dan Frumin's avatar
Dan Frumin committed
292
    rewrite runner_unfold.
Dan Frumin's avatar
Dan Frumin committed
293
294
295
    iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)".
    iDestruct "Htask" as (arg state res) "(% & HP & HINIT & #Htask)".
    simplify_eq. rewrite /task_Run.
296
    wp_rec. wp_pures.
Dan Frumin's avatar
Dan Frumin committed
297
298
299
    wp_bind (body _ arg).
    iDestruct ("Hbody" $! (PairV body bag) arg) as "Hbody'".
    iSpecialize ("Hbody'" with "[HP]").
Dan Frumin's avatar
Dan Frumin committed
300
    { iFrame. rewrite runner_unfold.
Dan Frumin's avatar
Dan Frumin committed
301
302
303
      iExists _,_; iSplitR; eauto. }
    iApply (wp_wand with "Hbody'").
    iIntros (v) "HQ". wp_let.
304
    wp_bind (#res <- SOME v)%E. wp_inj.
305
    iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT')|[Hstatus|Hstatus]]" "Hcl".
Dan Frumin's avatar
Dan Frumin committed
306
307
308
309
310
311
312
    - wp_store.
      iMod (INIT_SET_RES v γ' with "[HINIT HINIT']") as "[HSETRES HSETRES']".
      { iApply (fractional_split_2 with "HINIT HINIT'").
        assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
        apply _. }
      iMod ("Hcl" with "[HSETRES Hstate Hres Hpending]") as "_".
      { iNext. iRight. iLeft. iExists _; iFrame. }
313
      iModIntro. wp_seq.
314
      iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT')|[Hstatus|Hstatus]]" "Hcl".
Dan Frumin's avatar
Dan Frumin committed
315
316
317
318
319
320
321
322
323
324
325
      { iExFalso. iApply (INIT_not_SET_RES with "HINIT' HSETRES'"). }
      + iDestruct "Hstatus" as (v') "(Hstate & Hres & Hpending & HSETRES)".
        wp_store.
        iDestruct (SET_RES_agree with "HSETRES HSETRES'") as %->.
        iMod (SET_RES_FIN v v with "[HSETRES HSETRES']") as "#HFIN".
        { iApply (fractional_split_2 with "HSETRES HSETRES'").
          assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp_div_2.
          apply _. }
        iMod ("Hcl" with "[-HΦ]") as "_".
        { iNext. do 2 iRight. iExists _; iFrame. iFrame "HFIN". iLeft. iFrame.  }
        iModIntro. by iApply "HΦ".
326
      + iDestruct "Hstatus" as (v') "(Hstate & Hres & >HFIN & HQ')".
Dan Frumin's avatar
Dan Frumin committed
327
        iExFalso. iApply (SET_RES_not_FIN with "HSETRES' HFIN").
328
    - iDestruct "Hstatus" as (v') "(Hstate & Hres & Hpending & >HSETRES)".
Dan Frumin's avatar
Dan Frumin committed
329
      iExFalso. iApply (INIT_not_SET_RES with "HINIT HSETRES").
330
    - iDestruct "Hstatus" as (v') "(Hstate & Hres & >HFIN & HQ')".
Dan Frumin's avatar
Dan Frumin committed
331
332
333
      iExFalso. iApply (INIT_not_FIN with "HINIT HFIN").
  Qed.

334
  Lemma runner_runTask_spec γb P Q r:
Dan Frumin's avatar
Dan Frumin committed
335
    {{{ runner γb P Q r }}}
Dan Frumin's avatar
Dan Frumin committed
336
337
338
339
      runner_runTask r
    {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "#Hrunner HΦ".
Dan Frumin's avatar
Dan Frumin committed
340
    rewrite runner_unfold /runner_runTask.
Dan Frumin's avatar
Dan Frumin committed
341
    iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)"; simplify_eq.
342
    wp_rec. wp_pures.
Dan Frumin's avatar
Dan Frumin committed
343
344
345
346
347
348
349
350
    wp_bind (popBag b _).
    iApply (popBag_spec with "Hbag").
    iNext. iIntros (t') "[_ [%|Ht]]"; simplify_eq.
    - wp_match. by iApply "HΦ".
    - iDestruct "Ht" as (t) "[% Ht]".
      iDestruct "Ht" as (γ γ') "Htask".
      simplify_eq. wp_match.
      iApply (task_Run_spec with "[Hbag Hbody Htask]"); last done.
Dan Frumin's avatar
Dan Frumin committed
351
      iFrame "Htask". rewrite runner_unfold.
Dan Frumin's avatar
Dan Frumin committed
352
353
354
      iExists _,_; iSplit; eauto.
  Qed.

355
  Lemma runner_runTasks_spec γb P Q r:
Dan Frumin's avatar
Dan Frumin committed
356
    {{{ runner γb P Q r }}}
Dan Frumin's avatar
Dan Frumin committed
357
358
359
360
361
362
363
      runner_runTasks r
    {{{ RET #(); False }}}.
  Proof.
    iIntros (Φ) "#Hrunner HΦ".
    iLöb as "IH". rewrite /runner_runTasks.
    wp_rec. wp_bind (runner_runTask r).
    iApply runner_runTask_spec; eauto.
364
    iNext. iIntros "_". wp_seq. by iApply "IH".
Dan Frumin's avatar
Dan Frumin committed
365
366
  Qed.

367
  Lemma loop_spec (n i : nat) P Q γb r:
Dan Frumin's avatar
Dan Frumin committed
368
    {{{ runner γb P Q r }}}
369
      (RecV "loop" "i" (
Dan Frumin's avatar
Dan Frumin committed
370
371
         if: "i" < #n
         then Fork (runner_runTasks r);; "loop" ("i" + #1)
372
         else r)) #i
Dan Frumin's avatar
Dan Frumin committed
373
    {{{ r, RET r; runner γb P Q r }}}.
Dan Frumin's avatar
Dan Frumin committed
374
375
376
377
378
  Proof.
    iIntros (Φ) "#Hrunner HΦ".
    iLöb as "IH" forall (i).
    wp_rec. wp_op. case_bool_decide; wp_if; last first.
    { by iApply "HΦ". }
Robbert Krebbers's avatar
Robbert Krebbers committed
379
380
    wp_bind (Fork _). iApply (wp_fork with "[]").
    - iNext. by iApply runner_runTasks_spec.
381
    - iNext. wp_seq. wp_op.
Dan Frumin's avatar
Dan Frumin committed
382
383
384
385
386
      (* Set Printing Coercions. *)
      assert ((Z.of_nat i + 1) = Z.of_nat (i + 1)) as -> by lia.
      iApply ("IH" with "HΦ").
  Qed.

387
  Lemma newRunner_spec P Q (f : val) (n : nat) :
Dan Frumin's avatar
Dan Frumin committed
388
    {{{  (γ: name Σ b) (r: val),
Dan Frumin's avatar
Dan Frumin committed
389
            a: val, (runner γ P Q r  P a - WP f r a {{ v, Q a v }}) }}}
390
       newRunner f #n
Dan Frumin's avatar
Dan Frumin committed
391
    {{{ γb r, RET r; runner γb P Q r }}}.
Dan Frumin's avatar
Dan Frumin committed
392
  Proof.
393
    iIntros (Φ) "#Hf HΦ".
Dan Frumin's avatar
Dan Frumin committed
394
    unfold newRunner. iApply wp_fupd.
395
    wp_lam. wp_pures.
Dan Frumin's avatar
Dan Frumin committed
396
397
398
    wp_bind (newBag b #()).
    iApply (newBag_spec b (N.@"bag") (λ x y,  γ γ', isTask (f,x) γ γ' y P Q)%I); auto.
    iNext. iIntros (bag). iDestruct 1 as (γb) "#Hbag".
399
    wp_let. wp_pair. wp_let. wp_closure. wp_let.
Dan Frumin's avatar
Dan Frumin committed
400
401
    iAssert (runner γb P Q (PairV f bag))%I with "[]" as "#Hrunner".
    { rewrite runner_unfold. iExists _,_. iSplit; eauto. }
Dan Frumin's avatar
Dan Frumin committed
402
403
404
405
    iApply (loop_spec n 0 with "Hrunner [HΦ]"); eauto.
    iNext. iIntros (r) "Hr". by iApply "HΦ".
  Qed.

406
  Lemma runner_Fork_spec γb (r a:val) P Q :
Dan Frumin's avatar
Dan Frumin committed
407
    {{{ runner γb P Q r  P a }}}
408
       runner_Fork r a
409
    {{{ γ γ' t, RET t; task γ γ' t a P Q }}}.
Dan Frumin's avatar
Dan Frumin committed
410
  Proof.
411
    iIntros (Φ) "[#Hrunner HP] HΦ".
Dan Frumin's avatar
Dan Frumin committed
412
    rewrite /runner_Fork runner_unfold.
Dan Frumin's avatar
Dan Frumin committed
413
414
    iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)". simplify_eq.
    Local Opaque newTask.
415
    wp_lam. wp_pures. wp_bind (newTask _ _).
416
    iApply (newTask_spec γb (body,bag) a P Q with "[Hbag Hbody HP]").
Dan Frumin's avatar
Dan Frumin committed
417
    { iFrame "HP". rewrite runner_unfold.
Dan Frumin's avatar
Dan Frumin committed
418
419
420
421
      iExists _,_; iSplit; eauto. }
    iNext. iIntros (γ γ' t) "[Htask Htask']". wp_let.
    wp_bind (pushBag _ _ _).
    iApply (pushBag_spec with "[$Hbag Htask]"); eauto.
422
    iNext. iIntros "_". wp_seq. by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
423
424
  Qed.
End contents.
425

Dan Frumin's avatar
Dan Frumin committed
426
Opaque runner task newRunner runner_Fork task_Join.