Commit 06d9dc7d authored by Janno's avatar Janno
Browse files

Port atomic_incr to logically-atomic WP.

parent ba66f8bd
......@@ -17,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']".
......@@ -76,9 +77,13 @@ 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. iLöb as "IH".
rewrite {2}atomic_shift_unfold. iFrame "IH".
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
......@@ -90,7 +95,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".
......
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