Commit 5c51c26c authored by Marianna Rapoport's avatar Marianna Rapoport Committed by Ralf Jung

First motivating example for prophecy variables (coin-flip)

- Added my version of increment.v for practicing working with logically atomic triples
- Added implementation of coin-flip spec from Turon et al. (POPL'13) with an assumed spec for prophecy variables
parent 598a6902
......@@ -23,9 +23,10 @@ Open Scope Z_scope.
(** Expressions and vals. *)
Definition loc := positive. (* Really, any countable type. *)
Definition proph := positive.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitProphecy (p: proph).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
......@@ -192,11 +193,13 @@ Defined.
Instance base_lit_countable : Countable base_lit.
Proof.
refine (inj_countable' (λ l, match l with
| LitInt n => inl (inl n) | LitBool b => inl (inr b)
| LitUnit => inr (inl ()) | LitLoc l => inr (inr l)
| LitInt n => (inl (inl n), None) | LitBool b => (inl (inr b), None)
| LitUnit => (inr (inl ()), None) | LitLoc l => (inr (inr l), None)
| LitProphecy p => (inr (inl ()), Some p)
end) (λ l, match l with
| inl (inl n) => LitInt n | inl (inr b) => LitBool b
| inr (inl ()) => LitUnit | inr (inr l) => LitLoc l
| (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
| (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
| (_, Some p) => LitProphecy p
end) _); by intros [].
Qed.
Instance un_op_finite : Countable un_op.
......
From iris.heap_lang Require Export lifting notation.
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 par.
From iris.bi.lib Require Import fractional.
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".
Section coinflip.
Definition lateChoice: val :=
λ: "x",
"x" <- #0 ;;
rand #().
Context `{!heapG Σ} (N: namespace).
Lemma rand_spec :
{{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
Proof using N.
iIntros (Φ) "_ HP".
wp_lam. wp_alloc l as "Hl". wp_lam.
iMod (inv_alloc N _ ( (b: bool), l #b)%I with "[Hl]") as "#Hinv"; first by eauto.
wp_apply wp_fork. iSplitL.
- wp_lam. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
iApply "HP". done.
- iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
Qed.
Lemma earlyChoice_spec (x: loc) :
<<< x - >>>
earlyChoice #x
@
<<< (b: bool), x #0, RET #b >>>.
Proof using N.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_bind (rand _)%E. iApply 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.
(* lateChoice can currently not be proved in Iris *)
Lemma lateChoice_spec (x: loc) :
<<< x - >>>
lateChoice #x
@
<<< (b: bool), x #0, RET #b >>>.
Proof using N.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_bind (_ <- _)%E.
iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v) "Hl".
wp_store.
(* now we have to "predict" the value of b, which is the result of calling rand.
but we can't know at this point what that value is. *)
iMod ("Hclose" $! true with "[Hl]") as "AU"; first by eauto.
iModIntro. wp_seq.
iApply rand_spec; first done.
iIntros (b) "!> _".
Abort.
End coinflip.
Section prophecy.
Context `{!heapG Σ} (N: namespace).
Record prophecy {Σ} `{!heapG Σ} := Prophecy {
(* -- operations -- *)
new_prophecy : val;
resolve_prophecy : val;
(* -- predicates -- *)
is_prophecy : proph -> val -> iProp Σ;
(* -- general properties -- *)
new_prophecy_spec :
{{{ True }}} new_prophecy #() {{{ p, RET #p; v, is_prophecy p #v }}};
resolve_prophecy_spec p v w :
{{{ is_prophecy p v }}} resolve_prophecy #p w {{{ RET w; v = w }}}
}.
Context `{pr: prophecy}.
Definition lateChoice_proph: val :=
λ: "x",
let: "p" := new_prophecy pr #() in
"x" <- #0 ;;
let: "r" := rand #() in
resolve_prophecy pr "p" "r".
Definition val_to_bool v :=
match v with
| LitBool b => Some b
| _ => None
end.
Lemma lateChoice_proph_spec (x: loc) :
<<< x - >>>
lateChoice_proph #x
@
<<< (b: bool), x #0, RET #b >>>.
Proof using N.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_apply new_prophecy_spec; first done.
iIntros (p) "Hp". iDestruct "Hp" as (v) "Hp".
wp_let.
wp_bind (_ <- _)%E.
iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v') "Hl".
wp_store.
destruct (val_to_bool v) eqn:Heq.
- iMod ("Hclose" $! b with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_seq. wp_apply rand_spec; try done.
iIntros (b') "_". wp_let.
iDestruct (resolve_prophecy_spec with "Hp") as "Hs".
iAssert ((#v = #b' - Φ #b'))%I with "[HΦ]" as "Hb". {
iNext. iIntros "Heq". destruct v; inversion Heq; subst. iDestruct "Heq" as %->. done.
}
iSpecialize ("Hs" with "Hb"). done.
- iMod ("Hclose" $! true with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_seq. wp_apply rand_spec; try done.
iIntros (b') "_". wp_let.
iDestruct (resolve_prophecy_spec with "Hp") as "Hs".
iAssert ((#v = #b' - Φ #b'))%I with "[HΦ]" as "Hb". {
iNext. iIntros "Heq". iDestruct "Heq" as %[=Heq'].
destruct v; inversion Heq; inversion Heq'.
}
iSpecialize ("Hs" with "Hb"). done.
Qed.
End prophecy.
......@@ -8,6 +8,7 @@ Delimit Scope val_scope with V.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
Coercion LitProphecy : proph >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.
......
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