Lincheck 指南

Lincheck is a practical and user-friendly framework for testing concurrent algorithms on the JVM. It provides a simple and declarative way to write concurrent tests.

With the Lincheck framework, instead of describing how to perform tests, you can specify what to test by declaring all the operations to examine and the required correctness property. As a result, a typical concurrent Lincheck test contains only about 15 lines.

When given a list of operations, Lincheck automatically:

  • Generates a set of random concurrent scenarios.
  • Examines them using either stress-testing or bounded model checking.
  • Verifies that the results of each invocation satisfy the required correctness property (linearizability is the default one).

Add Lincheck to your project

To enable the Lincheck support, include the corresponding repository and dependency to the Gradle configuration. In your build.gradle(.kts) file, add the following:

【Kotlin】

  1. repositories {
  2.     mavenCentral()
  3. }
  5. dependencies {
  6.     testImplementation("org.jetbrains.kotlinx:lincheck:2.23")
  7. }

【Groovy】

  1. repositories {
  2.     mavenCentral()
  3. }
  5. dependencies {
  6.     testImplementation "org.jetbrains.kotlinx:lincheck:2.23"
  7. }

Explore Lincheck

This guide will help you get in touch with the framework and try the most useful features with examples. Learn the Lincheck features step-by-step:

  1. Write your first test with Lincheck
  2. Choose your testing strategy
  3. Configure operation arguments
  4. Consider popular algorithm constraints
  5. Check the algorithm for non-blocking progress guarantees
  6. Define sequential specification of the algorithm

Additional references

  • “How we test concurrent algorithms in Kotlin Coroutines” by Nikita Koval: Video. KotlinConf 2023
  • “Lincheck: Testing concurrency on the JVM” workshop by Maria Sokolova: Part 1, Part 2. Hydra 2021