CQS: A Formally-Verified Framework for Fair and Abortable Synchronization
summary
CQS provides a queue-based synchronizer that implements fair FIFO ordering and efficient abortable operations by reserving array slots for suspend and resume tokens so resume can safely precede suspend; algorithms cover mutexes, semaphores, barriers, latches and blocking pools. All algorithms come with modular machine-checked Iris/Coq proofs and a JVM implementation that integrates into Kotlin Coroutines and shows throughput improvements of up to two orders of magnitude versus Java’s AbstractQueuedSynchronizer.
AI-written summary · about
chapters (6)
- 0:00CQS framework intro
- 2:32Fair mutex with coroutines
- 8:56Semaphores and performance
- 11:29Barriers and primitives
- 12:51Formal verification
- 13:14Q&A
related talks
01h 14mSynchronization primitives can be faster with SegmentQueueSynchronizer
01h 35mThinking Outside the Synchronisation Quadrant
21mMechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr
01h 02mIntro to Concurrent Programming 2/3: Modern Queues and Flat Combining
01h 24mConcurrency in C++20 and Beyond
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
01h 07mThe C++20 Synchronization Library
01h 05mAn Interesting Lock-free Queue - Part 2 of N