concurrent_stack2.v 13.4 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.
5 6 7 8 9 10 11 12 13
Set Default Proof Using "Type".

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.

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
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.

Definition mk_stack : val := λ: "_", (mk_mailbox #(), ref NONEV).
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.
57 58 59 60 61 62 63 64

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.
65
  Context `{!heapG Σ, !channelG Σ} (N : namespace).
66 67
  Implicit Types l : loc.

68 69
  Definition revoke_tok γ := own γ (Excl ()).

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

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

78 79 80 81 82 83 84 85 86 87 88
  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. }
    iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto.
  Qed.
89 90

  (* A partial specification for revoke that will be useful later *)
91 92 93 94
  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 #() }}}.
95
  Proof.
96 97
    iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
    wp_let. wp_proj. wp_bind (CAS _ _ _).
98
    iInv N as "Hstages" "Hclose".
99 100 101 102
    iDestruct "Hstages" as "[[Hl HP] | [H | [Hl H]]]".
    - wp_cas_suc.
      iMod ("Hclose" with "[Hl Hγ]") as "_".
      { iRight; iRight; iFrame. }
103
      iModIntro.
104 105
      wp_if. wp_proj.
      by iApply "HΦ"; iLeft; iExists _; iSplit.
106
    - wp_cas_fail.
107 108
      iMod ("Hclose" with "[H]") as "_".
      { iRight; iLeft; auto. }
109 110
      iModIntro.
      wp_if.
111 112 113
      by iApply "HΦ"; iRight.
    - wp_cas_fail.
      iDestruct (own_valid_2 with "H Hγ") as %[].
114 115 116
  Qed.

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

Section mailbox.
148
  Context `{!heapG Σ, channelG Σ} (N : namespace).
149 150
  Implicit Types l : loc.

151 152 153 154 155 156 157 158 159 160
  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 }}}.
161
  Proof.
162
    iIntros (Φ) "_ HΦ".
163 164 165
    rewrite -wp_fupd.
    wp_lam.
    wp_alloc l as "Hl".
166 167
    iMod (inv_alloc N _ (mailbox_inv P l) with "[Hl]") as "#Hinv".
    { by iNext; iLeft. }
168
    iModIntro.
169 170 171 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
    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.
      wp_let. wp_match.
      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]".
    wp_let. wp_bind (Store _ _).
    iInv N as "[HNone | HSome]" "Hclose".
    - wp_store.
      iMod ("Hclose" with "[HNone]") as "_".
      { by iNext; iRight; iExists _, _; iFrame. }
212 213
      iModIntro.
      wp_let.
214 215 216 217 218 219 220 221 222 223 224 225 226 227
      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.
      wp_let.
      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.
228 229 230 231
  Qed.
End mailbox.

Section stack_works.
232
  Context `{!heapG Σ, channelG Σ} (N : namespace).
233 234
  Implicit Types l : loc.

235 236 237 238 239 240 241 242 243 244 245 246
  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.

  Definition is_list_pre (P : val  iProp Σ) (F : val -c> iProp Σ) :
247
     val -c> iProp Σ := λ v,
248
    (v  NONEV   (l : loc) (h t : val), v  SOMEV #l  l {-} (h, t)%V  P h   F t)%I.
249

250
  Local Instance is_list_contr (P : val  iProp Σ) : Contractive (is_list_pre P).
251
  Proof.
252
    rewrite /is_list_pre => n f f' Hf v.
253 254 255 256
    repeat (f_contractive || f_equiv).
    apply Hf.
  Qed.

257 258 259 260
  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).
261

262 263 264 265 266
  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.
267

268 269 270
  (* TODO: shouldn't have to explicitly return is_list *)
  Lemma is_list_unboxed (P : val  iProp Σ) v :
      is_list P v - val_is_unboxed v  is_list P v.
271
  Proof.
272 273 274
    iIntros "Hstack"; iSplit; last done;
    iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
    last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
275 276
  Qed.

277 278
  Lemma is_list_disj (P : val  iProp Σ) v :
    is_list P v - is_list P v  (v  NONEV   (l : loc) h t, v  SOMEV #l%V  l {-} (h, t)%V).
279 280
  Proof.
    iIntros "Hstack".
281 282 283 284 285
    iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
    - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
    - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
      rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
286 287
  Qed.

288 289 290 291 292 293
  Definition stack_inv P l := ( v, l  v  is_list P v)%I.
  Definition is_stack P v :=
    ( mailbox l, v = (mailbox, #l)%V  is_mailbox Nmailbox P mailbox  inv N (stack_inv P l))%I.

  Theorem mk_stack_works P :
    WP mk_stack #() {{ v, is_stack P v }}%I.
294
  Proof.
295
    rewrite -wp_fupd.
296
    wp_lam.
297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336
    wp_apply mk_mailbox_works; first done.
    iIntros (mailbox) "#Hmailbox".
    wp_alloc l as "Hl".
    iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv".
    { by iNext; iExists _; iFrame; rewrite is_list_unfold; iLeft. }
    iModIntro.
    iExists _, _; auto.
  Qed.

  Theorem push_works P s v :
    {{{ 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.
      wp_let. wp_alloc l' as "Hl'". wp_let. wp_bind (CAS _ _ _).
      iInv N as (list) "(Hl & Hlist)" "Hclose".
      destruct (decide (v'' = list)) as [ -> |].
      * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
        wp_cas_suc.
        iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
        { iNext; iExists (SOMEV _); iFrame.
          rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
        iModIntro.
        wp_if.
        by iApply "HΦ".
      * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
        wp_cas_fail.
        iMod ("Hclose" with "[Hl Hlist]") as "_".
        { iNext; iExists _; by iFrame. }
337
        iModIntro.
338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365
        wp_if.
        iApply ("IH" with "HP HΦ").
    - wp_match.
      by iApply "HΦ".
  Qed.

  Theorem pop_works P s :
    {{{ 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".
    wp_lam. wp_proj. wp_let. wp_proj. wp_lam.
    wp_apply get_works; first done.
    iIntros (ov) "[-> | HSome]".
    - wp_match. wp_bind (Load _).
      iInv N as (list) "[Hl Hlist]" "Hclose".
      wp_load.
      iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
      iMod ("Hclose" with "[Hl Hlist]") as "_".
      { iNext; iExists _; by iFrame. }
      iModIntro.
      iDestruct "Hdisj" as "[-> | Heq]".
      * wp_match.
        iApply "HΦ"; by iLeft.
      * iDestruct "Heq" as (l' h t) "[-> Hl']".
        wp_match. wp_bind (Load _).
        iInv N as (v') "[>Hl Hlist]" "Hclose".
        iDestruct "Hl'" as (q) "Hl'".
366
        wp_load.
367 368
        iMod ("Hclose" with "[Hl Hlist]") as "_".
        { iNext; iExists _; by iFrame. }
369
        iModIntro.
370 371 372 373 374 375 376 377 378 379 380
        wp_let. wp_proj. wp_bind (CAS _ _ _).
        iInv N as (v'') "[Hl Hlist]" "Hclose".
        destruct (decide (v'' = InjRV #l')) as [-> |].
        + rewrite is_list_unfold.
          iDestruct "Hlist" as "[>% | H]"; first done.
          iDestruct "H" as (l'' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
          iDestruct "Hl''" as (q') "Hl''".
          wp_cas_suc.
          iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
          iMod ("Hclose" with "[Hl Hlist]") as "_".
          { iNext; iExists _; by iFrame. }
381
          iModIntro.
382 383
          wp_if. wp_proj.
          iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
384
        + wp_cas_fail.
385 386
          iMod ("Hclose" with "[Hl Hlist]") as "_".
          { iNext; iExists _; by iFrame. }
387 388
          iModIntro.
          wp_if.
389 390 391 392
          iApply ("IH" with "HΦ").
    - iDestruct "HSome" as (v) "[-> HP]".
      wp_match.
      iApply "HΦ"; iRight; iExists _; auto.
393 394
  Qed.
End stack_works.