channel.v 8.76 KB
Newer Older
1
(** This file contains the definition of the channels, encoded as a pair of
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5 6
lock-protected buffers, and their primitive proof rules. Actris's proof rules
for channels in terms of dependent separation protocols can be found in the file
[theories/channel/proto_channel.v].

In this file we define the three message-passing connectives:
7

8 9 10 11 12 13
- [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.
14

Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17
The logically-atomic basic (i.e. non dependent separation protocol)
proof rules [new_chan_spec], [send_spec] and [recv_spec] are defined in terms
of the logical connectives [is_chan] and [chan_own]:
18 19 20 21

- [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
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24 25 26
  [s] ([Left] or [Right]) has contents [vs].

Note that the specifications include 3 laters [▷] to account for the three
levels of indirection due to step-indexing in the model of dependent separation
protocols. *)
27 28
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
Jonas Kastberg's avatar
Jonas Kastberg committed
29
From iris.heap_lang Require Import lifting.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
From iris.algebra Require Import excl auth list.
Jonas Kastberg's avatar
Jonas Kastberg committed
31
From actris.utils Require Import auth_excl llist.
32 33
Set Default Proof Using "Type".

Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36 37 38
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
39
(** * The definition of the message-passing connectives *)
40
Definition new_chan : val :=
41
  λ: <>,
42 43
     let: "l" := lnil #() in
     let: "r" := lnil #() in
44
     let: "lk" := newlock #() in
Robbert Krebbers's avatar
Robbert Krebbers committed
45
     ((("l","r"),"lk"), (("r","l"),"lk")).
46 47

Definition send : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
  λ: "c" "v",
    let: "lk" := Snd "c" in
50
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
51
    let: "l" := Fst (Fst "c") in
52
    lsnoc "l" "v";;
53
    release "lk".
54 55

Definition try_recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57
  λ: "c",
    let: "lk" := Snd "c" in
58
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
59
    let: "l" := Snd (Fst "c") in
60
    let: "ret" := if: lisnil "l" then NONE else SOME (lpop "l") in
61
    release "lk";; "ret".
62 63

Definition recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65
  rec: "go" "c" :=
    match: try_recv "c" with
66
      SOME "p" => "p"
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    | NONE => "go" "c"
68 69
    end.

Robbert Krebbers's avatar
Robbert Krebbers committed
70
(** * Setup of Iris's cameras *)
71 72
Class chanG Σ := {
  chanG_lockG :> lockG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  chanG_authG :> auth_exclG (listO valO) Σ;
74 75
}.
Definition chanΣ : gFunctors :=
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  #[ lockΣ; auth_exclΣ (constOF (listO valO)) ].
77 78 79
Instance subG_chanΣ {Σ} : subG chanΣ Σ  chanG Σ.
Proof. solve_inG. Qed.

80
Section channel.
81
  Context `{!heapG Σ, !chanG Σ} (N : namespace).
82

83 84 85 86 87 88
  Record chan_name := Chan_name {
    chan_lock_name : gname;
    chan_l_name : gname;
    chan_r_name : gname
  }.

Robbert Krebbers's avatar
Robbert Krebbers committed
89
  (** * The logical connectives *)
90
  Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
91
    ( ls rs,
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93
      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.
94 95
  Typeclasses Opaque chan_inv.

Robbert Krebbers's avatar
Robbert Krebbers committed
96
  Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
97 98
    ( (l r : loc) (lk : val),
       c1 = ((#l, #r), lk)%V  c2 = ((#r, #l), lk)%V  
99
      is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
100

Robbert Krebbers's avatar
Robbert Krebbers committed
101
  Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
102 103
  Proof. by apply _. Qed.

104 105 106 107 108 109 110 111 112 113 114
  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.

115 116
  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.
117

Robbert Krebbers's avatar
Robbert Krebbers committed
118
  (** * The proof rules *)
119
  Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
120 121
  Proof. by apply _. Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171 172 173 174 175 176
  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) {{ Φ }}.
177
  Proof.
178
    iIntros "Hc HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
180 181
    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
182 183
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
    iDestruct (chan_inv_alt s with "Hinv")
184 185 186 187
      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.
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 192 193 194
      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']".
195 196
      wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
      wp_apply (lisnil_spec with "Hll"); iIntros "Hll".
Robbert Krebbers's avatar
Robbert Krebbers committed
197
      wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
198
      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
Robbert Krebbers's avatar
Robbert Krebbers committed
199
      { iApply (chan_inv_alt s).
200
        rewrite /llist. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
201
      iIntros (_). by wp_pures.
202
  Qed.
203

Robbert Krebbers's avatar
Robbert Krebbers committed
204 205 206 207 208 209 210
  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) {{ Φ }}.
211
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
212 213 214 215 216 217 218
    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.
219
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
End channel.