joining_existentials.v 3.44 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)).
10
Global Opaque client.
Ralf Jung's avatar
Ralf Jung committed
11 12 13 14 15 16 17 18

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
19 20
Definition barrier_res γ (Φ : X  iProp) : iProp :=
  ( x, one_shot_own γ x  Φ x)%I.
Ralf Jung's avatar
Ralf Jung committed
21

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

Robbert Krebbers's avatar
Robbert Krebbers committed
32 33 34
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
35

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
51
Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) :
Ralf Jung's avatar
Ralf Jung committed
52
  heapN  N  eM' = wexpr' eM  eW1' = wexpr' eW1  eW2' = wexpr' eW2 
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  (heap_ctx heapN  P
54 55 56 57
   {{ 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
58
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61 62 63 64 65
  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"].
66
  - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
68
    iPvs (one_shot_init _ _ x with "Hγ") as "Hx".
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70
    iApply signal_spec; iFrame "Hs"; iSplit; last done.
    iExists x; by iSplitL "Hx".
71
  - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
72
    iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74 75 76 77
    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} "? >".
79
  - iIntros {_ v} "[_ H]"; iPoseProof (Q_res_join with "H"). by iNext; iExists γ.
Ralf Jung's avatar
Ralf Jung committed
80 81
Qed.
End proof.