joining_existentials.v 4.23 KB
Newer Older
1
2
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
3
From iris.algebra Require Import excl agree csum.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.heap_lang.lib.barrier Require Import proof specification.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris.heap_lang Require Import notation par proofmode.
6
From iris.proofmode Require Import tactics.
7
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
8

9
10
11
12
Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
  csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ)) : one_shotR Σ F :=
13
14
  Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.

15
16
Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
  one_shot_inG :> inG Σ (one_shotR Σ F).
17
18
19
Definition oneShotΣ (F : cFunctor) : gFunctors :=
  #[ GFunctor (csumRF (exclRF unitC) (agreeRF ( F))) ].
Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ  oneShotG Σ F.
20
Proof. solve_inG. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
21

22
Definition client eM eW1 eW2 : expr :=
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  let: "b" := newbarrier #() in
24
  (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
Ralf Jung's avatar
Ralf Jung committed
25
26

Section proof.
27
Local Set Default Proof Using "Type*".
28
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
29
Context (N : namespace).
30
Local Notation X := (F (iProp Σ)).
Ralf Jung's avatar
Ralf Jung committed
31

32
Definition barrier_res γ (Φ : X  iProp Σ) : iProp Σ :=
33
  ( x, own γ (Shot x)  Φ x)%I.
Ralf Jung's avatar
Ralf Jung committed
34

35
Lemma worker_spec e γ l (Φ Ψ : X  iProp Σ) `{!Closed [] e} :
36
37
  recv N l (barrier_res γ Φ) - ( x, {{ Φ x }} e {{ _, Ψ x }}) -
  WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Ralf Jung's avatar
Ralf Jung committed
38
Proof.
39
  iIntros "Hl #He". wp_apply (wait_spec with "[- $Hl]"); simpl.
40
  iDestruct 1 as (x) "[#Hγ Hx]".
Robbert Krebbers's avatar
Robbert Krebbers committed
41
  wp_seq. iApply (wp_wand with "[Hx]"); [by iApply "He"|].
42
  iIntros (v) "?"; iExists x; by iSplit.
Ralf Jung's avatar
Ralf Jung committed
43
44
Qed.

45
Context (P : iProp Σ) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp Σ).
46
47
Context {Φ_split :  x, Φ x - (Φ1 x  Φ2 x)}.
Context {Ψ_join  :  x, Ψ1 x - Ψ2 x - Ψ x}.
Ralf Jung's avatar
Ralf Jung committed
48

49
Lemma P_res_split γ : barrier_res γ Φ - barrier_res γ Φ1  barrier_res γ Φ2.
Ralf Jung's avatar
Ralf Jung committed
50
Proof.
51
  iDestruct 1 as (x) "[#Hγ Hx]".
52
  iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
Ralf Jung's avatar
Ralf Jung committed
53
54
Qed.

55
Lemma Q_res_join γ : barrier_res γ Ψ1 - barrier_res γ Ψ2 -  barrier_res γ Ψ.
Ralf Jung's avatar
Ralf Jung committed
56
Proof.
57
  iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']".
58
  iAssert ( (x  x'))%I as "Hxx".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
59
  { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
60
    rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
61
    rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
62
    rewrite (ne_proper (cFunctor_map F) (cid, cid) (_  _, _  _)); last first.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
    { by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
64
    rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  iNext. iRewrite -"Hxx" in "Hx'".
66
  iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
Ralf Jung's avatar
Ralf Jung committed
67
68
Qed.

69
Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
70
71
72
73
74
  P -
  {{ P }} eM {{ _,  x, Φ x }} -
  ( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -
  ( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -
  WP client eM eW1 eW2 {{ _,  γ, barrier_res γ Ψ }}.
75
Proof using All.
76
  iIntros "/= HP #He #He1 #He2"; rewrite /client.
77
  iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
78
  wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
79
  iIntros (l) "[Hr Hs]".
80
  set (workers_post (v : val) := (barrier_res γ Ψ1  barrier_res γ Ψ2)%I).
81
  wp_let. wp_apply (wp_par  (λ _, True)%I workers_post with "[HP Hs Hγ] [Hr]").
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  - wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|].
83
    iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
84
    iMod (own_update with "Hγ") as "Hx".
85
    { by apply (cmra_update_exclusive (Shot x)). }
Ralf Jung's avatar
Ralf Jung committed
86
    iApply (signal_spec with "[- $Hs]"); last auto.
87
    iExists x; auto.
88
  - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
89
    iMod (recv_split with "Hr") as "[H1 H2]"; first done.
90
91
92
93
    wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
                     (λ _, barrier_res γ Ψ2)%I with "[H1] [H2]").
    + iApply (worker_spec with "H1"); auto.
    + iApply (worker_spec with "H2"); auto.
94
    + auto.
95
  - iIntros (_ v) "[_ [H1 H2]]". iDestruct (Q_res_join with "H1 H2") as "?". auto.
Ralf Jung's avatar
Ralf Jung committed
96
97
Qed.
End proof.