Commit 25f6e916 authored by Zhen Zhang's avatar Zhen Zhang
Browse files

Fix FIXME in atomic.v

parent eb5b9b57
...@@ -61,19 +61,16 @@ Section demo. ...@@ -61,19 +61,16 @@ Section demo.
wp_load. wp_load.
iVs ("Hvs'" with "Hl") as "HP". iVs ("Hvs'" with "Hl") as "HP".
iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op. iVsIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
(* iVs ("Hvs" with "HP") as (x) "[Hl Hvs']". (* FIXME: Can't apply, bug? *) *)
iApply (wp_atomic heapN _); first by solve_atomic.
iVs ("Hvs" with "HP") as (x') "[Hl Hvs']". iVs ("Hvs" with "HP") as (x') "[Hl Hvs']".
destruct (decide (x = x')). destruct (decide (x = x')).
- subst. - subst.
iDestruct "Hvs'" as "[_ Hvs']". iDestruct "Hvs'" as "[_ Hvs']".
iSpecialize ("Hvs'" $! #x'). iSpecialize ("Hvs'" $! #x').
iVsIntro.
wp_cas_suc. wp_cas_suc.
iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame. iVs ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
iVsIntro. wp_if. iVsIntro. by iExists x'. iVsIntro. wp_if. iVsIntro. by iExists x'.
- iDestruct "Hvs'" as "[Hvs' _]". - iDestruct "Hvs'" as "[Hvs' _]".
iVsIntro. wp_cas_fail. wp_cas_fail.
iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame. iVs ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
iVsIntro. wp_if. by iApply "IH". iVsIntro. wp_if. by iApply "IH".
Qed. Qed.
......
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