channel.v 12.8 KB
Newer Older
1
(** This file contains the definition of the channels, encoded as a pair of
2 3 4 5
lock-protected buffers, and their primitive proof rules. Moreover:

- It defines the connective [c ↣ prot] for ownership of channel endpoints,
  which describes that channel endpoint [c] adheres to protocol [prot].
Robbert Krebbers's avatar
Robbert Krebbers committed
6
- It proves Actris's specifications of [send] and [recv] w.r.t. dependent
7 8 9 10 11
  separation protocols.

An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
[prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
file.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13

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

15 16 17 18 19
- [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,
20
  which it pops and returns, locking during each peek.*)
21 22
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
23 24
From actris.channel Require Export proto.
From actris.utils Require Import llist skip.
25 26
Set Default Proof Using "Type".

Robbert Krebbers's avatar
Robbert Krebbers committed
27
(** * The definition of the message-passing connectives *)
28
Definition new_chan : val :=
29
  λ: <>,
30 31
     let: "l" := lnil #() in
     let: "r" := lnil #() in
32
     let: "lk" := newlock #() in
Robbert Krebbers's avatar
Robbert Krebbers committed
33
     ((("l","r"),"lk"), (("r","l"),"lk")).
34

35 36 37 38
Definition start_chan : val := λ: "f",
  let: "cc" := new_chan #() in
  Fork ("f" (Snd "cc"));; Fst "cc".

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
63
(** * Setup of Iris's cameras *)
64 65
Definition chanN := nroot .@ "chan".

66 67
Class chanG Σ := {
  chanG_lockG :> lockG Σ;
68
  chanG_protoG :> protoG Σ val;
69
}.
70
Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
71 72 73
Instance subG_chanΣ {Σ} : subG chanΣ Σ  chanG Σ.
Proof. solve_inG. Qed.

74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
Record chan_name := ChanName {
  chan_lock_name : gname;
  chan_proto_name : proto_name;
}.

(** * Definition of the mapsto connective *)
Notation iProto Σ := (iProto Σ val).

Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
    (c : val) (p : iProto Σ) : iProp Σ :=
   γ s (l r : loc) (lk : val),
     c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V  
    is_lock chanN (chan_lock_name γ) lk ( vsl vsr,
      llist sbi_internal_eq l vsl 
      llist sbi_internal_eq r vsr 
      iProto_ctx (chan_proto_name γ) vsl vsr) 
    iProto_own (chan_proto_name γ) s p.
Definition iProto_mapsto_aux : seal (@iProto_mapsto_def). by eexists. Qed.
Definition iProto_mapsto := iProto_mapsto_aux.(unseal).
Definition iProto_mapsto_eq :
  @iProto_mapsto = @iProto_mapsto_def := iProto_mapsto_aux.(seal_eq).
Arguments iProto_mapsto {_ _ _} _ _%proto.
Instance: Params (@iProto_mapsto) 4 := {}.
Notation "c ↣ p" := (iProto_mapsto c p)
  (at level 20, format "c  ↣  p").

Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
    (p1 p2 : iProto Σ) : iProto Σ :=
  (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
Typeclasses Opaque iProto_branch.
Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
Instance: Params (@iProto_branch) 2 := {}.
Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Infix "<{ P1 }&{ P2 }>" := (iProto_branch Recv P1 P2) (at level 85) : proto_scope.
108
Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Infix "<&{ P2 }>" := (iProto_branch Recv True P2) (at level 85) : proto_scope.
110
Infix "<{ P1 }+>" := (iProto_branch Send P1 True) (at level 85) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
Infix "<{ P1 }&>" := (iProto_branch Recv P1 True) (at level 85) : proto_scope.
112
Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Infix "<&>" := (iProto_branch Recv True True) (at level 85) : proto_scope.
114

115
Section channel.
116 117 118 119 120 121 122 123 124 125
  Context `{!heapG Σ, !chanG Σ}.
  Implicit Types p : iProto Σ.
  Implicit Types TT : tele.

  Global Instance iProto_mapsto_ne c : NonExpansive (iProto_mapsto c).
  Proof. rewrite iProto_mapsto_eq. solve_proper. Qed.
  Global Instance iProto_mapsto_proper c : Proper (() ==> ()) (iProto_mapsto c).
  Proof. apply (ne_proper _). Qed.

  Lemma iProto_mapsto_le c p1 p2 : c  p1 - iProto_le p1 p2 - c  p2.
126
  Proof.
127 128 129
    rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
    iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
    by iApply (iProto_own_le with "H").
130 131
  Qed.

132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
  Global Instance iProto_branch_contractive n a :
    Proper (dist_later n ==> dist_later n ==>
            dist_later n ==> dist_later n ==> dist n) (@iProto_branch Σ a).
  Proof.
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
    apply iProto_message_contractive=> /= -[] //.
  Qed.
  Global Instance iProto_branch_ne n a :
    Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_branch Σ a).
  Proof.
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
    by apply iProto_message_ne=> /= -[].
  Qed.
  Global Instance iProto_branch_proper a :
    Proper (() ==> () ==> () ==> () ==> ()) (@iProto_branch Σ a).
  Proof.
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
    by apply iProto_message_proper=> /= -[].
  Qed.
151

152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
  Lemma iProto_dual_branch a P1 P2 p1 p2 :
    iProto_dual (iProto_branch a P1 P2 p1 p2)
     iProto_branch (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
  Proof.
    rewrite /iProto_branch iProto_dual_message /=.
    by apply iProto_message_proper=> /= -[].
  Qed.

  Lemma iProto_app_branch a P1 P2 p1 p2 q :
    (iProto_branch a P1 P2 p1 p2 <++> q)%proto
     (iProto_branch a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
  Proof.
    rewrite /iProto_branch iProto_app_message.
    by apply iProto_message_proper=> /= -[].
  Qed.
167

168 169
  (** ** Specifications of [send] and [recv] *)
  Lemma new_chan_spec p :
170
    {{{ True }}}
171
      new_chan #()
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224
    {{{ c1 c2, RET (c1,c2); c1  p  c2  iProto_dual p }}}.
  Proof.
    iIntros (Φ _) "HΦ". wp_lam.
    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (l) "Hl".
    wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (r) "Hr".
    iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
    wp_apply (newlock_spec chanN ( vsl vsr,
      llist sbi_internal_eq l vsl  llist sbi_internal_eq r vsr 
      iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
    { iExists [], []. iFrame. }
    iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
    set (γ := ChanName γlk γp). iSplitL "Hcl".
    - rewrite iProto_mapsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
    - rewrite iProto_mapsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
  Qed.

  Lemma start_chan_spec p Φ (f : val) :
     ( c, c  iProto_dual p - WP f c {{ _, True }}) -
     ( c, c  p - Φ c) -
    WP start_chan f {{ Φ }}.
  Proof.
    iIntros "Hfork HΦ". wp_lam.
    wp_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
    wp_apply (wp_fork with "[Hfork Hc2]").
    { iNext. wp_apply ("Hfork" with "Hc2"). }
    wp_pures. iApply ("HΦ" with "Hc1").
  Qed.

  Lemma send_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) (x : TT) :
    {{{ c  iProto_message Send pc  (pc x).1.2 }}}
      send c (pc x).1.1
    {{{ RET #(); c  (pc x).2 }}}.
  Proof.
    rewrite iProto_mapsto_eq. iIntros (Φ) "[Hc Hpc] HΦ". wp_lam; wp_pures.
    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
    - iMod (iProto_send_l with "Hctx H Hpc") as "[Hctx H]".
      wp_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
      wp_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
      wp_apply skipN_spec.
      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
      iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
    - iMod (iProto_send_r with "Hctx H Hpc") as "[Hctx H]".
      wp_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
      wp_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
      wp_apply skipN_spec.
      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
      iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
  Qed.

  (** A version written without Texan triples that is more convenient to use
  (via [iApply] in Coq. *)
225
  Lemma send_spec {TT} Φ c v (pc : TT  val * iProp Σ * iProto Σ) :
226 227 228 229 230 231 232 233 234 235
    c  iProto_message Send pc -
    (.. x : TT,
       v = (pc x).1.1   (pc x).1.2   (c  (pc x).2 - Φ #())) -
    WP send c v {{ Φ }}.
  Proof.
    iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΦ]".
    by iApply (send_spec_packed with "[$]").
  Qed.

  Lemma try_recv_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
236
    {{{ c  iProto_message Recv pc }}}
237
      try_recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
238
    {{{ v, RET v; (v = NONEV  c  iProto_message Recv pc) 
239 240 241 242 243 244 245 246 247 248 249 250 251
                  ( x : TT, v = SOMEV ((pc x).1.1)  c  (pc x).2  (pc x).1.2) }}}.
  Proof.
    rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
    wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
    - wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
      destruct vsr as [|vr vsr]; wp_pures.
      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
        iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
      wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
      iMod (iProto_recv_l with "Hctx H") as "H". wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
      iMod "H" as (x ->) "(Hctx & H & Hpc)".
253 254 255 256 257 258 259 260 261 262
      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
      iFrame "Hpc". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
    - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
      destruct vsl as [|vl vsl]; wp_pures.
      { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
        iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
        iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
      wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
      iMod (iProto_recv_r with "Hctx H") as "H". wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
      iMod "H" as (x ->) "(Hctx & H & Hpc)".
264 265 266 267 268 269
      wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
      iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
      iFrame "Hpc". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
  Qed.

  Lemma recv_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
270
    {{{ c  iProto_message Recv pc }}}
271 272
      recv c
    {{{ x, RET (pc x).1.1; c  (pc x).2  (pc x).1.2 }}}.
273
  Proof.
274 275 276 277
    iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
    wp_apply (try_recv_spec_packed with "Hc"); iIntros (v) "[[-> H]|H]".
    { wp_pures. by iApply ("IH" with "[$]"). }
    iDestruct "H" as (x ->) "[Hc Hpc]". wp_pures. iApply "HΦ". iFrame.
278 279
  Qed.

280 281
  (** A version written without Texan triples that is more convenient to use
  (via [iApply] in Coq. *)
282
  Lemma recv_spec {TT} Φ c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
283
    c  iProto_message Recv pc -
284 285
     (.. x : TT, c  (pc x).2 - (pc x).1.2 - Φ (pc x).1.1) -
    WP recv c {{ Φ }}.
286
  Proof.
287 288 289
    iIntros "Hc H". iApply (recv_spec_packed with "[$]").
    iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
    iApply ("H" with "[$] [$]").
290 291
  Qed.

292 293 294 295 296
  (** ** Specifications for branching *)
  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
    {{{ c  (p1 <{P1}+{P2}> p2)  if b then P1 else P2 }}}
      send c #b
    {{{ RET #(); c  (if b then p1 else p2) }}}.
297
  Proof.
298
    rewrite /iProto_branch. iIntros (Φ) "[Hc HP] HΦ".
299
    iApply (send_spec with "Hc"); simpl; eauto with iFrame.
300
  Qed.
301

302 303 304 305
  Lemma branch_spec c P1 P2 p1 p2 :
    {{{ c  (p1 <{P1}&{P2}> p2) }}}
      recv c
    {{{ b, RET #b; c  (if b : bool then p1 else p2)  if b then P1 else P2 }}}.
306
  Proof.
307
    rewrite /iProto_branch. iIntros (Φ) "Hc HΦ".
308
    iApply (recv_spec with "Hc"); simpl.
309
    iIntros "!>" (b) "Hc HP". iApply "HΦ". iFrame.
310
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
End channel.