channel.v 8.57 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(** This file contains the definition of the Channel language encoding,
being a pair of buffers, with the three message-passing primitives
[new_chan], [send] and [receive], along with their respective specifications.

The abstract representation of a channel endpoint is two buffer references
and a lock. [new_chan] creates references to two empty buffers and a lock, and
returns a pair of such endpoints, where the order of the two references
determines the polarity of the endpoints.

The [send] primitive takes such an endpoint abstraction and adds an element to
the first buffer under the lock. Conversely [recv] loops until there is
jihgfee's avatar
jihgfee committed
12 13
something in the second buffer, which it pops and returns, locking during
each peek.
14 15

The specifications are defined in terms of the logical connectives [is_chan]
jihgfee's avatar
jihgfee committed
16 17 18
and [chan_own], which respectively determines the contents of a channel using
a lock over an invariant and the ownership of it using ghost fragments
over buffers.
19
*)
20 21
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
From iris.algebra Require Import excl auth list.
23
From actris.utils Require Import auth_excl llist.
24 25
Set Default Proof Using "Type".

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

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

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

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

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

72 73 74 75 76 77 78 79
(** MOVE TO IRIS *)
Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V).
Proof.
  apply strongly_atomic_atomic, ectx_language_atomic;
    [inversion 1; naive_solver
    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
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
  }.

89
  (** The invariant of channels *)
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 115
  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 *)
116 117
  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.
118

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
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl []))) as (lsγ) "[Hls Hls']".
132
    { by apply auth_both_valid. }
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.
220

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