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, \emph{fair} FIFO ordering of synchronization requests and support for \emph{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 \texttt{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 \emph{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 significantly improves Java's \texttt{AbstractQueuedSynchronizer}, the only practical abstraction offering similar semantics. In sum, \texttt{CancellableQueueSynchronizer} is the first framework to combine expressiveness with formal guarantees and solid practical performance.

翻译：编写既正确又高效的并发代码众所周知地困难。因此，程序员通常倾向于使用同步抽象，这使代码更简洁且更易于推理。尽管该领域已有大量工作，但现代编程语言中同步抽象所提供的丰富语义——具体而言，同步请求的 *公平* FIFO 排序以及对 *可中断* 操作的支持——与正确高效实现这些语义的框架之间仍存在差距。鉴于异步编程构造（如协程）日益流行，且这些构造频繁中断且挂起/恢复成本低于原生线程，支持此类语义至关重要。本文提出一个名为 \texttt{CancellableQueueSynchronizer} (CQS) 的新框架，能够简单而高效地实现多种公平且可中断的同步原语：互斥锁、信号量、屏障、倒计时门闩以及阻塞池。我们的主要贡献在于算法层面，因为在如此通用的层面上高效实现公平性与可中断性并非易事。重要的是，我们所有算法——包括 CQS 框架及其上构建的原语——均针对其多项属性，在面向 Coq 的 Iris 框架中提供了 *形式化证明*。这些证明是模块化的，因此容易证明基于 CQS 实现的新原语的正确性。从实践角度看，在 JVM 上针对原生线程实现的 CQS 显著改进了 Java 的 \texttt{AbstractQueuedSynchronizer}——这是唯一提供类似语义的实用抽象。总之，\texttt{CancellableQueueSynchronizer} 是首个将表达能力、形式化保证与扎实的实践性能相结合的框架。