A Proof Recipe for Linearizability in Relaxed Memory Separation Logic

Explore a groundbreaking 19-minute video presentation from PLDI 2024 that introduces a novel proof recipe for linearizability in relaxed memory separation logic. Delve into the challenges of verifying concurrent objects under relaxed memory consistency and discover how the proposed object modification order (OMO) concept addresses event reordering and view transfer tracking. Learn about the innovative commit-with relation that enables proof reuse in concurrent libraries. Witness the first-time verification of linearizability for the Michael–Scott queue, elimination stack, and Folly's MPMC queue in relaxed memory consistency, as well as stronger specifications for spinlocks and atomic reference counting. Access the accompanying article and supplementary archive for a comprehensive understanding of this significant advancement in concurrent separation logic.

[PLDI24] A Proof Recipe for Linearizability in Relaxed Memory Separation Logic