In my last Colloquium talk, I presented early results of our verification of the liveness properties of mutual exclusion algorithms with atomic and non-atomic registers under the justness assumption.
In this talk, I will discuss the formal underpinnings of this work. I will give four different definitions of the concurrency relation that justness relies on, allowing us to simulate different memory models, and show how we model these in mCLR2.
Time allowing, I will also discuss the (im)possibility of deadlock and starvation freedom under certain memory models.

This is joint work with Bas Luttik and Rob van Glabbeek.