client.v 2.78 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").
Ralf Jung's avatar
Ralf Jung committed
14
15

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

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

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

  Lemma worker_safe q (n : Z) (b y : loc) :
    (heap_ctx heapN  recv heapN N b (y_inv q y))
30
     WP worker n #b #y {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
31
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
34
35
36
    iIntros "[#Hh Hrecv]". wp_lam. wp_let.
    wp_apply wait_spec; iFrame "Hrecv".
    iIntros "Hy"; iDestruct "Hy" as {f} "[Hy #Hf]".
    wp_seq. wp_load.
    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 heapN  WP client {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
40
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
44
45
    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".
46
    - (* The original thread, the sender. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
      wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
      iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
49
    - (* The two spawned threads, the waiters. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
50
      iSplitL; [|by iIntros {_ _} "_ >"].
Robbert Krebbers's avatar
Robbert Krebbers committed
51
      iDestruct recv_weaken "[] Hr" as "Hr".
Robbert Krebbers's avatar
Robbert Krebbers committed
52
      { iIntros "Hy". by iApply y_inv_split "Hy". }
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
      iPvs recv_split "Hr" as "[H1 H2]"; first done.
      iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
      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
67
68
    iIntros "! Hσ".
    iPvs (heap_alloc (nroot .@ "Barrier")) "Hσ" as {h} "[#Hh _]"; first done.
    iApply (client_safe (nroot .@ "Barrier") (nroot .@ "Heap")); auto with ndisj.
69
70
71
72
  Qed.

  Print Assumptions client_safe_closed.
End ClosedProofs.