...
 
Commits (10)
......@@ -2,21 +2,229 @@
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
From iris.proofmode Require Import tactics.
From stdpp Require Import hlist.
Import uPred.
Definition mono {M X} (F : (X uPred M) (X uPred M)) := P Q, ( (x : X), P x Q x) ( (x : X), F P x F Q x).
Definition Fix {M X} (F : (X uPred M) (X uPred M)) : X uPred M :=
(λ x, P (_ : x, P x F P x), P x)%I.
Lemma Fix_implies_F_Fix {M X} F :
@mono M X F
x, Fix F x F (Fix F) x.
Proof.
iIntros (Hmono x) "HFix".
iDestruct "HFix" as (P Hincl) "HP".
pose proof (Hmono P (Fix F)).
rewrite -(impl_elim_r (F P x) (F (Fix F) x)).
iSplit. by iApply Hincl.
rewrite -H. iIntros "{HP}". auto.
iIntros (x') "HP".
iExists P, Hincl. eauto.
Qed.
Lemma F_Fix_implies_Fix {M X} F :
@mono M X F
x, F (Fix F) x Fix F x.
Proof.
iIntros (H x) "HF".
iExists (F (Fix F)).
rewrite -exist_intro; first done.
apply H.
intros x'.
by rewrite Fix_implies_F_Fix.
Qed.
Corollary Fix_unfold {M X} F :
@mono M X F
x, Fix F x F (Fix F) x.
Proof.
iIntros.
iSplit.
- rewrite -Fix_implies_F_Fix //; auto.
- rewrite F_Fix_implies_Fix //; auto.
Qed.
Lemma Fix_coind {M X} (F : (X uPred M) (X uPred M)) :
(P : X uPred M), ( x, P x F P x)
( x, P x Fix F x).
Proof.
iIntros.
by iExists P, H.
Qed.
Fixpoint incl {M Tl} : relation (himpl Tl (uPred M)) :=
match Tl with
| tnil => λ P Q, P - Q
| tcons T' Tl => λ P Q, (x: T'), incl (P x) (Q x)
end.
Definition mono' {M Tl} F := P Q, @incl M Tl P Q @incl M Tl (F P) (F Q).
Definition Fix' {M Tl} (F : himpl Tl (uPred M) himpl Tl (uPred M)) :=
huncurry (Fix (λ P, hcurry (F (huncurry P)))).
Lemma incl_curry_impl {M Tl} P Q :
@incl M Tl P Q ( x, hcurry P x hcurry Q x).
Proof.
split.
- intros. induction x; simpl in *.
+ rewrite /incl in H. apply H.
+ by apply IHx.
- induction Tl; simpl in *; intros.
+ apply (H hnil).
+ apply IHTl. intros x'. apply (H (hcons _ _)).
Qed.
Lemma incl_uncurry_impl {M Tl} P Q :
@incl M Tl (huncurry P) (huncurry Q) ( x, P x Q x).
Proof.
split.
- intros. induction x; simpl in *.
+ rewrite /incl in H. apply H.
+ apply (IHx (λ l, P (hcons a l)) (λ l, Q (hcons a l))).
apply (H a).
- induction Tl; simpl in *; intros.
+ apply (H hnil).
+ apply IHTl. intros x'. apply (H (hcons _ _)).
Qed.
Lemma mono'_curry_mono {M Tl} F :
@mono' M Tl F mono (λ P, hcurry (F (huncurry P))).
Proof.
rewrite /mono /mono' /=.
intros.
setoid_rewrite incl_curry_impl in H.
apply H.
intros.
by rewrite ->! hcurry_uncurry.
Qed.
Lemma Fix'_implies_F_Fix' {M Tl} F :
@mono' M Tl F
incl (Fix' F) (F (Fix' F)).
Proof.
intros.
apply mono'_curry_mono in H.
rewrite incl_curry_impl.
intros.
eapply Fix_implies_F_Fix in H.
setoid_rewrite <- hcurry_uncurry at 1 in H.
apply H.
Qed.
Lemma F_Fix'_implies_Fix' {M Tl} F :
@mono' M Tl F
incl (F (Fix' F)) (Fix' F).
Proof.
intros.
apply mono'_curry_mono in H.
rewrite incl_curry_impl.
intros.
eapply F_Fix_implies_Fix in H.
setoid_rewrite <- hcurry_uncurry at 2 in H.
apply H.
Qed.
Fixpoint hequiv {M Tl} {struct Tl} : Equiv (himpl Tl (uPred M)) :=
match Tl with
| tnil => λ P Q, @equiv (uPred M) _ P Q
| tcons T' Tl => λ P Q, (x: T'), P x Q x
end.
Existing Instance hequiv.
Lemma double_hincl_hequiv {M Tl} P Q:
@incl M Tl P Q incl Q P P Q.
Proof.
intros.
induction Tl.
- apply equiv_spec.
auto.
- intros x.
by apply IHTl.
Qed.
Corollary Fix'_unfold {M Tl} F :
@mono' M Tl F
Fix' F F (Fix' F).
Proof.
intros.
apply double_hincl_hequiv.
{ by apply Fix'_implies_F_Fix'. }
by apply F_Fix'_implies_Fix'.
Qed.
Lemma Fix'_coind {M Tl} (F : himpl Tl (uPred M) himpl Tl (uPred M)) :
mono' F
(P : himpl Tl (uPred M)), incl P (F P)
incl P (Fix' F).
Proof.
intros.
rewrite incl_curry_impl.
intros.
rewrite /Fix'.
rewrite -> hcurry_uncurry.
apply Fix_coind.
intros x'.
eapply incl_curry_impl in H0.
rewrite -> H0.
apply incl_curry_impl.
simpl in *.
apply H.
apply incl_curry_impl.
intros.
by setoid_rewrite hcurry_uncurry.
Qed.
Section atomic.
Context `{irisG Λ Σ} {A: Type}.
Context `{irisG Λ Σ} {A: Type}
(α: A iProp Σ) (* atomic pre-condition *)
(β: A val Λ iProp Σ) (* atomic post-condition *)
(Ei Eo: coPset) (* inside/outside masks *)
.
Definition atomic_shift'_pre (Φ : val Λ iProp Σ) (F : iProp Σ) : iProp Σ :=
(|={Eo,Ei}=> x : A,
α x ((α x ={Ei,Eo}= F) y, β x y ={Ei,Eo}= Φ y))%I.
Lemma atomic_shift'_pre_mono' (Φ : val Λ iProp Σ) :
mono' (Tl := tnil) (atomic_shift'_pre Φ).
Proof.
unfold mono'.
simpl.
intros.
rewrite /atomic_shift'_pre.
by setoid_rewrite <- H.
Qed.
Definition atomic_shift (Φ : val Λ iProp Σ) :=
Fix' (Tl := tnil) (atomic_shift'_pre Φ).
Lemma atomic_shift_unfold (Φ : val Λ iProp Σ) :
atomic_shift Φ
(|={Eo,Ei}=> x : A,
α x ((α x ={Ei,Eo}= atomic_shift Φ) y, β x y ={Ei,Eo}= Φ y))%I.
Proof.
rewrite {1}/atomic_shift.
by rewrite (Fix'_unfold _ (atomic_shift'_pre_mono' Φ)).
Qed.
Lemma atomic_shift_unfold_coind (Φ : val Λ iProp Σ) (P : himpl tnil (uPred (iResUR Σ))) :
incl P (atomic_shift'_pre Φ P) incl P (atomic_shift Φ).
Proof.
intros H.
rewrite /atomic_shift.
by apply (Fix'_coind (Tl := tnil) _ (atomic_shift'_pre_mono' Φ)).
Qed.
(* 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 *)
(* logically atomic wp: <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_wp
(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.
( Φ, atomic_shift Φ - WP e @ Eo {{ Φ }})%I.
End atomic.
Arguments atomic_shift_unfold_coind {_ _ _ _ _ _ _ _ _} _ _.
......@@ -3,6 +3,7 @@ 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.
From stdpp Require Import hlist.
Section incr.
Context `{!heapG Σ} (N : namespace).
......@@ -16,27 +17,28 @@ Section incr.
(* 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).
atomic_wp (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".
rewrite /atomic_wp.
iLöb as "IH".
iIntros "!# HP".
iIntros (Φ) "Hvs".
wp_rec.
wp_bind (! _)%E.
iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
rewrite atomic_shift_unfold.
iMod ("Hvs") as (x) "[Hl [Hvs' _]]".
wp_load.
iMod ("Hvs'" with "Hl") as "HP".
iMod ("Hvs'" with "Hl") as "Hvs".
iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
rewrite atomic_shift_unfold.
iMod ("Hvs") as (x') "[Hl Hvs']".
destruct (decide (x = x')).
- subst.
iDestruct "Hvs'" as "[_ Hvs']".
......@@ -75,9 +77,15 @@ Section user.
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 "!# _".
rewrite /incr_triple /atomic_wp.
iRevert "Hincr". rewrite uPred.always_forall. iIntros "#Hincr".
iSpecialize ("Hincr" $! (fun _ => True%I)).
rewrite uPred.always_wand.
iSpecialize ("Hincr" with "[#]").
- iAlways.
rewrite -(atomic_shift_unfold_coind (inv N ( x' : Z, l #x')))%I /=; first done.
iIntros "#?".
iFrame "#".
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
......@@ -89,7 +97,7 @@ Section user.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
- iDestruct "Hincr" as "#HIncr". iAlways. by iApply "HIncr". }
- 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".
......
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import agree frac.
From iris_atomic Require Import sync atomic_sync.
From iris_atomic Require Import sync atomic_sync atomic.
Import uPred.
Section atomic_pair.
......@@ -10,72 +10,88 @@ Section atomic_pair.
!inG Σ (prodR fracR (agreeR (prodC valC valC)))} (N : namespace).
Definition pcas_seq : val :=
λ: "ls" "ab",
if: !(Fst "ls") = Fst "ab"
then if: !(Snd "ls") = Fst "ab"
then Fst "ls" <- Snd "ab";; Snd "ls" <- Snd "ab";; #true
λ: "lsab",
if: (!(Fst (Fst "lsab"))) = Fst (Snd "lsab")
then if: (!(Snd (Fst "lsab"))) = Fst (Snd "lsab")
then Fst (Fst "lsab") <- Snd (Snd "lsab");; Snd (Fst "lsab") <- Snd (Snd "lsab");; #true
else #false
else #false.
Local Opaque pcas_seq.
else #false.
Definition α (x: val) (_: val) : iProp Σ := ( a b: val, x = (a, b)%V)%I.
Definition ϕ (ls: val) (xs: val) : iProp Σ :=
( (l1 l2: loc) (x1 x2: val),
ls = (#l1, #l2)%V xs = (x1, x2)%V l1 x1 l2 x2)%I.
ls = (#l1, #l2)%V xs = (x1, x2)%V l1 x1 l2 x2)%I.
Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ :=
Definition β (ab: val) (xs: val) (xs': val) (v: val) : iProp Σ :=
⌜∃ a b x1 x2 x1' x2': val,
ab = (a, b)%V xs = (x1, x2)%V xs' = (x1', x2')%V
ab = (a, b)%V xs = (x1, x2)%V xs' = (x1', x2')%V
((v = #true x1 = a x2 = a x1' = b x2' = b)
(v = #false (x1 a x2 a) xs = xs'))%I.
(v = #false (x1 a x2 a) (x1, x2)%V = (x1', x2')%V))%I.
Local Opaque β.
(* TODO: This needs updating for the new atomic_syncer.
Lemma pcas_seq_spec x: atomic_seq_spec ϕ α β pcas_seq x.
Lemma pcas_seq_spec ls ab:
atomic_seq_spec (ϕ ls) (α ab) (β ab) pcas_seq (ls, ab)%V.
Proof.
iIntros (_ l) "!# _". wp_seq. iPureIntro.
iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
iDestruct "Hg" as (l1 l2 x1 x2) "(% & % & Hl1 & Hl2)".
iDestruct "Hα" as (a b) "%".
subst. simpl. iApply wp_fupd. wp_let. wp_proj. wp_load. wp_proj.
wp_op=>[?|Hx1na].
- subst.
wp_if. wp_proj. wp_load. wp_proj.
wp_op=>[?|Hx2na]. subst.
+ wp_if. wp_proj. wp_proj. wp_store. wp_proj. wp_proj. wp_store.
iDestruct ("HΦ" $! #true (b, b)%V) as "HΦ".
iApply ("HΦ" with "[Hl1 Hl2]").
{ iExists l1, l2, b, b. iFrame. eauto. }
rewrite /β. iPureIntro.
iIntros (g) "!# [HΦ H]".
iDestruct "HΦ" as (l1 l2 x1 x2) "[[% %] [HΦ1 HΦ2]]".
iDestruct "H" as (a b) "%"; subst.
wp_seq. repeat wp_proj. wp_load. repeat wp_proj.
wp_op=>[?|Hx1na]; subst.
- wp_if. repeat wp_proj. wp_load. repeat wp_proj.
wp_op=>[?|Hx2na]; subst.
+ wp_if. repeat wp_proj. wp_store. repeat wp_proj. wp_store.
iExists (b, b)%V.
iSplit.
{ iExists l1, l2, b, b. by iFrame. }
iPureIntro.
exists a, b, a, a, b, b.
repeat (split; first done). left. eauto.
+ wp_if.
iDestruct ("HΦ" $! #false (a, x2)%V) as "H".
iApply ("H" with "[Hl1 Hl2]").
iExists (a, x2)%V.
iSplit.
{ iExists l1, l2, a, x2. iFrame. eauto. }
rewrite /β. iPureIntro.
iPureIntro.
exists a, b, a, x2, a, x2. repeat (split; first done). right. eauto.
- subst. wp_if.
iDestruct ("HΦ" $! #false (x1, x2)%V) as "H".
iApply ("H" with "[Hl1 Hl2]").
- wp_if.
iExists (x1, x2)%V.
iSplit.
{ iExists l1, l2, x1, x2. iFrame. eauto. }
rewrite /β. iPureIntro.
iPureIntro.
exists a, b, x1, x2, x1, x2.
repeat (split; first done). right. eauto.
Qed.
Lemma pcas_atomic_spec (mk_syncer: val) (l1 l2: loc) (x1 x2: val) :
heapN N mk_syncer_spec N mk_syncer
heap_ctx l1 x1 l2 x2
WP sync mk_syncer pcas_seq (LitV l1, LitV l2)%V {{ f, γ, gHalf γ (x1, x2)%V x, atomic_triple' α β f x γ }}.
Lemma pcas_synced_spec (l1 l2: loc) γ s:
is_atomic_syncer (ϕ (#l1, #l2)) γ s -
WP s pcas_seq
{{ f', xs, atomic_sync_wp γ (α xs) (β xs) f' ((#l1, #l2), xs) }}.
Proof.
iIntros (HN Hmk_syncer) "(#Hh & Hl1 & Hl2)".
iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//.
- apply pcas_seq_spec.
- iFrame "Hh". iExists l1, l2, x1, x2. iFrame. eauto.
Qed.*)
End atomic_pair.
iIntros "#Hsyncer !#".
iApply wp_wand=>//.
iIntros (f') "#HΦ !#".
iIntros (xs).
iApply "HΦ".
iApply pcas_seq_spec.
Qed.
Lemma pcas_atomic_spec (mk_syncer : val) (l1 l2: loc) (x1 x2:val) :
mk_syncer_spec mk_syncer
{{{ l1 x1 l2 x2 }}}
mk_syncer #()
{{{ (s : val) γ, RET s;
WP (s pcas_seq)%V
{{ f', gHalf γ (x1, x2)%V
xs, atomic_sync_wp γ (α xs) (β xs) f' ((#l1, #l2), xs) }} }}}.
Proof.
iIntros (Hmksyncer Φ) "[Hl1 Hl2] Hsynced".
iApply (atomic_spec with "[Hl1 Hl2]"); first done.
- iAssert (ϕ (#l1, #l2) (x1, x2)) with "[-]" as "H".
{ iExists l1, l2, x1, x2. by iFrame. }
iApply "H".
- iNext.
iIntros (γ s) "[Hg Hsync]".
iApply ("Hsynced" $! s γ).
iFrame.
iApply (pcas_synced_spec with "Hsync").
Qed.
End atomic_pair.
\ No newline at end of file
......@@ -24,12 +24,15 @@ Section atomic_sync.
Definition atomic_seq_spec (ϕ: A iProp Σ) α β (f x: val) :=
( g, {{ ϕ g α g }} f x {{ v, g', ϕ g' β g g' v }})%I.
Definition atomic_sync_wp γ α β (f' x: val) :=
atomic_wp (fun g => gHalf γ g α g)%I
(fun g v => g', gHalf γ g' β g g' v)%I
(f' x)%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
atomic_triple (fun g => gHalf γ g α g)%I
(fun g v => g', gHalf γ g' β g g' v)%I
(f' x))%I.
( α β (x: val), atomic_seq_spec ϕ α β f x -
atomic_sync_wp γ α β f' x)%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
......@@ -54,25 +57,28 @@ Section atomic_sync.
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 "!#".
iSplitL "Hg2"=>//. 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".
(* TODO: Why can't I iApply "Hsynced"? *)
iSpecialize ("Hsynced" $! P Q x).
iApply wp_wand_r. iSplitL "HP".
- iApply ("Hsynced" with "[]")=>//.
iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
iIntros (Φ) "Hvss".
iApply (wp_wand with "[Hvss]").
- iApply ("Hsynced" $! Φ x)=>//.
iIntros "{Hsynced} HR". iDestruct "HR" as (g) "[Hϕ Hg1]".
(* we should view shift at this point *)
iDestruct ("Hvss" with "HP") as "Hvss'". iApply fupd_wp.
iDestruct ("Hvss") as "Hvss'". iApply fupd_wp.
rewrite atomic_shift_unfold.
iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
iDestruct (m_frag_agree with "[Hg1 Hg2]") as %Heq; first iFrame. subst.
iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "Hϕ".
{ iApply "Hseq". iFrame. done. }
iMod ("Hvs1" with "[Hg2]") as "Hvss"; first by iFrame.
rewrite /atomic_seq_spec.
iModIntro.
iApply wp_fupd.
iApply (wp_wand with "[Hϕ]").
{ iApply "Hseq". by iFrame. }
iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
iMod ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
rewrite atomic_shift_unfold.
iMod ("Hvss") as (g'') "[[Hg'' _] [_ Hvs2]]".
iSpecialize ("Hvs2" $! v).
iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
rewrite Qp_div_2.
......@@ -81,10 +87,10 @@ Section atomic_sync.
{ 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. }
iModIntro. iSplitL "Hg2 Hϕ'"=>//.
iExists g'. by iFrame.
- iIntros (?) "?". done.
- by iIntros (?) "?".
Qed.
End atomic_sync.
End atomic_sync.
\ No newline at end of file
......@@ -68,8 +68,8 @@ Section proof.
Definition installed_s R (ts: toks) (f x: val) :=
let '(γx, γ1, _, γ4, γq) := ts in
( (P: val iProp Σ) Q,
own γx ((1/2)%Qp, to_agree x) P x ({{ R P x }} f x {{ v, R Q x v }})
( Q,
own γx ((1/2)%Qp, to_agree x) (R - WP f x {{ v, R Q x v }})
saved_prop_own γq (Q x) own γ1 (Excl ()) own γ4 (Excl ()))%I.
Definition received_s (ts: toks) (x: val) γr :=
......@@ -101,12 +101,12 @@ Section proof.
let '(γx, _, γ3, _, γq) := ts in
(own γ3 (Excl ()) own γx ((1/2)%Qp, to_agree x) saved_prop_own γq Q)%I.
Lemma install_spec R P Q (f x: val) (γm γr: gname) (s: loc):
{{{ inv N (srv_bag R γm γr s) P ({{ R P }} f x {{ v, R Q v }}) }}}
Lemma install_spec R Q (f x: val) (γm γr: gname) (s: loc):
{{{ inv N (srv_bag R γm γr s) (R - WP f x {{ v, R Q v }}) }}}
install f x #s
{{{ p ts, RET #p; installed_recp ts x Q inv N (p_inv R γm γr ts p) }}}.
Proof.
iIntros (Φ) "(#? & HP & Hf) HΦ".
iIntros (Φ) "(#? & Hf) HΦ".
wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
iApply fupd_wp.
iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
......@@ -119,7 +119,7 @@ Section proof.
iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
with "[-HΦ Hx2 Ho3]") as "#HRx"; first eauto.
{ iNext. iRight. iLeft. iExists f, x. iFrame.
iExists (λ _, P), (λ _ v, Q v).
iExists (λ _ v, Q v).
iFrame. iFrame "#". }
iApply (push_spec N (p_inv' R γm γr) s #p
with "[-HΦ Hx2 Ho3]")=>//.
......@@ -143,23 +143,23 @@ Section proof.
iModIntro. wp_match. iApply ("HΦ" with "[Hor HR]"). iFrame.
- destruct ts as [[[[γx γ1] γ3] γ4] γq].
iDestruct "Hp" as (f x) "(>Hp & Hts)".
iDestruct "Hts" as (P Q) "(>Hx & Hpx & Hf' & HoQ & >Ho1 & >Ho4)".
iDestruct "Hts" as (Q) "(>Hx & Hf' & HoQ & >Ho1 & >Ho4)".
iAssert (|==> own γx (((1/2/2)%Qp, to_agree x)
((1/2/2)%Qp, to_agree x)))%I with "[Hx]" as ">[Hx1 Hx2]".
{ iDestruct (own_update with "Hx") as "?"; last by iAssumption.
rewrite -{1}(Qp_div_2 (1/2)%Qp).
by apply pair_l_frac_op'. }
wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]").
wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ]").
{ iNext. iFrame. iFrame "#". iRight. iRight. iLeft. iExists f, x. iFrame. }
iModIntro. wp_match. wp_proj. wp_proj.
wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
wp_bind (f _). iApply wp_wand_r. iSplitL "Hf' HR".
{ iApply "Hf'". iFrame. }
iIntros (v) "[HR HQ]". wp_value.
iInv N as "Hx" "Hclose".
iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
* iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
iApply excl_falso. iFrame.
* iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
* iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
* iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
wp_store. iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
......@@ -279,9 +279,9 @@ Section proof.
iNext. iIntros (s) "#Hss".
wp_let. iApply "HΦ". rewrite /synced.
iAlways. iIntros (f). wp_let. iAlways.
iIntros (P Q x) "#Hf".
iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
iIntros (Q x) "Hf".
wp_let. wp_bind (install _ _ _).
iApply (install_spec R Q f x γm γr s with "[-]")=>//.
{ iFrame. iFrame "#". }
iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
wp_let. wp_bind (loop _ _ _).
......
......@@ -26,11 +26,11 @@ Section syncer.
iApply (newlock_spec N R with "[HR]"); first done. iNext.
iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
iIntros (f). wp_let. iAlways.
iIntros (P Q x) "#Hf !# HP".
iIntros (Q x) "Hf".
wp_let. 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.
iSpecialize ("Hf" with "[R]"); 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]").
......
......@@ -12,8 +12,8 @@ Section sync.
How much more annoying? And how much to we gain in terms of things
becomign 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.
( Φ (x: val), (R - WP f x {{ v, R Φ v }}) -
WP f' x {{ Φ }})%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.
......
......@@ -99,7 +99,7 @@ Section proof.
Qed.
Definition push_triple (s: loc) (x: val) :=
atomic_triple (fun xs_hd: list val * loc =>
atomic_wp (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
......@@ -112,28 +112,28 @@ Section proof.
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.
iLöb as "IH". iIntros (Φ) "Hvs". wp_rec.
wp_let. wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
rewrite atomic_shift_unfold.
iMod "Hvs" as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "Hvs"; 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']".
rewrite atomic_shift_unfold.
iMod ("Hvs") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
destruct (decide (hd = hd')) as [->|Hneq].
* wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! #() with "[-]") as "HQ".
iMod ("Hvs'" $! #() with "[-]").
{ iExists l. iSplitR; first done. by iFrame. }
iModIntro. wp_if. eauto.
* wp_cas_fail.
iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iMod ("Hvs'" with "[-]"); first by iFrame.
iModIntro. wp_if. by iApply "IH".
Qed.
Definition pop_triple (s: loc) :=
atomic_triple (fun xs_hd: list val * loc =>
atomic_wp (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
......@@ -147,29 +147,29 @@ Section proof.
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.
iLöb as "IH". iIntros (Φ) "Hvs". wp_rec.
wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
rewrite atomic_shift_unfold.
iMod "Hvs" 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".
iMod ("Hvs'" $! NONEV with "[-Hhd]").
{ iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
iModIntro. wp_let. wp_load. wp_match.
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".
iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "Hvs".
{ 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']".
rewrite atomic_shift_unfold.
iMod "Hvs" 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".
iMod ("Hvs'" $! (SOMEV y') with "[-]").
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
destruct xs as [|x' xs''].
- simpl. iDestruct "Hhd''" as (?) "H".
......@@ -182,7 +182,7 @@ Section proof.
iFrame. }
iModIntro. wp_if. wp_proj. eauto.
+ wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iMod ("Hvs'" with "[-]"); first by iFrame.
iModIntro. wp_if. by iApply "IH".
Qed.
End proof.