Generalising Concurrent Correctness to Weak Memory

Brijesh Dongol

Understanding correctness of implementations of atomic objects has been an important problem for over three decades. In this talk, we develop a correctness condition, causal atomicity; a generalisation of correctness for concurrent implementations of atomic objects. First, it generalises the meaning of atomicity to the setting of weak memory models, where memory events are only partially ordered with respect to a happens-before relation. Second, it captures both linearizability (for concurrent objects) and opacity (for transactional memory (TM)). Causal atomicity gives rise to conditions, causal linearizability and causal opacity, suitable for weak memory, both of which are natural generalisations of their respective classical definitions whenever the memory events are totally ordered. Moreover, since causal atomicity is compositional, our result allows one to freely compose causally linearizable objects and causally opaque TMs. We also show that causal atomicity guarantees observational refinement, ensuring that every behaviour of a client when it uses a causally atomic object is a possible behaviour when it uses the corresponding abstract (sequential object).

This is joint work with Simon Doherty, John Derrick and Heike Wehrheim.