CQS

[kayceesrk]

From the abstract

We introduce a new framework called the CancellableQueueSynchronizer (CQS), which enables efficient fair and abortable implementations of fundamental synchronization primitives such as mutexes, semaphores, barriers, count-down-latches, and blocking pools. Our first contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms come with formal proofs in the Iris framework for Coq. These proofs are modular, so it is easy to prove correctness for new primitives implemented on top of CQS. To validate practical impact, we integrated CQS into the Kotlin Coroutines library. Compared against Java's AbstractQueuedSynchronizer, the only practical abstraction to provide similar semantics, CQS shows significant improvements across all benchmarks, of up to two orders of magnitude. In sum, CQS is the first framework to combine expressiveness with formal guarantees and strong practical performance, and should be extensible to other languages and other families of synchronization primitives.

I would think that we can make this work with effects.

[1] https://arxiv.org/abs/2111.12682
[2] https://nikitakoval.org/talks/#hydra-2020-sqs

[bartoszmodelski]

cc @talex5 who mentioned this

[talex5]

Yeah, it's tracked in ocaml-multicore/eio#382

I have a prototype mostly working now.