channel.v 7.55 KB
Newer Older
1 2
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.algebra Require Import excl auth list.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From actris.utils Require Import auth_excl list.
5 6
Set Default Proof Using "Type".

Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11
Inductive side := Left | Right.
Instance side_inhabited : Inhabited side := populate Left.
Definition side_elim {A} (s : side) (l r : A) : A :=
  match s with Left => l | Right => r end.

12
Definition new_chan : val :=
13
  λ: <>,
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
14 15
     let: "l" := ref (lnil #()) in
     let: "r" := ref (lnil #()) in
16
     let: "lk" := newlock #() in
Robbert Krebbers's avatar
Robbert Krebbers committed
17
     ((("l","r"),"lk"), (("r","l"),"lk")).
18 19

Definition send : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
  λ: "c" "v",
    let: "lk" := Snd "c" in
22
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
23
    let: "l" := Fst (Fst "c") in
24 25
    "l" <- lsnoc !"l" "v";;
    release "lk".
26 27

Definition try_recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29
  λ: "c",
    let: "lk" := Snd "c" in
30
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
31
    let: "l" := Snd (Fst "c") in
32 33 34 35 36 37
    let: "ret" :=
      match: !"l" with
        SOME "p" => "l" <- Snd "p";; SOME (Fst "p")
      | NONE => NONE
      end in
    release "lk";; "ret".
38 39

Definition recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
  rec: "go" "c" :=
    match: try_recv "c" with
42
      SOME "p" => "p"
Robbert Krebbers's avatar
Robbert Krebbers committed
43
    | NONE => "go" "c"
44 45
    end.

46 47
Class chanG Σ := {
  chanG_lockG :> lockG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
48
  chanG_authG :> auth_exclG (listO valO) Σ;
49 50
}.
Definition chanΣ : gFunctors :=
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  #[ lockΣ; auth_exclΣ (constOF (listO valO)) ].
52 53 54
Instance subG_chanΣ {Σ} : subG chanΣ Σ  chanG Σ.
Proof. solve_inG. Qed.

55
Section channel.
56
  Context `{!heapG Σ, !chanG Σ} (N : namespace).
57

58
  Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
59
    ( l' : loc, l = #l'  l'  llist xs)%I.
60

61 62 63 64 65 66
  Record chan_name := Chan_name {
    chan_lock_name : gname;
    chan_l_name : gname;
    chan_r_name : gname
  }.

67 68 69 70 71 72
  Definition chan_inv (γ : chan_name) (l r : val) : iProp Σ :=
    ( ls rs,
      is_list_ref l ls  own (chan_l_name γ) ( to_auth_excl ls) 
      is_list_ref r rs  own (chan_r_name γ) ( to_auth_excl rs))%I.
  Typeclasses Opaque chan_inv.

Robbert Krebbers's avatar
Robbert Krebbers committed
73
  Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
74
    ( l r lk : val,
Robbert Krebbers's avatar
Robbert Krebbers committed
75
       c1 = ((l, r), lk)%V  c2 = ((r, l), lk)%V  
76
      is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
77

Robbert Krebbers's avatar
Robbert Krebbers committed
78
  Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
79 80
  Proof. by apply _. Qed.

81 82
  Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
    own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl vs)%I.
83

84
  Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
85 86
  Proof. by apply _. Qed.

87 88
  Lemma new_chan_spec :
    {{{ True }}}
89
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
90
    {{{ c1 c2 γ, RET (c1,c2); is_chan γ c1 c2  chan_own γ Left []  chan_own γ Right [] }}}.
91
  Proof.
92
    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
93
    wp_lam.
94 95
    wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
    wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
96 97 98 99
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl []))) as (lsγ) "[Hls Hls']".
    { by apply auth_both_valid. }
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
    { by apply auth_both_valid. }
100 101 102 103 104 105 106 107 108 109
    iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
    { rewrite /is_list_ref; eauto. }
    iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
    { rewrite /is_list_ref; eauto. }
    wp_apply (newlock_spec N ( ls rs,
      is_list_ref #l ls  own lsγ ( to_auth_excl ls) 
      is_list_ref #r rs  own rsγ ( to_auth_excl rs))%I
                with "[Hl Hr Hls Hrs]").
    { eauto 10 with iFrame. }
    iIntros (lk γlk) "#Hlk". wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
    iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
111
    rewrite /chan_inv /=. eauto 20 with iFrame.
112 113
  Qed.

114 115 116 117 118 119 120 121 122 123
  Lemma chan_inv_alt s γ l r :
    chan_inv γ l r   ls rs,
      is_list_ref (side_elim s l r) ls 
      own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl ls) 
      is_list_ref (side_elim s r l) rs 
      own (side_elim s chan_r_name chan_l_name γ) ( to_auth_excl rs).
  Proof.
    destruct s; rewrite /chan_inv //=.
    iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
  Qed.
124

Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
  Lemma send_spec Φ E γ c1 c2 v s :
    is_chan γ c1 c2 -
127 128
    (|={,E}=>  vs,
      chan_own γ s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
       (chan_own γ s (vs ++ [v]) ={E,}=   Φ #())) -
    WP send (side_elim s c1 c2) v {{ Φ }}.
131
  Proof.
132
    iIntros "Hc HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135
    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
    assert (side_elim s (l, r, lk)%V (r, l, lk)%V =
      ((side_elim s l r, side_elim s r l), lk)%V) as -> by (by destruct s).
136
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    wp_pures.
138
    iDestruct (chan_inv_alt s with "Hinv") as
Robbert Krebbers's avatar
Robbert Krebbers committed
139
      (vs ws) "(Href & Hvs & Href' & Hws)".
140
    iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
    wp_load.
142
    wp_apply (lsnoc_spec with "[//]"); iIntros (_).
143 144
    wp_bind (_ <- _)%E.
    iMod "HΦ" as (vs') "[Hchan HΦ]".
145
    iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
146 147 148 149 150
    iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
    wp_store. iMod ("HΦ" with "Hchan") as "HΦ".
    iModIntro.
    wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
    iApply (chan_inv_alt s).
151
    rewrite /is_list_ref. eauto 20 with iFrame.
152 153
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156 157 158 159 160 161
  Lemma try_recv_spec Φ E γ c1 c2 s :
    is_chan γ c1 c2 -
    ((|={,E}=>  Φ NONEV) 
     (|={,E}=>  vs,
       chan_own γ s vs 
        ( v vs',  vs = v :: vs'  -
                   chan_own γ s vs' ={E,}=   Φ (SOMEV v)))) -
    WP try_recv (side_elim s c2 c1) {{ Φ }}.
162
  Proof.
163
    iIntros "Hc HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
164 165 166 167 168 169 170 171 172 173
    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
    assert (side_elim s (r, l, lk)%V (l, r, lk)%V =
      ((side_elim s r l, side_elim s l r), lk)%V) as -> by (by destruct s).
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
    wp_pures.
    iDestruct (chan_inv_alt s with "Hinv")
      as (vs ws) "(Href & Hvs & Href' & Hws)".
    iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
    wp_bind (! _)%E. destruct vs as [|v vs]; simpl.
    - iDestruct "HΦ" as "[>HΦ _]". wp_load. iMod "HΦ"; iModIntro.
174
      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
Robbert Krebbers's avatar
Robbert Krebbers committed
175
      { iApply (chan_inv_alt s).
176
        rewrite /is_list_ref. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179 180 181 182 183
      iIntros (_). by wp_pures.
    - iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
      iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv.
      iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']".
      wp_load.
      iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
      wp_store; wp_pures.
184
      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
Robbert Krebbers's avatar
Robbert Krebbers committed
185
      { iApply (chan_inv_alt s).
186
        rewrite /is_list_ref. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
187
      iIntros (_). by wp_pures.
188
  Qed.
189

Robbert Krebbers's avatar
Robbert Krebbers committed
190 191 192 193 194 195 196
  Lemma recv_spec Φ E γ c1 c2 s :
    is_chan γ c1 c2 -
    (|={,E}=>  vs,
      chan_own γ s vs 
        v vs',  vs = v :: vs'  -
                 chan_own γ s vs' ={E,}=   Φ v) -
    WP recv (side_elim s c2 c1) {{ Φ }}.
197
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
198 199 200 201 202 203 204
    iIntros "#Hc HΦ". iLöb as "IH". wp_lam.
    wp_apply (try_recv_spec _ E with "Hc")=> //. iSplit.
    - iMod (fupd_intro_mask' _ E) as "Hclose"; first done. iIntros "!> !>".
      iMod "Hclose" as %_; iIntros "!> !>". wp_pures. by iApply "IH".
    - iMod "HΦ" as (vs) "[Hvs HΦ]". iExists vs; iFrame "Hvs".
      iIntros "!> !>" (v vs' ->) "Hvs".
      iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures.
205
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
End channel.