Reverting to old (stronger) definition of atomicity
In Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: e
is atomic if for any e'
such that e
reduces to e'
we have that e'
is stuck.
The old definition was: e
is atomic if for any e'
such that e
reduces to e'
we have that e'
is a value.
These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike WP
do not guarantee safety, e.g., IC
(if convergent predicates).
Edited by Ralf Jung