Skip to content

In logatom lock: Formalize that the lock is Free before acquire.

Robbert Krebbers requested to merge robbert/logatom_lock_free into master

This makes it consistent with the Iris 1 appendix:

image

I think it also makes the spec strictly stronger because you learn the lock was unlocked before the linearization point.

Merge request reports