Commit 0bcdf840 authored by Ralf Jung's avatar Ralf Jung

port to new atomic triples

parent d8ea1ae9
-Q theories iris_atomic
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/atomic.v
theories/sync.v
theories/atomic_incr.v
theories/simple_sync.v
theories/flat.v
theories/atomic_sync.v
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
depends: [
"coq-iris" { (= "dev.2018-07-13.0.cbf73155") | (= "dev") }
"coq-iris" { (= "dev.2018-07-13.2.af5611c8") | (= "dev") }
]
(* Logically atomic triple *)
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
Import uPred.
Section atomic.
Context `{irisG Λ Σ} {A: Type}.
(* NOTE: This triple differs from the one described in the Iris 1.0 paper by
not having any laters. That works for this case study, but would not work for
the case study described in the paper. *)
(* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
(* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_triple
(α: A iProp Σ) (* atomic pre-condition *)
(β: A val _ iProp Σ) (* atomic post-condition *)
(Ei Eo: coPset) (* inside/outside masks *)
(e: expr _) : iProp Σ :=
( P Q, (P ={Eo, Ei}=> x:A,
α x
((α x ={Ei, Eo}= P)
( v, β x v ={Ei, Eo}= Q v))
) - {{ P }} e @ {{ Q }})%I.
End atomic.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris_atomic Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import par.
Section incr.
Context `{!heapG Σ} (N : namespace).
Definition incr: val :=
rec: "incr" "l" :=
let: "oldv" := !"l" in
if: CAS "l" "oldv" ("oldv" + #1)
then "oldv" (* return old value if success *)
else "incr" "l".
(* TODO: Can we have a more WP-style definition and avoid the equality? *)
Definition incr_triple (l: loc) :=
atomic_triple (fun (v: Z) => l #v)%I
(fun v ret => ret = #v l #(v + 1))%I
(incr #l).
Lemma incr_atomic_spec: (l: loc), incr_triple l.
Proof.
iIntros (l).
rewrite /incr_triple.
rewrite /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH".
iIntros "!# HP".
wp_rec.
wp_bind (! _)%E.
iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
wp_load.
iMod ("Hvs'" with "Hl") as "HP".
iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
destruct (decide (x = x')).
- subst.
iDestruct "Hvs'" as "[_ Hvs']".
iSpecialize ("Hvs'" $! #x').
wp_cas_suc.
iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
iModIntro. wp_if. done.
- iDestruct "Hvs'" as "[Hvs' _]".
wp_cas_fail.
iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH".
Qed.
End incr.
Section user.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition incr_2 : val :=
λ: "x",
let: "l" := ref "x" in
incr "l" ||| incr "l";;
!"l".
(* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
Lemma incr_2_safe:
(x: Z), (WP incr_2 #x {{ _, True }})%I.
Proof.
iIntros (x).
rewrite /incr_2 /=.
wp_lam.
wp_alloc l as "Hl".
iMod (inv_alloc N _ (x':Z, l #x')%I with "[Hl]") as "#?"; first eauto.
wp_let.
wp_bind (_ ||| _)%E.
iAssert ( WP incr #l {{ _, True }})%I as "#?".
{ (* prove worker triple *)
iDestruct (incr_atomic_spec l) as "Hincr"=>//.
rewrite /incr_triple /atomic_triple.
iSpecialize ("Hincr" $! True%I (fun _ => True%I) with "[]").
- iIntros "!# _".
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
iMod (fupd_intro_mask' _ ) as "Hvs"; first set_solver.
iModIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
- iDestruct "Hincr" as "#HIncr". iAlways. by iApply "HIncr". }
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[] []"); [done..|].
iIntros (v1 v2) "_ !>".
wp_seq. iInv N as (x') ">Hl" "Hclose".
wp_load. iApply "Hclose". eauto.
Qed.
End user.
From iris.program_logic Require Export weakestpre hoare.
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 atomic sync misc.
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.
......@@ -27,9 +29,7 @@ Section atomic_sync.
(* 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
atomic_triple (fun g => gHalf γ g α g)%I
(fun g v => g', gHalf γ g' β g g' v)%I
(f' x))%I.
<<< 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
......@@ -57,22 +57,21 @@ Section atomic_sync.
iSplitL "Hg2"; first done. iIntros "!#".
iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
iIntros (f') "#Hsynced {Hsyncer}".
iAlways. iIntros (α β x) "#Hseq".
iIntros (P Q) "#Hvss !# HP".
iAlways. iIntros (α β x) "#Hseq". change (ofe_car AC) with A.
iApply wp_atomic_intro. iIntros (Φ') "?".
(* TODO: Why can't I iApply "Hsynced"? *)
iSpecialize ("Hsynced" $! P Q x).
iApply wp_wand_r. iSplitL "HP".
- iApply ("Hsynced" with "[]")=>//.
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 *)
iDestruct ("Hvss" with "HP") as "Hvss'". iApply fupd_wp.
iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
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 ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
iMod ("HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
iSpecialize ("Hvs2" $! v).
iDestruct (m_frag_agree' with "Hg'' Hg1") as "[Hg %]". subst.
rewrite Qp_div_2.
......
......@@ -10,7 +10,7 @@ Section sync.
(* 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? *)
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.
......
From iris.program_logic Require Export weakestpre.
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.
From iris_atomic Require Import atomic misc.
From iris_atomic Require Import misc.
Definition new_stack: val := λ: <>, ref (ref NONE).
......@@ -98,32 +99,25 @@ Section proof.
Qed.
Definition push_triple (s: loc) (x: val) :=
atomic_triple (fun xs_hd: list val * loc =>
let '(xs, hd) := xs_hd in s #hd is_list hd xs)%I
(fun xs_hd ret =>
let '(xs, hd) := xs_hd in
hd': loc,
ret = #() s #hd' hd' SOMEV (x, #hd) is_list hd xs)%I
(push #s x).
<<< (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 /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec.
rewrite /push_triple. iApply wp_atomic_intro.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
wp_let. wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
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 ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
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".
{ iExists l. iSplitR; first done. by iFrame. }
iMod ("Hvs'" with "[-]") as "HQ".
{ by iFrame. }
iModIntro. wp_if. eauto.
* wp_cas_fail.
iDestruct "Hvs'" as "[Hvs' _]".
......@@ -132,30 +126,24 @@ Section proof.
Qed.
Definition pop_triple (s: loc) :=
atomic_triple (fun xs_hd: list val * loc =>
let '(xs, hd) := xs_hd in s #hd is_list hd xs)%I
(fun xs_hd ret =>
let '(xs, hd) := xs_hd in
(ret = NONEV xs = [] s #hd is_list hd [])
( x q (hd': loc) xs', hd {q} SOMEV (x, #hd') ret = SOMEV x
xs = x :: xs'⌝ s #hd' is_list hd' xs'))%I
(pop #s).
<<< (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 /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec.
rewrite /pop_triple. iApply wp_atomic_intro.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
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'" $! NONEV with "[-Hhd]") as "HQ".
{ iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
iMod ("Hvs'" with "[-Hhd]") as "HQ".
{ iFrame. eauto. }
iModIntro. wp_let. wp_load. wp_match.
eauto.
- simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
......@@ -165,20 +153,19 @@ Section proof.
{ iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj.
wp_bind (CAS _ _ _).
iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
iMod "HP" as (xs hd'') "[[Hs Hhd''] Hvs']".
destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
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.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
iFrame. }
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_proj. eauto.
+ wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
......
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