Commit 8d5768cb authored by Ralf Jung's avatar Ralf Jung

Merge branch 'uncurried-specs' into 'master'

Simpler syncer specs

This simplifies the syncer specs.
The sequential syncer only is slightly improved, by changing
```
  Definition synced R (f' f: val) :=
    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) →
                       ({{ P x }} f' x {{ v, Q x v }}))%I.
```
such that `P`, `Q` don't factor in a dependency on `x` any more. Since all three are quantified at the same time, the two specs are equivalent -- and the one where `P` is not a predicate and `Q` is exactly the postcondition is arguably simpler:
```
  Definition synced R (f f': val) :=
    (□ ∀ P Q (x: val), ({{ R ★ P }} f x {{ v, R ★ Q v }}) →
                       ({{ P }} f' x {{ Q }}))%I.
```

For the atomic spec, the changes are deeper. The currying on some location `l` is entirely removed. `is_atomic_syncer` better mirrors `is_syncer` from the sequential version. And finally, we use "original" atomic triples and not some modified version thereof (so `atomic_triple_base` is killed).

TODO: Fix `atomic_pcas.v`, it relied on the location currying done by `atomic_sync.v`. However, I don't entirely grok that file. @zhangz could you give that a look?

See merge request !1
parents 6396d121 908a83a4
05a588df59ddfdc2e7a4aec5a98a50614c819693
6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838
......@@ -6,24 +6,18 @@ From iris.prelude Require Export coPset.
Import uPred.
Section atomic.
Context `{irisG Λ Σ} (A: Type).
Context `{irisG Λ Σ} {A: Type}.
(* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
(* TODO RJ: Don't define atomic_triple_base; everybody should only ever use atomic_triple anyway. *)
(* TODO RJ: We probably will want to make `A` an implicit parameter. *)
Definition atomic_triple_base
(* 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 _) P Q : iProp Σ :=
((P ={Eo, Ei}=> x:A,
(e: expr _) : iProp Σ :=
( P Q, (P ={Eo, Ei}=> x:A,
α x
((α x ={Ei, Eo}= P)
( v, β x v ={Ei, Eo}= Q x v))
) - {{ P }} e @ {{ v, ( x: A, Q x v) }})%I.
(* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
Definition atomic_triple α β Ei Eo e := ( P Q, atomic_triple_base α β Ei Eo e P Q)%I.
Arguments atomic_triple {_} _ _ _ _.
( v, β x v ={Ei, Eo}= Q v))
) - {{ P }} e @ {{ Q }})%I.
End atomic.
......@@ -19,11 +19,11 @@ 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
(nclose heapN)
(incr #l).
atomic_triple (fun (v: Z) => l #v)%I
(fun v ret => ret = #v l #(v + 1))%I
(nclose heapN)
(incr #l).
Lemma incr_atomic_spec: (l: loc), heapN N heap_ctx incr_triple l.
Proof.
......@@ -46,7 +46,7 @@ Section incr.
iSpecialize ("Hvs'" $! #x').
wp_cas_suc.
iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
iModIntro. wp_if. iModIntro. by iExists x'.
iModIntro. wp_if. done.
- iDestruct "Hvs'" as "[Hvs' _]".
wp_cas_fail.
iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
......@@ -80,7 +80,7 @@ Section user.
(* prove worker triple *)
iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
rewrite /incr_triple /atomic_triple.
iSpecialize ("Hincr" $! True%I (fun _ _ => True%I) with "[]").
iSpecialize ("Hincr" $! True%I (fun _ => True%I) with "[]").
- iIntros "!# _".
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
......
......@@ -33,13 +33,14 @@ Section atomic_pair.
Local Opaque β.
Lemma pcas_seq_spec: seq_spec N pcas_seq ϕ α β .
(* TODO: This needs updating for the new atomic_syncer.
Lemma pcas_seq_spec x: atomic_seq_spec ϕ α β pcas_seq x.
Proof.
iIntros (_ l) "!# _". wp_seq. iModIntro. iPureIntro.
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. wp_let. wp_proj. wp_load. wp_proj.
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.
......@@ -75,6 +76,6 @@ Section atomic_pair.
iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//.
- apply pcas_seq_spec.
- iFrame "Hh". iExists l1, l2, x1, x2. iFrame. eauto.
Qed.
Qed.*)
End atomic_pair.
......@@ -15,63 +15,52 @@ Proof. by intros ?%subG_inG. Qed.
Section atomic_sync.
Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))} (N : namespace).
(* 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, DecAgree g).
Definition atomic_triple'
(α: val A iProp Σ)
(β: val A A val iProp Σ)
(Ei Eo: coPset)
(f x: val) γ : iProp Σ :=
( P Q, atomic_triple_base A (fun g => gHalf γ g α x g)
(fun g v => g':A, gHalf γ g' β x g g' v)
Ei Eo
(f x) (P x) (fun _ => Q x))%I.
Definition atomic_seq_spec (ϕ: A iProp Σ) α β (f x: val) :=
( g, {{ ϕ g α g }} f x {{ v, g', ϕ g' β g g' v }})%I.
Definition sync (mk_syncer: val) : val :=
λ: "f_seq" "l",
let: "s" := mk_syncer #() in
"s" ("f_seq" "l").
(* 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.
Definition seq_spec (f: val) (ϕ: val A iProp Σ) α β (E: coPset) :=
(Φ: val iProp Σ) (l: val),
{{ True }} f l {{ f', ( (x: val) (Φ: val iProp Σ) (g: A),
heapN N
heap_ctx ϕ l g α x g
( (v: val) (g': A),
ϕ l g' - β x g g' v ={E}= Φ v)
WP f' x @ E {{ Φ }} )}}.
(* The linear view shift in the above post-condition is for the final step
of computation. The client side of such triple will have to prove that the
specific post-condition he wants can be lvs'd from whatever threaded together
by magic wands. The library side, when proving seq_spec, will always have
a view shift at the end of evalutation, which is exactly what we need. *)
(* 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.
Lemma atomic_spec (mk_syncer f_seq l: val) (ϕ: val A iProp Σ) α β Ei:
(g0: A),
heapN N seq_spec f_seq ϕ α β
mk_syncer_spec N mk_syncer
heap_ctx ϕ l g0
WP (sync mk_syncer) f_seq l {{ f, γ, gHalf γ g0 x, atomic_triple' α β Ei f x γ }}.
Definition atomic_syncer_spec (mk_syncer: val) :=
(g0: A) (ϕ: A iProp Σ),
heapN N
{{{ heap_ctx ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 is_atomic_syncer ϕ γ s }}}.
Lemma atomic_spec (mk_syncer: val):
mk_syncer_spec N mk_syncer atomic_syncer_spec mk_syncer.
Proof.
iIntros (g0 HN Hseq Hsync) "[#Hh Hϕ]".
iIntros (Hsync g0 ϕ HN ret) "[#Hh Hϕ] Hret".
iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
{ by rewrite pair_op dec_agree_idemp. }
repeat wp_let. wp_bind (mk_syncer _).
iApply (Hsync ( g: A, ϕ l g gHalf γ g)%I)=>//. iFrame "Hh".
iSplitL "Hg1 Hϕ".
iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[$Hh Hg1 Hϕ]")=>//.
{ iExists g0. by iFrame. }
iIntros (s) "#Hsyncer".
wp_let. wp_bind (f_seq _). iApply wp_wand_r.
iSplitR; first iApply Hseq=>//; auto.
iIntros (f) "%".
iApply wp_wand_r.
iSplitR; first iApply "Hsyncer".
iIntros (f') "#Hsynced".
iExists γ. iFrame.
iIntros (x). iAlways.
iIntros (P Q) "#Hvss".
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".
iIntros (P Q) "#Hvss !# HP".
(* TODO: Why can't I iApply "Hsynced"? *)
iSpecialize ("Hsynced" $! P Q x).
iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
iApply wp_wand_r. iSplitL "HP".
- iApply ("Hsynced" with "[]")=>//.
iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
(* we should view shift at this point *)
......@@ -79,10 +68,11 @@ Section atomic_sync.
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 H=>//.
iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
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]]".
iSpecialize ("Hvs2" $! ret).
iSpecialize ("Hvs2" $! v).
iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
rewrite Qp_div_2.
iAssert (|==> own γ (((1 / 2)%Qp, DecAgree g') ((1 / 2)%Qp, DecAgree g')))%I
......@@ -93,7 +83,7 @@ Section atomic_sync.
{ iExists g'. iFrame. }
iModIntro. iSplitL "Hg2 Hϕ'"; last done.
iExists g'. by iFrame.
- iIntros (?) "?". by iExists g0.
- iIntros (?) "?". done.
Qed.
End atomic_sync.
......@@ -130,9 +130,9 @@ Section proof.
by iApply "HΦ".
Qed.
Definition installed_recp (ts: toks) (x: val) (Q: val val iProp Σ) :=
Definition installed_recp (ts: toks) (x: val) (Q: val iProp Σ) :=
let '(γx, _, γ3, _, γq) := ts in
(own γ3 (Excl ()) own γx ((1/2)%Qp, DecAgree x) saved_prop_own γq (Q x))%I.
(own γ3 (Excl ()) own γx ((1/2)%Qp, DecAgree x) saved_prop_own γq Q)%I.
Lemma install_spec
R P Q
......@@ -140,7 +140,7 @@ Section proof.
(Φ: val iProp Σ):
heapN N
heap_ctx inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
P x ({{ R P x }} f x {{ v, R Q x v }})
P ({{ R P }} f x {{ v, R Q v }})
( (p: loc) (ts: toks), installed_recp ts x Q - evm γm p ts -( hd, evs γs hd #p) - Φ #p)
WP install f x #s {{ Φ }}.
Proof.
......@@ -151,7 +151,7 @@ Section proof.
iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) (Q x)%I) as (γq) "#?".
iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) Q) as (γq) "#?".
iInv N as "[Hrs >Hm]" "Hclose".
iDestruct "Hm" as (m) "[Hm HRm]".
destruct (m !! p) eqn:Heqn.
......@@ -170,8 +170,10 @@ Section proof.
iApply install_push_spec=>//.
iFrame "#". rewrite /evm /installed_s. iFrame.
iSplitL "Hpx Hf".
{ iExists P, Q. by iFrame. }
iIntros "Hhd". wp_seq. iModIntro.
{ (* TODO: Something somewhere can be simplified so that we don't have
to add these dummy arguments any more. *)
iExists (fun _ => P), (fun _ => Q). by iFrame. }
iIntros "Hhd". wp_seq.
iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
{ rewrite /installed_recp. iFrame. iFrame "#". }
by iApply ("HΦ" with "[]").
......@@ -206,7 +208,7 @@ Section proof.
iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
iModIntro. wp_match. iModIntro. iApply ("HΦ'" with "[Hor HR]"). iFrame.
iModIntro. wp_match. iApply ("HΦ'" with "[Hor HR]"). iFrame.
+ iDestruct "Hp" as (f' x') "(Hp & Hs)".
wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
......@@ -227,7 +229,7 @@ Section proof.
wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
{ iApply "Hf'". iFrame. }
iIntros (v) "[HR HQ]".
wp_value. iModIntro. iInv N as "[Hs >Hm]" "Hclose".
wp_value. iInv N as "[Hs >Hm]" "Hclose".
iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
iDestruct "HRs" as (m') "[>Hom HRs]".
iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
......@@ -304,8 +306,8 @@ Section proof.
Proof.
iIntros (?) "(#? & #? & #? & HΦ)".
wp_seq. wp_let.
wp_bind (try_acquire _). iApply try_acquire_spec.
iFrame "#". iNext. iIntros ([]); last by (iIntros; wp_if).
wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
iNext. iIntros ([]); last by (iIntros; wp_if).
(* acquired the lock *)
iIntros "[Hlocked [Ho2 HR]]".
wp_if. wp_bind (! _)%E.
......@@ -320,8 +322,8 @@ Section proof.
{ iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) R v = #()))%I=>//.
iFrame "#". iFrame. iIntros "? ?". by iFrame. }
iIntros (f') "[Ho [HR %]]". subst.
wp_let. iApply release_spec. iFrame "#".
iFrame. iNext. iIntros. done.
wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#★".
iNext. iIntros. done.
Qed.
Lemma loop_spec R (p s: loc) (lk: val)
......@@ -390,20 +392,20 @@ Section proof.
Lemma mk_flat_spec: mk_syncer_spec N mk_flat.
Proof.
iIntros (R Φ HN) "(#Hh & HR & HΦ)".
iIntros (R HN Φ) "(#Hh & HR) HΦ".
iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
iMod (own_alloc ( (: tokmR) )) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
{ iExists . iFrame. by rewrite big_sepM_empty. }
wp_seq. wp_bind (newlock _).
iApply (newlock_spec _ (own γr (Excl ()) R))%I=>//.
iFrame "Hh Ho2 HR". iNext. iIntros (lk γlk) "#Hlk".
iApply (newlock_spec _ (own γr (Excl ()) R)%I with "[$Hh $Ho2 $HR]")=>//.
iNext. iIntros (lk γlk) "#Hlk".
wp_let. wp_bind (new_stack _).
iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
iFrame "Hh Hm". iIntros (γ s) "#Hss".
wp_let. iModIntro. iApply "HΦ". rewrite /synced.
wp_let. iApply "HΦ". rewrite /synced.
iAlways.
iIntros (f). wp_let. iModIntro. iAlways.
iIntros (f). wp_let. iAlways.
iIntros (P Q x) "#Hf".
iIntros "!# Hp". wp_let.
wp_bind (install _ _ _).
......
......@@ -92,7 +92,7 @@ Lemma new_stack_spec' Φ RI:
heap_ctx RI ( γ s : loc, inv N (( xs, is_stack' R γ xs s) RI) - Φ #s)
WP new_stack #() {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & HR & HΦ)".
iIntros (HN) "(#Hh & HR & HΦ)". iApply wp_fupd.
iMod (own_alloc ( (: evmapR loc val unitR) )) as (γ) "[Hm Hm']".
{ apply auth_valid_discrete_2. done. }
wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
......@@ -115,10 +115,10 @@ Lemma new_stack_spec' Φ RI:
induction xs as [|x xs' IHxs'].
- simpl. iIntros (hd f f' HN ? ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
iDestruct "Hxs1" as (q) "Hhd".
wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
wp_rec. wp_value. wp_let. wp_load. wp_match. by iApply "HΦ".
- simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. wp_proj.
wp_rec. wp_value. wp_let. wp_load. wp_match. wp_proj.
wp_bind (f' _). iApply Hf=>//. iFrame "#".
iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
......@@ -133,7 +133,7 @@ Lemma new_stack_spec' Φ RI:
Proof.
iIntros (HN) "(#Hh & HRx & #? & HΦ)".
iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
iSpecialize ("Hpush" $! (R x) (fun _ ret => ( hd, evs γ hd x) ret = #())%I with "[]").
iSpecialize ("Hpush" $! (R x) (fun ret => ( hd, evs γ hd x) ret = #())%I with "[]").
- iIntros "!# Rx".
(* open the invariant *)
iInv N as "[IH1 ?]" "Hclose".
......@@ -180,7 +180,7 @@ Lemma new_stack_spec' Φ RI:
iModIntro. iSplitL; last auto. by iExists hd'.
- iApply wp_wand_r. iSplitL "HRx Hpush".
+ by iApply "Hpush".
+ iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst.
+ iIntros (?) "[? %]". subst.
by iApply "HΦ".
Qed.
......
......@@ -23,20 +23,19 @@ Section syncer.
Lemma mk_sync_spec: mk_syncer_spec N mk_sync.
Proof.
iIntros (R Φ HN) "(#Hh & HR & HΦ)".
iIntros (R HN Φ) "(#Hh & HR) HΦ".
wp_seq. wp_bind (newlock _).
iApply newlock_spec; first done.
iSplitL "HR"; first by iFrame. iNext.
iApply (newlock_spec _ R with "[$Hh $HR]"); first done. iNext.
iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
iIntros (f). wp_let. iModIntro. iAlways.
iIntros (f). wp_let. iAlways.
iIntros (P Q x) "#Hf !# HP".
wp_let. wp_bind (acquire _).
iApply acquire_spec. iSplit; first done. iNext.
iApply (acquire_spec with "Hl"). iNext.
iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
iDestruct ("Hf" with "[R HP]") as "Hf'"; first by iFrame.
iApply wp_wand_r. iSplitL "Hf'"; first done.
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. iFrame "HR Hl Hlocked".
iApply (release_spec with "[$HR $Hl $Hlocked]").
iNext. iIntros "_". by wp_seq.
Qed.
End syncer.
......@@ -7,15 +7,22 @@ From iris.heap_lang Require Import proofmode notation.
Section sync.
Context `{!heapG Σ} (N : namespace).
Definition synced R (f' f: val) :=
( P Q (x: val), ({{ R P x }} f x {{ v, R Q x v }})
({{ P x }} f' x {{ v, Q x v }}))%I.
(* 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? *)
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.
( (f : val), WP s f {{ f', synced R f f' }})%I.
Definition mk_syncer_spec (mk_syncer: val) :=
(R: iProp Σ) (Φ: val -> iProp Σ),
heapN N
heap_ctx R ( s, is_syncer R s - Φ s) WP mk_syncer #() {{ Φ }}.
(R: iProp Σ), heapN N
{{{ heap_ctx R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
End sync.
......@@ -107,15 +107,15 @@ 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
(nclose heapN)
(push #s x).
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
(nclose heapN)
(push #s x).
Lemma push_atomic_spec (s: loc) (x: val) :
heapN N heap_ctx push_triple s x.
......@@ -133,7 +133,7 @@ Section proof.
* wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! #() with "[-]") as "HQ".
{ iExists l. iSplitR; first done. by iFrame. }
iModIntro. wp_if. iModIntro. eauto.
iModIntro. wp_if. eauto.
* wp_cas_fail.
iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
......@@ -141,16 +141,16 @@ 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
(nclose heapN)
(pop #s).
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
(nclose heapN)
(pop #s).
Lemma pop_atomic_spec (s: loc):
heapN N heap_ctx pop_triple s.
......@@ -167,7 +167,7 @@ Section proof.
iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
{ iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
iModIntro. wp_let. wp_load. wp_match.
iModIntro. eauto.
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' _]".
......
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