channel.v 8.3 KB
Newer Older
1 2
(** This file contains the definition of the channels, encoded as a pair of
lock-protected buffers, on which we define the three message-passing primitives:
3

4 5 6 7 8 9
- [new_chan] creates references to two empty buffers and a lock, and returns a
  pair of endpoints, where the order of the two references determines the
  polarity of the endpoints.
- [send] takes an endpoint and adds an element to the first buffer.
- [recv] performs a busy loop until there is something in the second buffer,
  which it pops and returns, locking during each peek.
10 11

The specifications are defined in terms of the logical connectives [is_chan]
12 13 14 15 16 17
and [chan_own]:

- [is_chan γ v1 v2] is a persistent proposition expressing that [v1] and [v2]
  are the endpoints of a channel with logical name [γ].
- [chan_own γ s vs] is an exclusive proposition expressing the buffer of side
  [s] ([Left] or [Right]) has contents [vs]. *)
18 19
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
Jonas Kastberg's avatar
Jonas Kastberg committed
20
From iris.heap_lang Require Import lifting.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
From iris.algebra Require Import excl auth list.
Jonas Kastberg's avatar
Jonas Kastberg committed
22
From actris.utils Require Import auth_excl llist.
23 24
Set Default Proof Using "Type".

Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27 28 29
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.

30
(** Message-Passing Primitives *)
31
Definition new_chan : val :=
32
  λ: <>,
33 34
     let: "l" := lnil #() in
     let: "r" := lnil #() in
35
     let: "lk" := newlock #() in
Robbert Krebbers's avatar
Robbert Krebbers committed
36
     ((("l","r"),"lk"), (("r","l"),"lk")).
37 38

Definition send : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40
  λ: "c" "v",
    let: "lk" := Snd "c" in
41
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
42
    let: "l" := Fst (Fst "c") in
43
    lsnoc "l" "v";;
44
    release "lk".
45 46

Definition try_recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48
  λ: "c",
    let: "lk" := Snd "c" in
49
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
50
    let: "l" := Snd (Fst "c") in
51
    let: "ret" := if: lisnil "l" then NONE else SOME (lpop "l") in
52
    release "lk";; "ret".
53 54

Definition recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
  rec: "go" "c" :=
    match: try_recv "c" with
57
      SOME "p" => "p"
Robbert Krebbers's avatar
Robbert Krebbers committed
58
    | NONE => "go" "c"
59 60
    end.

61
(** Channel ghost functor *)
62 63
Class chanG Σ := {
  chanG_lockG :> lockG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  chanG_authG :> auth_exclG (listO valO) Σ;
65 66
}.
Definition chanΣ : gFunctors :=
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  #[ lockΣ; auth_exclΣ (constOF (listO valO)) ].
68 69 70
Instance subG_chanΣ {Σ} : subG chanΣ Σ  chanG Σ.
Proof. solve_inG. Qed.

71
Section channel.
72
  Context `{!heapG Σ, !chanG Σ} (N : namespace).
73

74 75 76 77 78 79
  Record chan_name := Chan_name {
    chan_lock_name : gname;
    chan_l_name : gname;
    chan_r_name : gname
  }.

80
  (** The invariant of channels *)
81
  Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
82
    ( ls rs,
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
      llist sbi_internal_eq l ls  own (chan_l_name γ) ( to_auth_excl ls) 
      llist sbi_internal_eq r rs  own (chan_r_name γ) ( to_auth_excl rs))%I.
85 86
  Typeclasses Opaque chan_inv.

Robbert Krebbers's avatar
Robbert Krebbers committed
87
  Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
88 89
    ( (l r : loc) (lk : val),
       c1 = ((#l, #r), lk)%V  c2 = ((#r, #l), lk)%V  
90
      is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
91

Robbert Krebbers's avatar
Robbert Krebbers committed
92
  Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
93 94
  Proof. by apply _. Qed.

95 96 97 98 99 100 101 102 103 104 105 106
  Lemma chan_inv_alt s γ l r :
    chan_inv γ l r   ls rs,
      llist sbi_internal_eq (side_elim s l r) ls 
      own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl ls) 
      llist sbi_internal_eq (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.

  (** The ownership of channels *)
107 108
  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.
109

110
  Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
111 112
  Proof. by apply _. Qed.

113 114
  Lemma new_chan_spec :
    {{{ True }}}
115
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
116
    {{{ c1 c2 γ, RET (c1,c2); is_chan γ c1 c2  chan_own γ Left []  chan_own γ Right [] }}}.
117
  Proof.
118
    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
119
    wp_lam.
120 121
    wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
    wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
jihgfee's avatar
jihgfee committed
122
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl []))) as (lsγ) "[Hls Hls']".
123
    { by apply auth_both_valid. }
jihgfee's avatar
jihgfee committed
124
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
125
    { by apply auth_both_valid. }
126
    wp_apply (newlock_spec N ( ls rs,
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128
      llist sbi_internal_eq l ls  own lsγ ( to_auth_excl ls) 
      llist sbi_internal_eq r rs  own rsγ ( to_auth_excl rs))%I with "[Hl Hr Hls Hrs]").
129 130
    { eauto 10 with iFrame. }
    iIntros (lk γlk) "#Hlk". wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
    iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
132
    rewrite /chan_inv /=. eauto 20 with iFrame.
133 134
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
135 136
  Lemma send_spec Φ E γ c1 c2 v s :
    is_chan γ c1 c2 -
137 138
    (|={,E}=>  vs,
      chan_own γ s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140
       (chan_own γ s (vs ++ [v]) ={E,}=   Φ #())) -
    WP send (side_elim s c1 c2) v {{ Φ }}.
141
  Proof.
142
    iIntros "Hc HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
144 145
    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).
146
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
147
    iDestruct (chan_inv_alt s with "Hinv") as
148 149
      (vs ws) "(Hll & Hvs & Href' & Hws)".
    wp_seq. wp_bind (Fst (_,_)%V)%E.
150
    iMod "HΦ" as (vs') "[Hchan HΦ]".
151
    iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
152
    iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
153
    wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
155 156
    wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
    iApply (chan_inv_alt s).
157
    rewrite /llist. eauto 20 with iFrame.
158 159
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
160 161 162 163 164 165 166 167
  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) {{ Φ }}.
168
  Proof.
169
    iIntros "Hc HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
171 172
    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).
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
    iDestruct (chan_inv_alt s with "Hinv")
175 176 177 178
      as (vs ws) "(Hll & Hvs & Href' & Hws)".
    wp_seq. wp_bind (Fst (_,_)%V)%E. destruct vs as [|v vs]; simpl.
    - iDestruct "HΦ" as "[>HΦ _]". wp_pures. iMod "HΦ"; iModIntro.
      wp_apply (lisnil_spec with "Hll"); iIntros "Hll". wp_pures.
179
      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
Robbert Krebbers's avatar
Robbert Krebbers committed
180
      { iApply (chan_inv_alt s).
181
        rewrite /llist. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
182 183 184 185
      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']".
186 187
      wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
      wp_apply (lisnil_spec with "Hll"); iIntros "Hll".
Robbert Krebbers's avatar
Robbert Krebbers committed
188
      wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
189
      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
Robbert Krebbers's avatar
Robbert Krebbers committed
190
      { iApply (chan_inv_alt s).
191
        rewrite /llist. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
192
      iIntros (_). by wp_pures.
193
  Qed.
194

Robbert Krebbers's avatar
Robbert Krebbers committed
195 196 197 198 199 200 201
  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) {{ Φ }}.
202
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205 206 207 208 209
    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.
210
  Qed.
211

Robbert Krebbers's avatar
Robbert Krebbers committed
212
End channel.