coin_flip.v 2.48 KB
Newer Older
1 2 3
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
4
From iris.heap_lang Require Import proofmode notation.
5 6 7 8 9 10 11
Set Default Proof Using "Type".

(** Nondeterminism and Speculation:
    Implementing "Late choice versus early choice" example from
    Logical Relations for Fine-Grained Concurrency by Turon et al. (POPL'13) *)

Definition rand: val :=
Ralf Jung's avatar
Ralf Jung committed
12 13 14 15
  λ: "_",
    let: "y" := ref #false in
    Fork ("y" <- #true) ;;
    !"y".
16

17 18
Definition earlyChoice: val :=
  λ: "x",
Ralf Jung's avatar
Ralf Jung committed
19 20 21
    let: "r" := rand #() in
    "x" <- #0 ;;
    "r".
22

23 24
Definition lateChoice: val :=
  λ: "x",
Ralf Jung's avatar
Ralf Jung committed
25 26 27 28 29
    let: "p" := NewProph in
    "x" <- #0 ;;
    let: "r" := rand #() in
    resolve_proph: "p" to: "r" ;;
    "r".
30

31
Section coinflip.
Ralf Jung's avatar
Ralf Jung committed
32 33 34
  Context `{!heapG Σ}.

  Local Definition N := nroot .@ "coin".
35

36 37
  Lemma rand_spec :
    {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
Ralf Jung's avatar
Ralf Jung committed
38
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
39
    iIntros (Φ) "_ HP". wp_lam. wp_alloc l as "Hl".
40
    iMod (inv_alloc N _ ( (b: bool), l  #b)%I with "[Hl]") as "#Hinv"; first by eauto.
41 42
    wp_apply wp_fork.
    - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
43
    - wp_pures. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
44 45 46 47 48 49 50 51
      iApply "HP". done.
  Qed.

  Lemma earlyChoice_spec (x: loc) :
    <<< x  - >>>
        earlyChoice #x
        @ 
    <<<  (b: bool), x  #0, RET #b >>>.
Ralf Jung's avatar
Ralf Jung committed
52
  Proof.
53
    iIntros (Φ) "AU". wp_lam.
Ralf Jung's avatar
Ralf Jung committed
54 55
    wp_apply rand_spec; first done.
    iIntros (b) "_". wp_let.
56 57 58 59 60 61 62 63
    wp_bind (_ <- _)%E.
    iMod "AU" as "[Hl [_ Hclose]]".
    iDestruct "Hl" as (v) "Hl".
    wp_store.
    iMod ("Hclose" with "[Hl]") as "HΦ"; first by eauto.
    iModIntro. wp_seq. done.
  Qed.

64 65 66 67
  Definition extract_bool (l : list (val * val)) : bool :=
    match l with
    | (_, LitV (LitBool b)) :: _ => b
    | _                          => true
Marianna Rapoport's avatar
Marianna Rapoport committed
68 69
    end.

70
  Lemma lateChoice_spec (x: loc) :
71
    <<< x  - >>>
72
        lateChoice #x
73
        @ 
74
    <<<  (b: bool), x  #0, RET #b >>>.
Ralf Jung's avatar
Ralf Jung committed
75
  Proof.
76
    iIntros (Φ) "AU". wp_lam.
77
    wp_apply wp_new_proph; first done.
Ralf Jung's avatar
Ralf Jung committed
78
    iIntros (v p) "Hp".
79
    wp_let.
80 81 82 83
    wp_bind (_ <- _)%E.
    iMod "AU" as "[Hl [_ Hclose]]".
    iDestruct "Hl" as (v') "Hl".
    wp_store.
84
    iMod ("Hclose" $! (extract_bool v) with "[Hl]") as "HΦ"; first by eauto.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
85 86
    iModIntro. wp_apply rand_spec; try done.
    iIntros (b') "_".
Ralf Jung's avatar
Ralf Jung committed
87
    wp_apply (wp_resolve_proph with "Hp").
88
    iIntros (vs) "[HEq _]". iDestruct "HEq" as "->". wp_seq. done.
89 90
  Qed.

91
End coinflip.