channel.v 10.7 KB
Newer Older
1
2
3
4
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
5
6
From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import auth.
7
8
From iris.heap_lang.lib Require Import spin_lock.
From osiris Require Import list.
9
From osiris Require Import auth_excl.
10
Set Default Proof Using "Type".
11
Import uPred.
12

13
Definition new_chan : val :=
14
  λ: <>,
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
15
16
     let: "l" := ref (lnil #()) in
     let: "r" := ref (lnil #()) in
17
18
     let: "lk" := newlock #() in
     (("l","r"),"lk").
19

20
21
22
Inductive side := Left | Right.
Coercion side_to_bool (s : side) : bool :=
  match s with Left => true | Right => false end.
23
24
25
26
27
28
29

Definition get_buffs c := Fst c.
Definition get_left c := Fst (get_buffs c).
Definition get_right c := Snd (get_buffs c).
Definition get_lock c := Snd c.

Definition dual_side s :=
30
  (if: s = #Left then #Right else #Left)%E.
31
32

Definition get_side c s :=
33
  (if: s = #Left then get_left c else get_right c)%E.
34
35
36

Definition send : val :=
  λ: "c" "s" "v",
37
38
39
40
41
    let: "lk" := get_lock "c" in
    acquire "lk";;
    let: "l" := get_side "c" "s" in
    "l" <- lsnoc !"l" "v";;
    release "lk".
42
43
44

Definition try_recv : val :=
  λ: "c" "s",
45
46
47
48
49
50
    let: "lk" := get_lock "c" in
    acquire "lk";;
    let: "l" := (get_side "c" (dual_side "s")) in
    match: !"l" with
      SOME "p" => "l" <- Snd "p";; release "lk";; SOME (Fst "p")
    | NONE => release "lk";; NONE
51
    end.
52
53
54
55
56
57
58
59
60

Definition recv : val :=
  rec: "go" "c" "s" :=
    match: try_recv "c" "s" with
      SOME "p" => "p"
    | NONE => "go" "c" "s"
    end.

Section channel.
61
  Context `{!heapG Σ, !lockG Σ, !auth_exclG (list val) Σ} (N : namespace).
62

63
  Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
64
    ( l':loc,  hd : val, l = #l'  l'  hd  is_list hd xs)%I.
65

66
67
68
69
70
71
72
73
74
  Record chan_name := Chan_name {
    chan_lock_name : gname;
    chan_l_name : gname;
    chan_r_name : gname
  }.

  Definition chan_ctx (γ : chan_name) (c : val) : iProp Σ :=
    ( l r lk : val,
      c = ((l, r), lk)%V 
75
      is_lock N (chan_lock_name γ) lk ( ls rs,
76
77
78
        is_list_ref l ls  own (chan_l_name γ) ( to_auth_excl ls) 
        is_list_ref r rs  own (chan_r_name γ) ( to_auth_excl rs)))%I.

79
80
81
  Global Instance chan_ctx_persistent : Persistent (chan_ctx γ c).
  Proof. by apply _. Qed.

82
  Definition chan_frag (γ : chan_name) (c : val) (ls rs : list val) : iProp Σ :=
83
84
    ( l r lk : val,
      c = ((l, r), lk)%V 
85
86
      own (chan_l_name γ) ( to_auth_excl ls) 
      own (chan_r_name γ) ( to_auth_excl rs))%I.
87

88
89
90
  Global Instance chan_frag_timeless : Timeless (chan_frag γ c ls rs).
  Proof. by apply _. Qed.

91
92
93
  Definition is_chan (γ : chan_name) (c : val) (ls rs : list val) : iProp Σ :=
    (chan_ctx γ c  chan_frag γ c ls rs)%I.

94
95
  Lemma new_chan_spec :
    {{{ True }}}
96
      new_chan #()
97
    {{{ c γ, RET c; is_chan γ c [] [] }}}.
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
  Proof.
    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_ctx /chan_frag.
    wp_lam.
    wp_apply (lnil_spec with "[//]"); iIntros (ls Hls). wp_alloc l as "Hl".
    wp_apply (lnil_spec with "[//]"); iIntros (rs Hrs). wp_alloc r as "Hr".
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl [])))
      as (lsγ) "[Hls Hls']"; first done.
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl [])))
      as (rsγ) "[Hrs Hrs']"; first done.
    iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
    { rewrite /is_list_ref; eauto. }
    iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
    { rewrite /is_list_ref; eauto. }
    wp_apply (newlock_spec N ( ls rs,
      is_list_ref #l ls  own lsγ ( to_auth_excl ls) 
      is_list_ref #r rs  own rsγ ( to_auth_excl rs))%I
                with "[Hl Hr Hls Hrs]").
    { eauto 10 with iFrame. }
    iIntros (lk γlk) "#Hlk". wp_pures.
    iApply ("HΦ" $! _ (Chan_name γlk lsγ rsγ)).
    eauto 20 with iFrame.
119
120
  Qed.

121
122
123
  Definition chan_frag_snoc (γ : chan_name) (c : val)
             (l r : list val) (s : side) (v : val)
    : iProp Σ :=
124
    match s with
125
126
    | Left  => chan_frag γ c (l ++ [v]) r
    | Right => chan_frag γ c l (r ++ [v])
127
128
    end.

129
  Lemma send_spec Φ E γ c v s :
130
    chan_ctx γ c -
131
132
133
    (|={,E}=>  ls rs,
      chan_frag γ c ls rs 
       (chan_frag_snoc γ c ls rs s v ={E,}= Φ #())) -
134
    WP send c #s v {{ Φ }}.
135
  Proof.
136
    iIntros "Hc HΦ". wp_lam; wp_pures.
137
138
139
    iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
    iDestruct "Hinv" as (ls rs) "(Hl & Hls & Hr & Hrs)".
140
    destruct s.
141
142
    - wp_pures. iDestruct "Hl" as (ll lhd ->) "(Hl & Hll)".
      wp_load. wp_apply (lsnoc_spec with "Hll").
143
      iIntros (hd' Hll).
144
      wp_bind (_ <- _)%E. iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
145
146
147
      iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hls' Hrs']".
      iDestruct (excl_eq with "Hls Hls'") as %->.
      iMod (excl_update _ _ _ (ls ++ [v]) with "Hls Hls'") as "[Hls Hls']".
148
      wp_store.
149
      iMod ("HΦ" with "[Hls' Hrs']") as "HΦ".
150
      { rewrite /= /chan_frag. eauto with iFrame. }
151
      iModIntro.
152
      wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
153
154
155
      { rewrite /is_list_ref. eauto 10 with iFrame. }
    - wp_pures. iDestruct "Hr" as (lr rhd ->) "(Hr & Hlr)".
      wp_load. wp_apply (lsnoc_spec with "Hlr").
156
      iIntros (hd' Hlr). wp_pures.
157
158
      wp_bind (_ <- _)%E. iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
      wp_store.
159
160
161
162
      iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hls' Hrs']".
      iDestruct (excl_eq with "Hrs Hrs'") as %->.
      iMod (excl_update _ _ _ (rs ++ [v]) with "Hrs Hrs'") as "[Hrs Hrs']".
      iMod ("HΦ" with "[Hls' Hrs']") as "HΦ".
163
      { rewrite /= /chan_frag. eauto with iFrame. }
164
      iModIntro.
165
      wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
166
      { rewrite /is_list_ref. eauto 10 with iFrame. }
167
168
  Qed.

169
170
  Definition try_recv_fail (γ : chan_name) (c : val)
             (l r : list val) (s : side) : iProp Σ :=
171
    match s with
172
173
    | Left  => (chan_frag γ c l r  r = [])%I
    | Right => (chan_frag γ c l r  l = [])%I
174
    end.
175

176
177
  Definition try_recv_succ (γ : chan_name) (c : val)
             (l r : list val) (s : side) (v : val) : iProp Σ :=
178
    match s with
179
180
    | Left =>  ( r', chan_frag γ c l  r'  r = v::r')%I
    | Right => ( l', chan_frag γ c l' r   l = v::l')%I
181
182
    end.

183
  Lemma try_recv_spec Φ E γ c s :
184
    chan_ctx γ c -
185
186
    (|={,E}=>  ls rs,
      chan_frag γ c ls rs 
187
188
189
       ((try_recv_fail γ c ls rs s ={E,}= Φ NONEV) 
         ( v, try_recv_succ γ c ls rs s v ={E,}= Φ (SOMEV v)))) -
    WP try_recv c #s {{ Φ }}.
190
  Proof.
191
    iIntros "Hc HΦ". wp_lam; wp_pures.
192
193
194
    iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
    iDestruct "Hinv" as (ls rs) "(Hls & Hlsa & Hrs & Hrsa)".
195
    destruct s; simpl.
196
    - iDestruct "Hrs" as (rl rhd ->) "[Hrs #Hrhd]".
197
198
199
      wp_pures.
      wp_bind (Load _).
      iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
200
      wp_load.
201
202
      destruct rs; simpl.
      + iDestruct "Hrhd" as %->.
203
204
205
        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
206
        iDestruct "HΦ" as "[HΦ _]".
207
        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
208
        { rewrite /try_recv_fail /chan_frag.
209
          eauto 10 with iFrame. }
210
        iModIntro.
211
212
213
        wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
        { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
        iIntros (_).
214
        wp_pures.
215
        by iApply "HΦ".
216
      + iDestruct "Hrhd" as %[hd' [-> Hrhd']].
217
218
219
220
        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
        iDestruct (excl_update _ _ _ (rs) with "Hrsa Hrsf") as ">[Hrsa Hrsf]".
221
        iDestruct "HΦ" as "[_ HΦ]".
222
        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
223
        { rewrite /try_recv_succ /chan_frag.
224
          eauto 10 with iFrame. }
225
        iModIntro.
226
227
228
229
        wp_store.
        wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
        { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
        iIntros (_).
230
        wp_pures.
231
232
        by iApply "HΦ".
    - iDestruct "Hls" as (ll lhd ->) "[Hls #Hlhd]".
233
234
235
      wp_pures.
      wp_bind (Load _).
      iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
236
      wp_load.
237
238
      destruct ls; simpl.
      + iDestruct "Hlhd" as %->.
239
240
241
        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
242
        iDestruct "HΦ" as "[HΦ _]".
243
        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
244
        { rewrite /try_recv_fail /chan_frag.
245
          eauto 10 with iFrame. }
246
        iModIntro.
247
248
249
        wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
        { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
        iIntros (_).
250
        wp_pures.
251
        by iApply "HΦ".
252
      + iDestruct "Hlhd" as %[hd' [-> Hlhd']].
253
254
255
256
        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
        iDestruct (excl_update _ _ _ (ls) with "Hlsa Hlsf") as ">[Hlsa Hlsf]".
257
        iDestruct "HΦ" as "[_ HΦ]".
258
        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
259
        { rewrite /try_recv_succ /chan_frag. eauto 10 with iFrame. }
260
        iModIntro.
261
262
263
264
265
266
267
        wp_store.
        wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
        { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
        iIntros (_).
        wp_pures.
        by iApply "HΦ".
  Qed.
268

269
270
  Lemma recv_spec Φ E γ c s :
    chan_ctx γ c -
271
272
    ( (|={,E}=>  ls rs,
      chan_frag γ c ls rs 
273
274
         ((try_recv_fail γ c ls rs s ={E,}= True) 
          ( v, try_recv_succ γ c ls rs s v ={E,}= Φ v)))) -
275
    WP recv c #s {{ Φ }}.
276
  Proof.
277
    iIntros "#Hc #HΦ".
278
279
280
    rewrite /recv.
    iLöb as "IH".
    wp_apply (try_recv_spec with "Hc")=> //.
281
    iMod "HΦ" as (ls rs) "[Hchan [HΦfail HΦsucc]]".
282
    iModIntro.
283
    iExists _, _.
284
    iFrame.
285
    iNext.
286
287
288
    iSplitL "HΦfail".
    - iIntros "Hupd".
      iDestruct ("HΦfail") as "HΦ".
289
290
291
      iMod ("HΦ" with "Hupd") as "HΦ".
      iModIntro.
      wp_match.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
292
      by iApply ("IH").
293
294
    - iDestruct ("HΦsucc") as "HΦ".
      iIntros (v) "Hupd".
295
296
297
      iSpecialize("HΦ" $!v).
      iMod ("HΦ" with "Hupd") as "HΦ".
      iModIntro.
Jonas Kastberg Hinrichsen's avatar
Jonas Kastberg Hinrichsen committed
298
      by wp_pures.
299
  Qed.
300
End channel.