concurrent_stack2.v 13.7 KB
Newer Older
1
From iris.heap_lang Require Import notation proofmode.
2
From iris.algebra Require Import excl.
3 4
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Export weakestpre.
Daniel Gratzer's avatar
Daniel Gratzer committed
5
From iris_examples.concurrent_stacks Require Import specs.
6 7
Set Default Proof Using "Type".

Daniel Gratzer's avatar
Daniel Gratzer committed
8 9
(** Stack 2: Helping, bag spec. *)

10 11 12 13 14 15 16
Definition mk_offer : val :=
  λ: "v", ("v", ref #0).
Definition revoke_offer : val :=
  λ: "v", if: CAS (Snd "v") #0 #2 then SOME (Fst "v") else NONE.
Definition take_offer : val :=
  λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE.

17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
Definition mk_mailbox : val := λ: "_", ref NONEV.
Definition put : val :=
  λ: "r" "v",
    let: "off" := mk_offer "v" in
    "r" <- SOME "off";;
    revoke_offer "off".

Definition get : val :=
  λ: "r",
    let: "offopt" := !"r" in
    match: "offopt" with
      NONE => NONE
    | SOME "x" => take_offer "x"
    end.

Daniel Gratzer's avatar
Daniel Gratzer committed
32
Definition new_stack : val := λ: "_", (mk_mailbox #(), ref NONEV).
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
Definition push : val :=
  rec: "push" "p" "v" :=
    let: "mailbox" := Fst "p" in
    let: "s" := Snd "p" in
    match: put "mailbox" "v" with
      NONE => #()
    | SOME "v'" =>
      let: "tail" := ! "s" in
      let: "new" := SOME (ref ("v'", "tail")) in
      if: CAS "s" "tail" "new" then #() else "push" "p" "v'"
    end.
Definition pop : val :=
  rec: "pop" "p" :=
    let: "mailbox" := Fst "p" in
    let: "s" := Snd "p" in
    match: get "mailbox" with
      NONE =>
      match: !"s" with
        NONE => NONEV
      | SOME "l" =>
        let: "pair" := !"l" in
        if: CAS "s" (SOME "l") (Snd "pair")
        then SOME (Fst "pair")
        else "pop" "p"
      end
    | SOME "x" => SOME "x"
    end.
60 61 62 63 64 65 66 67

Definition channelR := exclR unitR.
Class channelG Σ := { channel_inG :> inG Σ channelR }.
Definition channelΣ : gFunctors := #[GFunctor channelR].
Instance subG_channelΣ {Σ} : subG channelΣ Σ  channelG Σ.
Proof. solve_inG. Qed.

Section side_channel.
68
  Context `{!heapG Σ, !channelG Σ} (N : namespace).
69 70
  Implicit Types l : loc.

71 72
  Definition revoke_tok γ := own γ (Excl ()).

73 74 75
  Definition stages γ (P : val  iProp Σ) l v :=
    ((l  #0  P v)
      (l  #1)
76
      (l  #2  revoke_tok γ))%I.
77 78

  Definition is_offer γ (P : val  iProp Σ) (v : val) : iProp Σ :=
79
    ( v' l, v = (v', #l)%V  inv N (stages γ P l v'))%I.
80

81 82 83 84 85 86 87 88 89
  Lemma mk_offer_works P v :
    {{{ P v }}} mk_offer v {{{ o γ, RET o; is_offer γ P o  revoke_tok γ }}}.
  Proof.
    iIntros (Φ) "HP HΦ".
    rewrite -wp_fupd.
    wp_lam. wp_alloc l as "Hl".
    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
    iMod (inv_alloc N _ (stages γ P l v) with "[Hl HP]") as "#Hinv".
    { iNext; iLeft; iFrame. }
90
    wp_pures; iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto.
91
  Qed.
92 93

  (* A partial specification for revoke that will be useful later *)
94 95 96 97
  Lemma revoke_works γ P v :
    {{{ is_offer γ P v  revoke_tok γ }}}
      revoke_offer v
    {{{ v', RET v'; ( v'' : val, v' = InjRV v''  P v'')  v' = InjLV #() }}}.
98
  Proof.
99
    iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
100
    wp_lam. wp_bind (CmpXchg _ _ _). wp_pures.
101
    iInv N as "Hstages" "Hclose".
102
    iDestruct "Hstages" as "[[Hl HP] | [H | [Hl H]]]".
103
    - wp_cmpxchg_suc.
104 105
      iMod ("Hclose" with "[Hl Hγ]") as "_".
      { iRight; iRight; iFrame. }
106
      iModIntro.
107
      wp_pures.
108
      by iApply "HΦ"; iLeft; iExists _; iSplit.
109
    - wp_cmpxchg_fail.
110 111
      iMod ("Hclose" with "[H]") as "_".
      { iRight; iLeft; auto. }
112
      iModIntro.
113
      wp_pures.
114
      by iApply "HΦ"; iRight.
115
    - wp_cmpxchg_fail.
116
      iDestruct (own_valid_2 with "H Hγ") as %[].
117 118 119
  Qed.

  (* A partial specification for take that will be useful later *)
120 121 122 123
  Lemma take_works γ P o :
    {{{ is_offer γ P o }}}
      take_offer o
    {{{ v', RET v'; ( v'' : val, v' = InjRV v''  P v'')  v' = InjLV #() }}}.
124
  Proof.
125
    iIntros (Φ) "H HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
126
    wp_lam. wp_proj. wp_bind (CmpXchg _ _ _).
127
    iInv N as "Hstages" "Hclose".
128
    iDestruct "Hstages" as "[[H HP] | [H | [Hl Hγ]]]".
129
    - wp_cmpxchg_suc.
130 131
      iMod ("Hclose" with "[H]") as "_".
      { by iRight; iLeft. }
132
      iModIntro.
133
      wp_pures.
134
      iApply "HΦ"; iLeft; auto.
135
    - wp_cmpxchg_fail.
136 137
      iMod ("Hclose" with "[H]") as "_".
      { by iRight; iLeft. }
138
      iModIntro.
139
      wp_pures.
140
      iApply "HΦ"; auto.
141
    - wp_cmpxchg_fail.
142
      iMod ("Hclose" with "[Hl Hγ]").
143
      { iRight; iRight; iFrame. }
144
      iModIntro.
145
      wp_pures.
146
      iApply "HΦ"; auto.
147 148 149 150
  Qed.
End side_channel.

Section mailbox.
151
  Context `{!heapG Σ, channelG Σ} (N : namespace).
152 153
  Implicit Types l : loc.

154 155 156 157 158 159 160 161 162 163
  Definition Noffer := N .@ "offer".

  Definition mailbox_inv (P : val  iProp Σ) (l : loc) : iProp Σ :=
    (l  NONEV  ( v' γ, l  SOMEV v'  is_offer Noffer γ P v'))%I.

  Definition is_mailbox (P : val  iProp Σ) (v : val) : iProp Σ :=
    ( l, v = #l  inv N (mailbox_inv P l))%I.

  Theorem mk_mailbox_works (P : val  iProp Σ) :
    {{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}.
164
  Proof.
165
    iIntros (Φ) "_ HΦ".
166 167 168
    rewrite -wp_fupd.
    wp_lam.
    wp_alloc l as "Hl".
169 170
    iMod (inv_alloc N _ (mailbox_inv P l) with "[Hl]") as "#Hinv".
    { by iNext; iLeft. }
171
    iModIntro.
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
    iApply "HΦ"; iExists _; eauto.
  Qed.

  Theorem get_works (P : val  iProp Σ) mailbox :
    {{{ is_mailbox P mailbox }}}
      get mailbox
    {{{ ov, RET ov; ov = NONEV   v, ov = SOMEV v  P v}}}.
  Proof.
    iIntros (Φ) "H HΦ". iDestruct "H" as (l) "[-> #Hinv]".
    wp_lam. wp_bind (Load _).
    iInv N as "[Hnone | Hsome]" "Hclose".
    - wp_load.
      iMod ("Hclose" with "[Hnone]") as "_".
      { by iNext; iLeft. }
      iModIntro.
187
      wp_pures.
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
      iApply "HΦ"; auto.
    - iDestruct "Hsome" as (v' γ) "[Hl #Hoffer]".
      wp_load.
      iMod ("Hclose" with "[Hl]") as "_".
      { by iNext; iRight; iExists _, _; iFrame. }
      iModIntro.
      wp_let. wp_match.
      iApply (take_works with "Hoffer").
      iNext; iIntros (offer) "[Hsome | Hnone]".
      * iDestruct "Hsome" as (v'') "[-> HP]".
        iApply ("HΦ" with "[HP]"); iRight; auto.
      * iApply "HΦ"; iLeft; auto.
  Qed.

  Theorem put_works (P : val  iProp Σ) (mailbox v : val) :
    {{{ is_mailbox P mailbox  P v }}}
      put mailbox v
    {{{ o, RET o; ( v', o = SOMEV v'  P v')  o = NONEV }}}.
  Proof.
    iIntros (Φ) "[Hmailbox HP] HΦ"; iDestruct "Hmailbox" as (l) "[-> #Hmailbox]".
    wp_lam. wp_let. wp_apply (mk_offer_works with "HP").
    iIntros (offer γ) "[#Hoffer Hrevoke]".
210
    wp_let. wp_bind (Store _ _). wp_pures.
211 212 213 214
    iInv N as "[HNone | HSome]" "Hclose".
    - wp_store.
      iMod ("Hclose" with "[HNone]") as "_".
      { by iNext; iRight; iExists _, _; iFrame. }
215
      iModIntro.
216
      wp_pures.
217 218 219 220 221 222 223 224 225
      wp_apply (revoke_works with "[Hrevoke]"); first by iFrame.
      iIntros (v') "H"; iDestruct "H" as "[HSome | HNone]".
      * iApply ("HΦ" with "[HSome]"); by iLeft.
      * iApply ("HΦ" with "[HNone]"); by iRight.
    - iDestruct "HSome" as (v' γ') "[Hl #Hoffer']".
      wp_store.
      iMod ("Hclose" with "[Hl]") as "_".
      { by iNext; iRight; iExists _, _; iFrame. }
      iModIntro.
226
      wp_pures.
227 228 229 230
      wp_apply (revoke_works with "[Hrevoke]"); first by iFrame.
      iIntros (v'') "H"; iDestruct "H" as "[HSome | HNone]".
      * iApply ("HΦ" with "[HSome]"); by iLeft.
      * iApply ("HΦ" with "[HNone]"); by iRight.
231 232 233 234
  Qed.
End mailbox.

Section stack_works.
235
  Context `{!heapG Σ, channelG Σ} (N : namespace).
236 237
  Implicit Types l : loc.

238 239 240 241 242 243 244 245 246 247 248
  Definition Nmailbox := N .@ "mailbox".

  Local Notation "l ↦{-} v" := ( q, l {q} v)%I
    (at level 20, format "l  ↦{-}  v") : bi_scope.

  Lemma partial_mapsto_duplicable l v :
    l {-} v - l {-} v  l {-} v.
  Proof.
    iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
  Qed.

249 250 251 252 253 254 255 256 257 258 259 260 261
  Definition oloc_to_val (ol: option loc) : val :=
    match ol with
    | None => NONEV
    | Some loc => SOMEV (#loc)
    end.
  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
  Proof. intros [|][|]; simpl; congruence. Qed.

  Definition is_list_pre (P : val  iProp Σ) (F : option loc -d> iProp Σ) :
     option loc -d> iProp Σ := λ v, match v with
     | None => True
     | Some l =>  (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V  P h   F t
     end%I.
262

263
  Local Instance is_list_contr (P : val  iProp Σ) : Contractive (is_list_pre P).
264
  Proof.
265
    rewrite /is_list_pre => n f f' Hf v.
266 267 268 269
    repeat (f_contractive || f_equiv).
    apply Hf.
  Qed.

270 271 272 273
  Definition is_list_def (P : val -> iProp Σ) := fixpoint (is_list_pre P).
  Definition is_list_aux P : seal (@is_list_def P). by eexists. Qed.
  Definition is_list P := unseal (is_list_aux P).
  Definition is_list_eq P : @is_list P = @is_list_def P := seal_eq (is_list_aux P).
274

275 276 277 278 279
  Lemma is_list_unfold (P : val  iProp Σ) v :
    is_list P v ⊣⊢ is_list_pre P (is_list P) v.
  Proof.
    rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
  Qed.
280

281 282 283 284 285
  Lemma is_list_dup (P : val  iProp Σ) v :
    is_list P v - is_list P v  match v with
      | None => True
      | Some l =>  h t, l {-} (h, oloc_to_val t)%V
      end.
286
  Proof.
287 288 289 290 291 292
    iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
    destruct v as [l|].
    - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
      rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
    - rewrite is_list_unfold; iSplitR; eauto.
293 294
  Qed.

295
  Definition stack_inv P l := ( v, l  oloc_to_val v  is_list P v)%I.
296 297 298
  Definition is_stack P v :=
    ( mailbox l, v = (mailbox, #l)%V  is_mailbox Nmailbox P mailbox  inv N (stack_inv P l))%I.

Daniel Gratzer's avatar
Daniel Gratzer committed
299 300
  Theorem new_stack_spec P :
    {{{ True }}} new_stack #() {{{ v, RET v; is_stack P v }}}.
301
  Proof.
Daniel Gratzer's avatar
Daniel Gratzer committed
302
    iIntros (ϕ) "_ Hpost".
303
    rewrite -wp_fupd.
304
    wp_lam.
305
    wp_alloc l as "Hl".
306 307 308
    wp_apply mk_mailbox_works; first done.
    iIntros (mailbox) "#Hmailbox".
    iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv".
309
    { iNext; iExists None; iFrame. rewrite is_list_unfold. done. }
Daniel Gratzer's avatar
Daniel Gratzer committed
310
    wp_pures; iModIntro; iApply "Hpost"; iExists _, _; auto.
311 312
  Qed.

Daniel Gratzer's avatar
Daniel Gratzer committed
313
  Theorem push_spec P s v :
314 315 316 317 318 319 320 321 322 323 324 325 326 327 328
    {{{ is_stack P s  P v }}} push s v {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "[Hstack HP] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
    iLöb as "IH" forall (v).
    wp_lam. wp_let. wp_proj. wp_let. wp_proj. wp_let.
    wp_apply (put_works _ P with "[HP]"); first by iFrame.
    iIntros (result) "Hopt".
    iDestruct "Hopt" as "[HSome | ->]".
    - iDestruct "HSome" as (v') "[-> HP]".
      wp_match. wp_bind (Load _).
      iInv N as (v'') "[Hl Hlist]" "Hclose".
      wp_load.
      iMod ("Hclose" with "[Hl Hlist]") as "_".
      { iNext; iExists _; iFrame. }
      iModIntro.
329
      wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
330 331
      iInv N as (list) "(Hl & Hlist)" "Hclose".
      destruct (decide (v'' = list)) as [ -> |].
332
      * wp_cmpxchg_suc. { destruct list; left; done. }
333
        iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
334 335
        { iNext; iExists (Some _); iFrame.
          rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
336
        iModIntro.
337
        wp_pures.
338
        by iApply "HΦ".
339
      * wp_cmpxchg_fail.
340 341
        { destruct list, v''; simpl; congruence. }
        { destruct list; left; done. }
342 343
        iMod ("Hclose" with "[Hl Hlist]") as "_".
        { iNext; iExists _; by iFrame. }
344
        iModIntro.
345
        wp_pures.
346 347 348 349 350
        iApply ("IH" with "HP HΦ").
    - wp_match.
      by iApply "HΦ".
  Qed.

Daniel Gratzer's avatar
Daniel Gratzer committed
351
  Theorem pop_spec P s :
352 353 354 355
    {{{ is_stack P s }}} pop s {{{ ov, RET ov; ov = NONEV   v, ov = SOMEV v  P v }}}.
  Proof.
    iIntros (Φ) "Hstack HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hstack)".
    iLöb as "IH".
356
    wp_lam. wp_proj. wp_let. wp_proj. wp_pures.
357 358 359 360 361
    wp_apply get_works; first done.
    iIntros (ov) "[-> | HSome]".
    - wp_match. wp_bind (Load _).
      iInv N as (list) "[Hl Hlist]" "Hclose".
      wp_load.
362
      iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
363 364 365
      iMod ("Hclose" with "[Hl Hlist]") as "_".
      { iNext; iExists _; by iFrame. }
      iModIntro.
366
      destruct list as [list|]; last first.
367 368
      * wp_match.
        iApply "HΦ"; by iLeft.
369
      * wp_match. wp_bind (Load _).
370
        iInv N as (v') "[>Hl Hlist]" "Hclose".
371
        iDestruct "Hlist2" as (???) "Hl'".
372
        wp_load.
373 374
        iMod ("Hclose" with "[Hl Hlist]") as "_".
        { iNext; iExists _; by iFrame. }
375
        iModIntro.
376
        wp_let. wp_proj. wp_bind (CmpXchg _ _ _). wp_pures.
377
        iInv N as (v'') "[Hl Hlist]" "Hclose".
378
        destruct (decide (v'' = Some list)) as [-> |].
379
        + rewrite is_list_unfold.
380
          iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
381
          iDestruct "Hl''" as (q') "Hl''".
382
          wp_cmpxchg_suc.
383 384 385
          iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
          iMod ("Hclose" with "[Hl Hlist]") as "_".
          { iNext; iExists _; by iFrame. }
386
          iModIntro.
387
          wp_pures.
388
          iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
389
        + wp_cmpxchg_fail. { destruct v''; simpl; congruence. }
390 391
          iMod ("Hclose" with "[Hl Hlist]") as "_".
          { iNext; iExists _; by iFrame. }
392
          iModIntro.
393
          wp_pures.
394 395
          iApply ("IH" with "HΦ").
    - iDestruct "HSome" as (v) "[-> HP]".
396
      wp_pures.
397
      iApply "HΦ"; iRight; iExists _; auto.
398 399
  Qed.
End stack_works.
Daniel Gratzer's avatar
Daniel Gratzer committed
400

401 402
Program Definition spec {Σ} N `{heapG Σ, channelG Σ} : concurrent_bag Σ :=
  {| is_bag := is_stack N; new_bag := new_stack; bag_push := push; bag_pop := pop |} .
Daniel Gratzer's avatar
Daniel Gratzer committed
403
Solve Obligations of spec with eauto using pop_spec, push_spec, new_stack_spec.