How to write a robust test for a concurrent data structure? 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.

Talk Level:

Nikita Koval is a researcher in the Kotlin team at JetBrains and a Team Lead for the Concurrent Computing Lab at JetBrains Research. Nikita has recently redesigned internal synchronization in Kotlin coroutines and has been leading the development of the Lincheck framework, simplifying the testing of concurrent data structures. His primary research interests include but are not limited to concurrent data structures and algorithms, their verification, and practically applicable code analysis.