Commit 4beb6889 authored by Ralf Jung's avatar Ralf Jung

Merge "iris-atomic" history

parents b254321f 016104c0
From iris.program_logic Require Export weakestpre hoare atomic.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import agree frac.
From iris_atomic Require Import sync misc.
(** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
Instance subG_syncΣ {Σ} : subG syncΣ Σ syncG Σ.
Proof. by intros ?%subG_inG. Qed.
Section atomic_sync.
Context `{EqDecision A, !heapG Σ, !lockG Σ}.
Canonical AC := leibnizC A.
Context `{!inG Σ (prodR fracR (agreeR AC))}.
(* TODO: Rename and make opaque; the fact that this is a half should not be visible
to the user. *)
Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, to_agree g).
Definition atomic_seq_spec (ϕ: A iProp Σ) α β (f x: val) :=
( g, {{ ϕ g α g }} f x {{ v, g', ϕ g' β g g' v }})%I.
(* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
Definition atomic_synced (ϕ: A iProp Σ) γ (f f': val) :=
( α β (x: val), atomic_seq_spec ϕ α β f x
<<< g, gHalf γ g α g >>> f' x @ <<< v, g', gHalf γ g' β g g' v, RET v >>>)%I.
(* TODO: Use our usual style with a generic post-condition. *)
(* TODO: We could get rid of the x, and hard-code a unit. That would
be no loss in expressiveness, but probably more annoying to apply.
How much more annoying? And how much to we gain in terms of things
becomign easier to prove? *)
(* This is really the core of the spec: It says that executing `s` on `f`
turns the sequential spec with f, α, β into the concurrent triple with f', α, β. *)
Definition is_atomic_syncer (ϕ: A iProp Σ) γ (s: val) :=
( (f: val), WP s f {{ f', atomic_synced ϕ γ f f' }})%I.
Definition atomic_syncer_spec (mk_syncer: val) :=
(g0: A) (ϕ: A iProp Σ),
{{{ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 is_atomic_syncer ϕ γ s }}}.
Lemma atomic_spec (mk_syncer: val):
mk_syncer_spec mk_syncer atomic_syncer_spec mk_syncer.
Proof.
iIntros (Hsync g0 ϕ ret) "Hϕ Hret".
iMod (own_alloc (((1 / 2)%Qp, to_agree g0) ((1 / 2)%Qp, to_agree g0))) as (γ) "[Hg1 Hg2]".
{ by rewrite pair_op agree_idemp. }
iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[Hg1 Hϕ]")=>//.
{ iExists g0. by iFrame. }
iNext. iIntros (s) "#Hsyncer". iApply "Hret".
iSplitL "Hg2"; first done. iIntros "!#".
iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
iIntros (f') "#Hsynced {Hsyncer}".
iAlways. iIntros (α β x) "#Hseq". change (ofe_car AC) with A.
iApply wp_atomic_intro. iIntros (Φ') "?".
(* TODO: Why can't I iApply "Hsynced"? *)
iSpecialize ("Hsynced" $! _ Φ' x).
iApply wp_wand_r. iSplitL.
- iApply ("Hsynced" with "[]")=>//; last iAccu.
iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
(* we should view shift at this point *)
iApply fupd_wp. iMod "HP" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
iDestruct (m_frag_agree with "Hg1 Hg2") as %Heq. subst.
iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "Hϕ".
{ iApply "Hseq". iFrame. done. }
iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
iMod ("HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
iSpecialize ("Hvs2" $! v).
iDestruct (m_frag_agree' with "Hg'' Hg1") as "[Hg %]". subst.
rewrite Qp_div_2.
iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ((1 / 2)%Qp, to_agree g')))%I
with "[Hg]" as ">[Hg1 Hg2]".
{ iApply own_update; last by iAssumption.
apply cmra_update_exclusive. by rewrite pair_op agree_idemp. }
iMod ("Hvs2" with "[Hg1 Hβ]").
{ iExists g'. iFrame. }
iModIntro. iSplitL "Hg2 Hϕ'"; last done.
iExists g'. by iFrame.
- iIntros (?) "?". done.
Qed.
End atomic_sync.
This diff is collapsed.
(* Miscellaneous lemmas *)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap agree.
From iris.bi Require Import fractional.
From iris.base_logic Require Import auth.
Import uPred.
Section lemmas.
Lemma pair_l_frac_op' (p q: Qp) (g g': val):
((p + q)%Qp, to_agree g') ~~> (((p, to_agree g') (q, to_agree g'))).
Proof. by rewrite pair_op agree_idemp frac_op'. Qed.
Lemma pair_l_frac_op_1' (g g': val):
(1%Qp, to_agree g') ~~> (((1/2)%Qp, to_agree g') ((1/2)%Qp, to_agree g')).
Proof. by rewrite pair_op agree_idemp frac_op' Qp_div_2. Qed.
End lemmas.
Section excl.
Context `{!inG Σ (exclR unitC)}.
Lemma excl_falso γ Q':
own γ (Excl ()) own γ (Excl ()) Q'.
Proof.
iIntros "[Ho1 Ho2]". iCombine "Ho1" "Ho2" as "Ho".
iExFalso. by iDestruct (own_valid with "Ho") as "%".
Qed.
End excl.
Section heap_extra.
Context `{heapG Σ}.
Lemma bogus_heap p (q1 q2: Qp) a b:
~((q1 + q2)%Qp 1%Qp)%Qc
p {q1} a p {q2} b False.
Proof.
iIntros (?) "Hp".
iDestruct "Hp" as "[Hl Hr]".
iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
Qed.
End heap_extra.
Section big_op_later.
Context {M : ucmraT}.
Context `{Countable K} {A : Type}.
Implicit Types m : gmap K A.
Implicit Types Φ Ψ : K A uPred M.
Lemma big_sepM_delete_later Φ m i x :
m !! i = Some x
([ map] ky m, Φ k y) ⊣⊢ Φ i x [ map] ky delete i m, Φ k y.
Proof. intros ?. rewrite big_sepM_delete=>//. apply later_sep. Qed.
Lemma big_sepM_insert_later Φ m i x :
m !! i = None
([ map] ky <[i:=x]> m, Φ k y) ⊣⊢ Φ i x [ map] ky m, Φ k y.
Proof. intros ?. rewrite big_sepM_insert=>//. apply later_sep. Qed.
End big_op_later.
Section pair.
Context {A : ofeT} `{EqDecision A, !OfeDiscrete A, !LeibnizEquiv A, !inG Σ (prodR fracR (agreeR A))}.
Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, to_agree a1) - own γm (q2, to_agree a2) - a1 = a2.
Proof.
iIntros "Ho Ho'".
destruct (decide (a1 = a2)) as [->|Hneq]=>//.
iCombine "Ho" "Ho'" as "Ho".
iDestruct (own_valid with "Ho") as %Hvalid.
exfalso. destruct Hvalid as [_ Hvalid].
simpl in Hvalid. apply agree_op_inv in Hvalid. apply (inj to_agree) in Hvalid.
apply Hneq. by fold_leibniz.
Qed.
Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, to_agree a1) - own γm (q2, to_agree a2)
- own γm ((q1 + q2)%Qp, to_agree a1) a1 = a2.
Proof.
iIntros "Ho Ho'".
iDestruct (m_frag_agree with "Ho Ho'") as %Heq.
subst. iCombine "Ho" "Ho'" as "Ho".
by iFrame.
Qed.
End pair.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap csum.
From iris_atomic Require Export treiber misc.
From iris.base_logic.lib Require Import invariants.
Section defs.
Context `{heapG Σ} (N: namespace).
Context (R: val iProp Σ) `{ x, TimelessP (R x)}.
Fixpoint is_list_R (hd: loc) (xs: list val) : iProp Σ :=
match xs with
| [] => ( q, hd { q } NONEV)%I
| x :: xs => ( (hd': loc) q, hd {q} SOMEV (x, #hd') inv N (R x) is_list_R hd' xs)%I
end.
Definition is_bag_R xs s := ( hd: loc, s #hd is_list_R hd xs)%I.
Lemma dup_is_list_R : xs hd,
is_list_R hd xs |==> is_list_R hd xs is_list_R hd xs.
Proof.
induction xs as [|y xs' IHxs'].
- iIntros (hd) "Hs".
simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
- iIntros (hd) "Hs". simpl.
iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hinv & Hs')".
iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
Qed.
Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
{{{ inv N R Rf }}}
f x
{{{ RET #(); Rf }}}.
End defs.
Section proofs.
Context `{heapG Σ} (N: namespace).
Context (R: val iProp Σ).
Definition bag_inv s: iProp Σ := inv N ( xs, is_bag_R N R xs s)%I.
Lemma new_bag_spec:
{{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd.
wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc s as "Hs".
iAssert (( xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
{ iFrame. iExists [], l.
iFrame. simpl. eauto. }
iMod (inv_alloc N _ ( xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
iApply "HΦ". iFrame "#". done.
Qed.
Lemma push_spec (s: loc) (x: val):
{{{ R x bag_inv s }}} push #s x {{{ RET #() ; inv N (R x) }}}.
Proof.
iIntros (Φ) "(HRx & #?) HΦ".
iLöb as "IH". wp_rec. wp_let.
wp_bind (! _)%E.
iInv N as "H1" "Hclose".
iDestruct "H1" as (xs hd) "[>Hs H1]".
wp_load. iMod ("Hclose" with "[Hs H1]").
{ iNext. iFrame. iExists xs, hd. iFrame. }
iModIntro. wp_let. wp_alloc l as "Hl".
wp_let. wp_bind (CAS _ _ _)%E.
iInv N as "H1" "Hclose".
iDestruct "H1" as (xs' hd') "[>Hs H1]".
destruct (decide (hd = hd')) as [->|Hneq].
- wp_cas_suc.
iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
iMod ("Hclose" with "[Hs Hl H1]").
{ iNext. iFrame. iExists (x::xs'), l.
iFrame. simpl. iExists hd', 1%Qp. iFrame.
by iFrame "#". }
iModIntro. wp_if. by iApply "HΦ".
- wp_cas_fail.
iMod ("Hclose" with "[Hs H1]").
{ iNext. iFrame. iExists (xs'), hd'. iFrame. }
iModIntro. wp_if. iApply ("IH" with "HRx").
by iNext.
Qed.
End proofs.
(* Coarse-grained syncer *)
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import frac.
From iris_atomic Require Import sync.
Import uPred.
Definition mk_sync: val :=
λ: <>,
let: "l" := newlock #() in
λ: "f" "x",
acquire "l";;
let: "ret" := "f" "x" in
release "l";;
"ret".
Section syncer.
Context `{!heapG Σ, !lockG Σ} (N: namespace).
Lemma mk_sync_spec: mk_syncer_spec mk_sync.
Proof.
iIntros (R Φ) "HR HΦ".
wp_lam. wp_bind (newlock _).
iApply (newlock_spec N R with "[HR]"); first done. iNext.
iIntros (lk γ) "#Hl". wp_pures. iApply "HΦ". iIntros "!#".
iIntros (f). wp_pures. iAlways.
iIntros (P Q x) "#Hf !# HP".
wp_pures. wp_bind (acquire _).
iApply (acquire_spec with "Hl"). iNext.
iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
iSpecialize ("Hf" with "[R HP]"); first by iFrame.
iApply wp_wand_r. iSplitL "Hf"; first done.
iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
iApply (release_spec with "[$Hl $HR $Hlocked]").
iNext. iIntros "_". by wp_seq.
Qed.
End syncer.
(* Syncer spec *)
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Section sync.
Context `{!heapG Σ} (N : namespace).
(* TODO: We could get rid of the x, and hard-code a unit. That would
be no loss in expressiveness, but probably more annoying to apply.
How much more annoying? And how much to we gain in terms of things
becoming easier to prove? *)
Definition synced R (f f': val) :=
( P Q (x: val), {{ R P }} f x {{ v, R Q v }}
{{ P }} f' x {{ Q }})%I.
(* Notice that `s f` is *unconditionally safe* to execute, and only
when executing the returned f' we have to provide a spec for f.
This is crucial. *)
(* TODO: Use our usual style with a generic post-condition. *)
Definition is_syncer (R: iProp Σ) (s: val) :=
( (f : val), WP s f {{ f', synced R f f' }})%I.
Definition mk_syncer_spec (mk_syncer: val) :=
(R: iProp Σ),
{{{ R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
End sync.
From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre atomic.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth gmap csum.
Definition new_stack: val := λ: <>, ref (ref NONE).
Definition push: val :=
rec: "push" "s" "x" :=
let: "hd" := !"s" in
let: "s'" := ref SOME ("x", "hd") in
if: CAS "s" "hd" "s'"
then #()
else "push" "s" "x".
Definition pop: val :=
rec: "pop" "s" :=
let: "hd" := !"s" in
match: !"hd" with
SOME "cell" =>
if: CAS "s" "hd" (Snd "cell")
then SOME (Fst "cell")
else "pop" "s"
| NONE => NONE
end.
Definition iter: val :=
rec: "iter" "hd" "f" :=
match: !"hd" with
NONE => #()
| SOME "cell" => "f" (Fst "cell") ;; "iter" (Snd "cell") "f"
end.
Section proof.
Context `{!heapG Σ} (N: namespace).
Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ :=
match xs with
| [] => ( q, hd { q } NONEV)%I
| x :: xs => ( (hd': loc) q, hd { q } SOMEV (x, #hd') is_list hd' xs)%I
end.
Lemma dup_is_list : xs hd,
is_list hd xs is_list hd xs is_list hd xs.
Proof.
induction xs as [|y xs' IHxs'].
- iIntros (hd) "Hs".
simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
- iIntros (hd) "Hs". simpl.
iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hs')".
iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame.
iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
Qed.
Lemma uniq_is_list:
xs ys hd, is_list hd xs is_list hd ys xs = ys.
Proof.
induction xs as [|x xs' IHxs'].
- induction ys as [|y ys' IHys'].
+ auto.
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
iExFalso. iDestruct "Hxs" as (?) "Hhd'".
(* FIXME: If I dont use the @ here and below through this file, it loops. *)
by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
- induction ys as [|y ys' IHys'].
+ iIntros (hd) "(Hxs & Hys)".
simpl.
iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
iDestruct "Hys" as (?) "Hhd'".
by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
by subst.
Qed.
Definition is_stack (s: loc) xs: iProp Σ := ( hd: loc, s #hd is_list hd xs)%I.
Global Instance is_list_timeless xs hd: Timeless (is_list hd xs).
Proof. generalize hd. induction xs; apply _. Qed.
Global Instance is_stack_timeless xs hd: Timeless (is_stack hd xs).
Proof. generalize hd. induction xs; apply _. Qed.
Lemma new_stack_spec:
(Φ: val iProp Σ),
( s, is_stack s [] - Φ #s) WP new_stack #() {{ Φ }}.
Proof.
iIntros (Φ) "HΦ". wp_lam.
wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc l' as "Hl'".
iApply "HΦ". rewrite /is_stack. iExists l.
iFrame. by iExists 1%Qp.
Qed.
Definition push_triple (s: loc) (x: val) :=
<<< (xs : list val) (hd : loc), s #hd is_list hd xs >>>
push #s x @
<<< hd' : loc, s #hd' hd' SOMEV (x, #hd) is_list hd xs, RET #() >>>.
Lemma push_atomic_spec (s: loc) (x: val) :
push_triple s x.
Proof.
rewrite /push_triple. iApply wp_atomic_intro.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
wp_let. wp_bind (! _)%E.
iMod "HP" as (xs hd) "[[Hs Hhd] [Hvs' _]]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
wp_bind (CAS _ _ _)%E.
iMod "HP" as (xs' hd') "[[Hs Hhd'] Hvs']".
destruct (decide (hd = hd')) as [->|Hneq].
* wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" with "[-]") as "HQ".
{ by iFrame. }
iModIntro. wp_if. eauto.
* wp_cas_fail.
iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH".
Qed.
Definition pop_triple (s: loc) :=
<<< (xs : list val) (hd : loc), s #hd is_list hd xs >>>
pop #s @
<<< match xs with [] => s #hd is_list hd []
| x::xs' => q (hd': loc), hd {q} SOMEV (x, #hd') s #hd' is_list hd' xs' end,
RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
Lemma pop_atomic_spec (s: loc):
pop_triple s.
Proof.
rewrite /pop_triple. iApply wp_atomic_intro.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
wp_bind (! _)%E.
iMod "HP" as (xs hd) "[[Hs Hhd] Hvs']".
destruct xs as [|y' xs'].
- simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
iDestruct "Hhd" as (q) "[Hhd Hhd']".
iMod ("Hvs'" with "[-Hhd]") as "HQ".
{ iFrame. eauto. }
iModIntro. wp_let. wp_load. wp_pures.
eauto.
- simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
wp_load. iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
{ iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj.
wp_bind (CAS _ _ _).
iMod "HP" as (xs hd'') "[[Hs Hhd''] Hvs']".
destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
destruct xs as [|x' xs''].
{ simpl. iDestruct "Hhd''" as (?) "H".
iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?. }
simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=]. subst.
iMod ("Hvs'" with "[-]") as "HQ".
{ iExists (q / 2 / 2)%Qp, _.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
iFrame. }
iModIntro. wp_if. wp_pures. eauto.
+ wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH".
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