Commit a555a33c authored by Ralf Jung's avatar Ralf Jung

Merge branch 'lazy_coin' into 'master'

Add the lazy_coin example

See merge request !264
parents 5bdb226b 1b6cfe1a
Pipeline #17488 passed with stage
in 14 minutes and 5 seconds
......@@ -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