barrier_client.v 2.79 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.heap_lang.lib.barrier Require Import proof.
2 3
From iris.heap_lang Require Import par.
From iris.program_logic Require Import auth sts saved_prop hoare ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris.heap_lang Require Import proofmode.
Ralf Jung's avatar
Ralf Jung committed
5 6
Import uPred.

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

Section client.
17
  Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
Ralf Jung's avatar
Ralf Jung committed
18 19
  Local Notation iProp := (iPropG heap_lang Σ).

Robbert Krebbers's avatar
Robbert Krebbers committed
20
  Definition y_inv (q : Qp) (l : loc) : iProp :=
21
    ( f : val, l {q} f    n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
22

Robbert Krebbers's avatar
Robbert Krebbers committed
23
  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
24
  Proof.
25
    iDestruct 1 as {f} "[[Hl1 Hl2] #Hf]".
Robbert Krebbers's avatar
Robbert Krebbers committed
26
    iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
Ralf Jung's avatar
Ralf Jung committed
27 28 29
  Qed.

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

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

Section ClosedProofs.
62
  Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ].
63 64
  Notation iProp := (iPropG heap_lang Σ).

65
  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}.
66
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    iIntros "! Hσ".
68
    iPvs (heap_alloc (nroot .@ "Barrier") with "Hσ") as {h} "[#Hh _]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
    iApply (client_safe (nroot .@ "Barrier") (nroot .@ "Heap")); auto with ndisj.
70 71 72 73
  Qed.

  Print Assumptions client_safe_closed.
End ClosedProofs.