A Proof Recipe for Linearizability in Relaxed Memory Separation Logic

• Published in: Proceedings of ACM on programming languages 2024-06, Vol.8 (PLDI), p.175-198, Article 154
• Main Authors: Park, Sunho, Kim, Jaewoo, Mulder, Ike, Jung, Jaehwang, Lee, Janggun, Krebbers, Robbert, Kang, Jeehoon
• Format: Article
• Language: English
• Subjects: Automated reasoning; Concurrency; Separation logic; Theory of computation
• ISSN: 2475-1421; 2475-1421
• DOI: 10.1145/3656384

Linearizability is the de facto standard for correctness of concurrent objects—it essentially says that all the object’s operations behave as if they were atomic. There have been a number of recent advances in developing increasingly strong linearizability specifications for relaxed memory consistency (RMC), but scalable proof methods for these specifications do not exist due to the challenges arising from out-of-order executions (requiring event reordering) and selected synchronization (requiring tracking of view transfers). We propose a proof recipe for the linearizable history specifications by Dang et al. in the Iris-based iRC11 concurrent separation logic in Coq. Key to our proof recipe is the notion of object modification order (OMO), which generalizes the modification order of the C11 memory model to an object-local setting. Using OMO we minimize the conditions that need to be proved for event reordering. To enable proof reuse for concurrent libraries that are built on top of others, OMO provides the novel notion of a commit-with relation that connects the linearization points of the lower and upper libraries. Using our recipe, we verify the linearizability of the Michael–Scott queue, the elimination stack, and Folly’s MPMC queue in RMC for the first time; and verify stronger specifications of a spinlock and atomic reference counting in RMC than prior work.