barrier_client.v 2.67 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
9
  λ: "b" "y", wait "b" ;; !"y" #n.
Definition client : expr :=
10
  let: "y" := ref #0 in
11
12
13
  let: "b" := newbarrier #() in
  ("y" <- (λ: "z", "z" + #42) ;; signal "b") ||
    (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 Σ} (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  recv N b (y_inv q y)  WP worker n #b #y {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
31
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
    iIntros "[#Hh Hrecv]". wp_lam. wp_let.
    wp_apply wait_spec; iFrame "Hrecv".
34
    iDestruct 1 as (f) "[Hy #Hf]".
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    wp_seq. wp_load.
36
    iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"].
Ralf Jung's avatar
Ralf Jung committed
37
38
  Qed.

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

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

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

  Print Assumptions client_safe_closed.
End ClosedProofs.