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 [1] for writing concurrent tests was introduced. Users list all the data structure operations, and Lincheck verifies whether these operations are thread-safe, examining them with a model checker and providing a detailed execution trace when detecting a bug. This trace includes all shared memory access and synchronization events so that you can understand in what order the operations were executed and pinpoint the root cause of the bug.

Recently, we developed an IntelliJ IDEA plugin [2] for Lincheck, which offers record-and-replay debugging (a.k.a. time-traveling debugging) to allow you to study the execution trace. The plugin provides native debugging experience and out-of-the-box data structure visualization in the IDE. This talk presents Lincheck and its integration with IntelliJ IDEA, explaining how you can apply the tool to your setting and giving a brief overview of the framework’s internals.

[1] https://github.com/JetBrains/lincheck
[2] https://plugins.jetbrains.com/plugin/24171-lincheck