Commit 1b6cfe1a by Amin Timany Committed by Ralf Jung

### Add the lazy_coin example

parent 5bdb226b
 ... ... @@ -110,7 +110,8 @@ theories/heap_lang/lib/assert.v theories/heap_lang/lib/lock.v theories/heap_lang/lib/spin_lock.v theories/heap_lang/lib/ticket_lock.v theories/heap_lang/lib/coin_flip.v theories/heap_lang/lib/nondet_bool.v theories/heap_lang/lib/lazy_coin.v theories/heap_lang/lib/counter.v theories/heap_lang/lib/atomic_heap.v theories/heap_lang/lib/increment.v ... ...
 From iris.base_logic.lib Require Export invariants. From iris.program_logic Require Export atomic. From iris.proofmode Require Import tactics. From iris.heap_lang Require Import proofmode notation. 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 := λ: "_", let: "y" := ref #false in Fork ("y" <- #true) ;; !"y". Definition earlyChoice: val := λ: "x", let: "r" := rand #() in "x" <- #0 ;; "r". Definition lateChoice: val := λ: "x", let: "p" := NewProph in "x" <- #0 ;; let: "r" := rand #() in resolve_proph: "p" to: "r" ;; "r". Section coinflip. Context `{!heapG Σ}. Local Definition N := nroot .@ "coin". Lemma rand_spec : {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}. Proof. iIntros (Φ) "_ HP". wp_lam. wp_alloc l as "Hl". iMod (inv_alloc N _ (∃ (b: bool), l ↦ #b)%I with "[Hl]") as "#Hinv"; first by eauto. wp_apply wp_fork. - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto. - wp_pures. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto. iApply "HP". done. Qed. Lemma earlyChoice_spec (x: loc) : <<< x ↦ - >>> earlyChoice #x @ ⊤ <<< ∃ (b: bool), x ↦ #0, RET #b >>>. Proof. iIntros (Φ) "AU". wp_lam. wp_apply rand_spec; first done. iIntros (b) "_". wp_let. 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. Definition extract_bool (l : list (val * val)) : bool := match l with | (_, LitV (LitBool b)) :: _ => b | _ => true end. Lemma lateChoice_spec (x: loc) : <<< x ↦ - >>> lateChoice #x @ ⊤ <<< ∃ (b: bool), x ↦ #0, RET #b >>>. Proof. iIntros (Φ) "AU". wp_lam. wp_apply wp_new_proph; first done. iIntros (v p) "Hp". wp_let. wp_bind (_ <- _)%E. iMod "AU" as "[Hl [_ Hclose]]". iDestruct "Hl" as (v') "Hl". wp_store. iMod ("Hclose" \$! (extract_bool v) with "[Hl]") as "HΦ"; first by eauto. iModIntro. wp_apply rand_spec; try done. iIntros (b') "_". wp_apply (wp_resolve_proph with "Hp"). iIntros (vs) "[HEq _]". iDestruct "HEq" as "->". wp_seq. done. Qed. End coinflip.
 From iris.base_logic Require Export invariants. From iris.program_logic Require Export weakestpre. From iris.heap_lang Require Export lang proofmode notation. From iris.heap_lang.lib Require Export nondet_bool. Definition new_coin: val := λ: <>, (ref NONE, NewProph). Definition read_coin : val := λ: "cp", let: "c" := Fst "cp" in let: "p" := Snd "cp" in match: !"c" with NONE => let: "r" := nondet_bool #() in "c" <- SOME "r";; resolve_proph: "p" to: "r";; "r" | SOME "b" => "b" end. Section proof. Context `{!heapG Σ}. Definition val_to_bool (v : val) : bool := bool_decide (v = #true). Definition prophecy_to_bool (vs : list (val * val)) : bool := default false (val_to_bool ∘ snd <\$> head vs). Lemma prophecy_to_bool_of_bool (b : bool) v vs : prophecy_to_bool ((v, #b) :: vs) = b. Proof. by destruct b. Qed. Definition coin (cp : val) (b : bool) : iProp Σ := (∃ (c : loc) (p : proph_id) (vs : list (val * val)), ⌜cp = (#c, #p)%V⌝ ∗ proph p vs ∗ (c ↦ SOMEV #b ∨ (c ↦ NONEV ∗ ⌜b = prophecy_to_bool vs⌝)))%I. Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c b, RET c; coin c b }}}. Proof. iIntros (Φ) "_ HΦ". wp_lam. wp_apply wp_new_proph; first done. iIntros (vs p) "Hp". wp_alloc c as "Hc". wp_pair. iApply ("HΦ" \$! (#c, #p)%V ). rewrite /coin; eauto 10 with iFrame. Qed. Lemma read_coin_spec cp b : {{{ coin cp b }}} read_coin cp {{{ RET #b; coin cp b }}}. Proof. iIntros (Φ) "Hc HΦ". iDestruct "Hc" as (c p vs ->) "[Hp [Hc | [Hc ->]]]". - wp_lam. wp_load. wp_match. iApply "HΦ". rewrite /coin; eauto 10 with iFrame. - wp_lam. wp_load. wp_match. wp_apply nondet_bool_spec; first done. iIntros (r) "_". wp_let. wp_store. wp_apply (wp_resolve_proph with "[Hp]"); first done. iIntros (ws) "[-> Hws]". rewrite !prophecy_to_bool_of_bool. wp_seq. iApply "HΦ". rewrite /coin; eauto with iFrame. Qed. End proof.
 From iris.base_logic Require Export invariants. From iris.program_logic Require Export weakestpre. From iris.heap_lang Require Export lang proofmode notation. Definition nondet_bool : val := λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l". Section proof. Context `{!heapG Σ}. Lemma nondet_bool_spec : {{{ True }}} nondet_bool #() {{{ (b : bool), RET #b; True }}}. Proof. iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l as "Hl". wp_let. pose proof (nroot .@ "rnd") as rndN. iMod (inv_alloc rndN _ (∃ (b : bool), l ↦ #b)%I with "[Hl]") as "#Hinv"; first by eauto. wp_apply wp_fork. - iInv rndN as (?) "?". wp_store; eauto. - wp_seq. iInv rndN as (?) "?". wp_load. iSplitR "HΦ"; first by eauto. by iApply "HΦ". Qed. End proof.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment