Concurrent Algorithms
in Kotlin Coroutines

What were the design goals of the coroutines in Kotlin, and how are they implemented on the JVM? What is the concept behind suspending functions in Kotlin, and how are they implemented? Exactly what happens when you launch coroutines, and how much actual overhead do they have? This talk answers these and lots of other coroutine-related questions, showing and explaining the corresponding byte code produced by the Kotlin compiler with code samples and benchmarks.

Coroutines provide end-users with new programming paradigms that present unique challenges to the design of an efficient scheduler, whose task is to allocate coroutines among operating system threads. We will contrast the coroutines workloads to more traditional fork-join workloads, show the benchmarks that drove the design of a dedicated coroutines scheduler, and discuss its algorithm, implementation details, and engineering trade-offs.

The key data structure enabling communication between coroutines is the rendezvous channel. In essence, it is a blocking queue of size zero, so both send(e) and receive() operations wait for one another, performing a rendezvous when they meet. To optimize the message-passing pattern, channels are usually equipped with a fixed-size buffer, so sends do not suspend and put elements into the buffer until its capacity is exceeded. This primitive is known as a buffered channel. This talk presents a fast and scalable algorithm for both rendezvous and buffered channels developed for Kotlin coroutines.

This talk is based on our PPoPP '23 paper.

Programmers often use synchronization abstractions, such as mutex, semaphore, barriers, and count-down latches, to simplify their code. Despite much work in this area, only a few algorithms support both fair FIFO ordering of synchronization requests and abortability. Supporting such semantics is critical for coroutines, which abort frequently and are cheaper to suspend and resume than native threads. This talk introduces a new CancellableQueueSynchronizer (CQS) framework for Kotlin coroutines that enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives. Besides the algorithmic contribution, we also proved the correctness of all algorithms in Coq and compared them with the primitives in the standard Java library, demonstrating significant improvement.

This talk is based on our PLDI '23 paper.

Kotlin coroutines are used to maintain a dozen non-trivial concurrent data structures, which need to be tested properly. Straightforward stress tests are unlikely to catch all possible bugs and flack periodically. The quality of such testing is below the bar. We need a way to write concurrent tests in a convenient, declarative way, keeping in mind "what" we are testing as opposed to "how" we are testing it. With this in mind, the Lincheck framework for writing concurrent tests was introduced. Users list all the data structure operations, and Lincheck verifies whether these operations are thread-safe. This talk presents Lincheck and explains how you can apply it to your setting while also giving a brief overview of the framework’s internals.

This talk is based on our CAV '23 paper.