一句话：提出 CQS，用队列算法与 Coq/Iris 形式化证明实现公平、可中止同步原语，并在 JVM/Kotlin 协程中落地。
并发代码难以兼顾正确与高效，程序员依赖同步抽象；但现代语言中的公平 FIFO 排序与可中止操作语义，仍缺乏既正确又高效的实现框架，异步协程频繁中止更凸显该需求。本文提出 CancellableQueueSynchronizer（CQS），通过新的队列同步算法支持互斥锁、信号量、屏障、倒计数锁存器和阻塞池等公平且可中止原语。所有算法及基于 CQS 的原语均在 Coq 的 Iris 框架中完成模块化形式化证明，便于扩展新原语。JVM 原生线程实现相较 Java AbstractQueuedSynchronizer 吞吐量提升最多两个数量级，并已集成到 Kotlin Coroutines 库，展示表达力、形式保证与实用性能的结合。
Writing concurrent code that is both correct and efficient is notoriously difficult. Thus, programmers often prefer to use synchronization abstractions, which render code simpler and easier to reason about. Despite a wealth of work on this topic, there is still a gap between the rich semantics provided by synchronization abstractions in modern programming languages—specifically, fair FIFO ordering of synchronization requests and support for abortable operations—and frameworks for implementing it correctly and efficiently. Supporting such semantics is critical given the rising popularity of constructs for asynchronous programming, such as coroutines, which abort frequently and are cheaper to suspend and resume compared to native threads. This paper introduces a new framework called CancellableQueueSynchronizer (CQS), which enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives: mutexes, semaphores, barriers, count-down latches, and blocking pools. Our main contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms, including the CQS framework and the primitives built on top of it, come with formal proofs in the Iris framework for Coq for many of their properties. These proofs are modular, so it is easy to show correctness for new primitives implemented on top of CQS. From a practical perspective, implementation of CQS for native threads on the JVM improves throughput by up to two orders of magnitude over Java’s AbstractQueuedSynchronizer, the only practical abstraction offering similar semantics. Further, we successfully integrated CQS as a core component of the popular Kotlin Coroutines library, validating the framework’s practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer is the first framework to combine expressiveness with formal guarantees and solid practical performance. Our approach should be extensible to other languages and families of synchronization primitives.
@article{paperbot1985,
title = {CQS: A Formally-Verified Framework for Fair and Abortable Synchronization},
author = {Nikita Koval and Dmitry Khalanskiy and Dan Alistarh},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591230}
}