channel.v 8.77 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.
30 31
From iris.algebra Require Import excl_auth list.
From actris.utils Require Import 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 Σ;
73
  chanG_authG :> inG Σ (excl_authR (listO valO));
74 75
}.
Definition chanΣ : gFunctors :=
76
  #[ lockΣ; GFunctor (excl_authR (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,
92 93
      llist sbi_internal_eq l ls  own (chan_l_name γ) (E ls) 
      llist sbi_internal_eq r rs  own (chan_r_name γ) (E 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
  Lemma chan_inv_alt s γ l r :
    chan_inv γ l r   ls rs,
      llist sbi_internal_eq (side_elim s l r) ls 
107
      own (side_elim s chan_l_name chan_r_name γ) (E ls) 
108
      llist sbi_internal_eq (side_elim s r l) rs 
109
      own (side_elim s chan_r_name chan_l_name γ) (E rs).
110 111 112 113 114
  Proof.
    destruct s; rewrite /chan_inv //=.
    iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
  Qed.

115
  Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
116
    own (side_elim s chan_l_name chan_r_name γ) (E 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".
131 132 133 134
    iMod (own_alloc (E []  E [])) as (lsγ) "[Hls Hls']".
    { by apply excl_auth_valid. }
    iMod (own_alloc (E []  E [])) as (rsγ) "[Hrs Hrs']".
    { by apply excl_auth_valid. }
135
    wp_apply (newlock_spec N ( ls rs,
136 137
      llist sbi_internal_eq l ls  own lsγ (E ls) 
      llist sbi_internal_eq r rs  own rsγ (E 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 161 162
    iDestruct (own_valid_2 with "Hvs Hchan") as %<-%excl_auth_agreeL.
    iMod (own_update_2 _ _ _ (E (vs ++ [v])  _) with "Hvs Hchan") as "[Hvs Hchan]".
    { apply excl_auth_update. }
163
    wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
    wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
165 166
    wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
    iApply (chan_inv_alt s).
167
    rewrite /llist. eauto 20 with iFrame.
168 169
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
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'  -
211
                 chan_own γ s vs' ={E,,}=  Φ v) -
Robbert Krebbers's avatar
Robbert Krebbers committed
212
    WP recv (side_elim s c2 c1) {{ Φ }}.
213
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
214 215 216 217 218 219
    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".
220 221
      iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !>". iMod "HΦ".
      iIntros "!> !>". by wp_pures.
222
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
End channel.