joining_existentials.v 3.41 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.program_logic Require Import saved_one_shot hoare.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.heap_lang.lib.barrier Require Import proof specification.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
From iris.heap_lang Require Import notation par proofmode.
From iris.proofmode Require Import invariants.
Ralf Jung's avatar
Ralf Jung committed
5
6
7
Import uPred.

Definition client eM eW1 eW2 : expr [] :=
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
  let: "b" := newbarrier #() in
  (eM ;; ^signal '"b") || ((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2)).
Ralf Jung's avatar
Ralf Jung committed
10
11
12
13
14
15
16
17

Section proof.
Context (G : cFunctor).
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG heap_lang Σ G}.
Context (heapN N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation X := (G iProp).

Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
Definition barrier_res γ (Φ : X  iProp) : iProp :=
  ( x, one_shot_own γ x  Φ x)%I.
Ralf Jung's avatar
Ralf Jung committed
20

Robbert Krebbers's avatar
Robbert Krebbers committed
21
Lemma worker_spec e γ l (Φ Ψ : X  iProp) :
22
  (recv heapN N l (barrier_res γ Φ)   x, {{ Φ x }} e {{ _, Ψ x }})
23
   WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Ralf Jung's avatar
Ralf Jung committed
24
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
27
28
  iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
  iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
  wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He" "!"].
  iIntros {v} "?"; iExists x; by iSplit.
Ralf Jung's avatar
Ralf Jung committed
29
30
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
Context (P : iProp) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp).
Context {Φ_split :  x, Φ x  (Φ1 x  Φ2 x)}.
Context {Ψ_join  :  x, (Ψ1 x  Ψ2 x)  Ψ x}.
Ralf Jung's avatar
Ralf Jung committed
34

Robbert Krebbers's avatar
Robbert Krebbers committed
35
Lemma P_res_split γ : barrier_res γ Φ  (barrier_res γ Φ1  barrier_res γ Φ2).
Ralf Jung's avatar
Ralf Jung committed
36
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
  iDestruct Φ_split "Hx" as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
Ralf Jung's avatar
Ralf Jung committed
39
40
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
41
Lemma Q_res_join γ : (barrier_res γ Ψ1  barrier_res γ Ψ2)   barrier_res γ Ψ.
Ralf Jung's avatar
Ralf Jung committed
42
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
47
  iIntros "[Hγ Hγ']";
  iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
  iDestruct (one_shot_agree γ x x') "- !" as "Hxx"; first (by iSplit).
  iNext. iRewrite -"Hxx" in "Hx'".
  iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
Ralf Jung's avatar
Ralf Jung committed
48
49
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
50
Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) :
Ralf Jung's avatar
Ralf Jung committed
51
  heapN  N  eM' = wexpr' eM  eW1' = wexpr' eW1  eW2' = wexpr' eW2 
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  (heap_ctx heapN  P
53
54
55
56
   {{ P }} eM {{ _,  x, Φ x }}
   ( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }})
   ( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}))
   WP client eM' eW1' eW2' {{ _,  γ, barrier_res γ Ψ }}.
Ralf Jung's avatar
Ralf Jung committed
57
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
  iIntros {HN -> -> ->} "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
  iPvs one_shot_alloc as {γ} "Hγ".
  wp_apply (newbarrier_spec heapN N (barrier_res γ Φ)); auto.
  iFrame "Hh". iIntros {l} "[Hr Hs]".
  set (workers_post (v : val) := (barrier_res γ Ψ1  barrier_res γ Ψ2)%I).
  wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post); first done.
  iFrame "Hh". iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|iApply "He" "HP"].
    iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
    iPvs (one_shot_init _ _ x) "Hγ" as "Hx".
    iApply signal_spec; iFrame "Hs"; iSplit; last done.
    iExists x; by iSplitL "Hx".
  - iDestruct recv_weaken "[] Hr" as "Hr".
    { iIntros "?". by iApply P_res_split "-". }
    iPvs recv_split "Hr" as "[H1 H2]"; first done.
    wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
      (λ _, barrier_res γ Ψ2)%I); first done.
    iSplit; [done|]; iSplitL "H1"; [|iSplitL "H2"].
    + by iApply worker_spec; iSplitL "H1".
    + by iApply worker_spec; iSplitL "H2".
Robbert Krebbers's avatar
Robbert Krebbers committed
78
    + by iIntros {v1 v2} "? >".
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  - iIntros {_ v} "[_ H]"; iPoseProof Q_res_join "H". by iNext; iExists γ.
Ralf Jung's avatar
Ralf Jung committed
80
81
Qed.
End proof.