CQS: A Formally-Verified Framework for Fair and Abortable Synchronization

Explore a conference talk introducing CancellableQueueSynchronizer (CQS), a novel framework for implementing fair and abortable synchronization primitives. Delve into the challenges of concurrent programming and the importance of synchronization abstractions in modern programming languages. Learn about CQS's ability to support efficient implementations of mutexes, semaphores, barriers, count-down latches, and blocking pools. Discover the formal proofs developed using the Iris framework for Coq, ensuring the correctness of CQS and its derived primitives. Examine the practical implications of CQS, including its performance improvements over Java's AbstractQueuedSynchronizer and its integration into the Kotlin Coroutines library. Gain insights into how CQS combines expressiveness, formal guarantees, and practical performance in the realm of concurrent programming.

[PLDI24] [PLDI 2023] CQS: A Formally-Verified Framework for Fair and Abortable Synchronization