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

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

Ralf Jung's avatar
Ralf Jung committed
16 17 18
Section client.
  Local Set Default Proof Using "Type*".
  Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
Ralf Jung's avatar
Ralf Jung committed
19

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

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
60
Section ClosedProofs.
Ralf Jung's avatar
Ralf Jung committed
61

Ralf Jung's avatar
Ralf Jung committed
62
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
Ralf Jung's avatar
Ralf Jung committed
63

Robbert Krebbers's avatar
Robbert Krebbers committed
64
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Ralf Jung's avatar
Ralf Jung committed
65
Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
Ralf Jung's avatar
Ralf Jung committed
66

Ralf Jung's avatar
Ralf Jung committed
67 68 69
End ClosedProofs.

Print Assumptions client_adequate.