channel.v 8.26 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
From iris.algebra Require Import excl auth list.
jihgfee's avatar
jihgfee committed
21
From actris.utils Require Import auth_excl llist misc.
22 23
Set Default Proof Using "Type".

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

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

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

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

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

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

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

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

79
  (** The invariant of channels *)
80
  Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
81
    ( ls rs,
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83
      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.
84 85
  Typeclasses Opaque chan_inv.

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

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

94 95 96 97 98 99 100 101 102 103 104 105
  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 *)
106 107
  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.
108

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

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

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

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

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

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