channel.v 7.5 KB
Newer Older
1 2
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.algebra Require Import excl auth list.
4
From actris.utils Require Import auth_excl llist.
5 6
Set Default Proof Using "Type".

Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11
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.

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

Definition send : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
  λ: "c" "v",
    let: "lk" := Snd "c" in
22
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
23
    let: "l" := Fst (Fst "c") in
24
    lsnoc "l" "v";;
25
    release "lk".
26 27

Definition try_recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29
  λ: "c",
    let: "lk" := Snd "c" in
30
    acquire "lk";;
Robbert Krebbers's avatar
Robbert Krebbers committed
31
    let: "l" := Snd (Fst "c") in
32
    let: "ret" := if: lisnil "l" then NONE else SOME (lpop "l") in
33
    release "lk";; "ret".
34 35

Definition recv : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37
  rec: "go" "c" :=
    match: try_recv "c" with
38
      SOME "p" => "p"
Robbert Krebbers's avatar
Robbert Krebbers committed
39
    | NONE => "go" "c"
40 41
    end.

42 43
Class chanG Σ := {
  chanG_lockG :> lockG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  chanG_authG :> auth_exclG (listO valO) Σ;
45 46
}.
Definition chanΣ : gFunctors :=
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  #[ lockΣ; auth_exclΣ (constOF (listO valO)) ].
48 49 50
Instance subG_chanΣ {Σ} : subG chanΣ Σ  chanG Σ.
Proof. solve_inG. Qed.

51 52 53 54 55 56 57 58
(** 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.

59
Section channel.
60
  Context `{!heapG Σ, !chanG Σ} (N : namespace).
61

62 63 64 65 66 67
  Record chan_name := Chan_name {
    chan_lock_name : gname;
    chan_l_name : gname;
    chan_r_name : gname
  }.

68
  Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
69
    ( ls rs,
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
      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.
72 73
  Typeclasses Opaque chan_inv.

Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
75 76
    ( (l r : loc) (lk : val),
       c1 = ((#l, #r), lk)%V  c2 = ((#r, #l), lk)%V  
77
      is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
78

Robbert Krebbers's avatar
Robbert Krebbers committed
79
  Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
80 81
  Proof. by apply _. Qed.

82 83
  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.
84

85
  Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
86 87
  Proof. by apply _. Qed.

88 89
  Lemma new_chan_spec :
    {{{ True }}}
90
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    {{{ c1 c2 γ, RET (c1,c2); is_chan γ c1 c2  chan_own γ Left []  chan_own γ Right [] }}}.
92
  Proof.
93
    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
94
    wp_lam.
95 96
    wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
    wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
97 98 99 100
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl []))) as (lsγ) "[Hls Hls']".
    { by apply auth_both_valid. }
    iMod (own_alloc ( (to_auth_excl [])   (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
    { by apply auth_both_valid. }
101
    wp_apply (newlock_spec N ( ls rs,
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103
      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]").
104 105
    { eauto 10 with iFrame. }
    iIntros (lk γlk) "#Hlk". wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
    iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
107
    rewrite /chan_inv /=. eauto 20 with iFrame.
108 109
  Qed.

110 111
  Lemma chan_inv_alt s γ l r :
    chan_inv γ l r   ls rs,
Robbert Krebbers's avatar
Robbert Krebbers committed
112
      llist sbi_internal_eq (side_elim s l r) ls 
113
      own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl ls) 
Robbert Krebbers's avatar
Robbert Krebbers committed
114
      llist sbi_internal_eq (side_elim s r l) rs 
115 116 117 118 119
      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.
120

Robbert Krebbers's avatar
Robbert Krebbers committed
121 122
  Lemma send_spec Φ E γ c1 c2 v s :
    is_chan γ c1 c2 -
123 124
    (|={,E}=>  vs,
      chan_own γ s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
       (chan_own γ s (vs ++ [v]) ={E,}=   Φ #())) -
    WP send (side_elim s c1 c2) v {{ Φ }}.
127
  Proof.
128
    iIntros "Hc HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
130 131
    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).
132
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
133
    iDestruct (chan_inv_alt s with "Hinv") as
134 135
      (vs ws) "(Hll & Hvs & Href' & Hws)".
    wp_seq. wp_bind (Fst (_,_)%V)%E.
136
    iMod "HΦ" as (vs') "[Hchan HΦ]".
137
    iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
138
    iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
139
    wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
    wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
141 142
    wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
    iApply (chan_inv_alt s).
143
    rewrite /llist. eauto 20 with iFrame.
144 145
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
146 147 148 149 150 151 152 153
  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) {{ Φ }}.
154
  Proof.
155
    iIntros "Hc HΦ". wp_lam; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
    iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
157 158
    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
159 160
    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
    iDestruct (chan_inv_alt s with "Hinv")
161 162 163 164
      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.
165
      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
Robbert Krebbers's avatar
Robbert Krebbers committed
166
      { iApply (chan_inv_alt s).
167
        rewrite /llist. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170 171
      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']".
172 173
      wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
      wp_apply (lisnil_spec with "Hll"); iIntros "Hll".
Robbert Krebbers's avatar
Robbert Krebbers committed
174
      wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
175
      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
Robbert Krebbers's avatar
Robbert Krebbers committed
176
      { iApply (chan_inv_alt s).
177
        rewrite /llist. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
178
      iIntros (_). by wp_pures.
179
  Qed.
180

Robbert Krebbers's avatar
Robbert Krebbers committed
181 182 183 184 185 186 187
  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) {{ Φ }}.
188
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
189 190 191 192 193 194 195
    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.
196
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
End channel.