barrier_client.v 2.41 KB
Newer Older
1 2
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.heap_lang.lib.barrier Require Import proof.
4
From iris.heap_lang Require Import par.
5
From iris.heap_lang Require Import adequacy proofmode.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7

8
Definition worker (n : Z) : val :=
9 10
  λ: "b" "y", wait "b" ;; !"y" #n.
Definition client : expr :=
11
  let: "y" := ref #0 in
12
  let: "b" := newbarrier #() in
13 14
  ("y" <- (λ: "z", "z" + #42) ;; signal "b") |||
    (worker 12 "b" "y" ||| worker 17 "b" "y").
Ralf Jung's avatar
Ralf Jung committed
15 16

Section client.
17
  Set Default Proof Using "Type*".
18 19
  Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.

20
  Definition N := nroot .@ "barrier".
Ralf Jung's avatar
Ralf Jung committed
21

22
  Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
23
    ( f : val, l {q} f    n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
24

25
  Lemma y_inv_split q l : y_inv q l - (y_inv (q/2) l  y_inv (q/2) l).
Ralf Jung's avatar
Ralf Jung committed
26
  Proof.
27
    iDestruct 1 as (f) "[[Hl1 Hl2] #Hf]".
Robbert Krebbers's avatar
Robbert Krebbers committed
28
    iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
Ralf Jung's avatar
Ralf Jung committed
29 30 31
  Qed.

  Lemma worker_safe q (n : Z) (b y : loc) :
32
    recv N b (y_inv q y) - WP worker n #b #y {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
33
  Proof.
34
    iIntros "Hrecv". wp_lam. wp_let.
35
    wp_apply (wait_spec with "Hrecv"). iDestruct 1 as (f) "[Hy #Hf]".
Robbert Krebbers's avatar
Robbert Krebbers committed
36
    wp_seq. wp_load.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
    iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
Ralf Jung's avatar
Ralf Jung committed
38 39
  Qed.

40
  Lemma client_safe : WP client {{ _, True }}%I.
Ralf Jung's avatar
Ralf Jung committed
41
  Proof.
42 43
    iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
    wp_apply (newbarrier_spec N (y_inv 1 y)).
44
    iIntros (l) "[Hr Hs]". wp_let.
45
    iApply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
46
    - (* The original thread, the sender. *)
Ralf Jung's avatar
Ralf Jung committed
47 48
      wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
      iSplitR "Hy"; first by eauto.
49
      iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
50
    - (* The two spawned threads, the waiters. *)
51 52
      iDestruct (recv_weaken with "[] Hr") as "Hr".
      { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
53
      iMod (recv_split with "Hr") as "[H1 H2]"; first done.
54 55 56
      iApply (wp_par (λ _, True%I) (λ _, True%I) with "[H1] [H2]"); last auto.
      + by iApply worker_safe.
      + by iApply worker_safe.
57
Qed.
Ralf Jung's avatar
Ralf Jung committed
58
End client.
59

60 61
Section ClosedProofs.

62
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
63

64
Lemma client_adequate σ : adequate client σ (λ _, True).
65
Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
66

67
End ClosedProofs.
68 69

Print Assumptions client_adequate.