Synchronization primitives can be faster with SegmentQueueSynchronizer
summary
Presents a new synchronization abstraction called SegmentQueueSynchronizer implemented for Kotlin coroutines that starts from a novel semaphore/mutex algorithm with segment‑based wait queues, elimination (resume before suspend), synchronous/asynchronous modes, and cancellation-aware futures. Shows how cancelled cells trigger segment removal to prevent memory leaks, explains counter balancing tricks to avoid double‑counting, and reports a complete implementation plus formal correctness proofs in Iris/Coq. Claims faster, fair primitives; implementation and proofs take months and experiments are underway toward a paper.
AI-written summary · about
chapters (6)
- 0:00Start
- 2:42and Semaphores
- 9:06forward Semaphore Implementation
- 14:58Array Implementation
- 22:54ryAcquire correct?
- 48:08ore with Cancellation
related talks
15mCQS: A Formally-Verified Framework for Fair and Abortable Synchronization
40mConcurrency made easy with Kotlin Coroutines
28mConcurrency for Imposters
01h 07mThe C++20 Synchronization Library
32mStructured Concurrency: The paradigm shift
43mCoroutines for Java Developers
38mKotlin coroutines
01h 35mThinking Outside the Synchronisation Quadrant