Skip to content
Snippets Groups Projects
Commit 141a635e authored by Ralf Jung's avatar Ralf Jung
Browse files

further extend comment

parent d7b84ad4
No related branches found
No related tags found
No related merge requests found
...@@ -59,8 +59,9 @@ Section increment. ...@@ -59,8 +59,9 @@ Section increment.
(* Prove the atomic update for load *) (* Prove the atomic update for load *)
(* To [iMod] a *mask-changing* update (like "AU"), we have to unfold (* To [iMod] a *mask-changing* update (like "AU"), we have to unfold
[atomic_acc]. [atomic_acc].
Note that [iInv] would work here without unfolding, i.e., an [AACC] in Note that non-mask-changing [iMod] and [iInv] would work here without
the goal supports eliminating accessors but it does not support unfolding, i.e., an [AACC] in the goal supports eliminating
non-mask-changing updates and accessors but it does not support
eliminating mask-changing updates. *) eliminating mask-changing updates. *)
rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]". rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
(* Usually, we would use [iAaccIntro], but here we cannot because we (* Usually, we would use [iAaccIntro], but here we cannot because we
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment