Lincheck: concurrency tests that fail with a schedule you can replay

The product of the tool is the failure report, not the detection

Lincheck is a practical framework for writing deterministic and reproducible concurrent tests on the JVM, and the README puts the emphasis in an unusual place. It does not lead with finding bugs. It leads with what happens after one is found: Lincheck provides a reproducible execution trace and the ability to debug it step by step in IntelliJ IDEA.

That reframing is the whole idea. A concurrency test that fails once in fifty runs tells you almost nothing, because the passing runs are the majority and the failing one is a schedule you cannot reproduce on demand. A tool that records the interleaving converts a flaky test into a fixed report, and the report is a table of what each thread did and when it switched.

The audience is therefore JVM engineers writing concurrent code, whether that is a collection implementation, a lock-based component or a piece of application logic with shared state. The framework grew out of JetBrains work on data structures, and version 3.0 widened the scope: Lincheck now focuses on testing arbitrary concurrent code while still providing a declarative API for testing concurrent data structures.

The project is a JetBrains official project, and the implementation is Kotlin, which fits a tool whose main job is instrumenting a running JVM and replaying a schedule.

Two checking modes decide how hard the framework works

The engine behind both styles of test is the same. When you wrap your concurrent logic in the runConcurrentTest function, Lincheck automatically studies different thread interleavings and reports an error if one leads to a test failure. For data structures it generates a set of random concurrent scenarios and examines them using either stress-testing or bounded model checking, then verifies that the results of each invocation satisfy the required correctness property, which is linearizability by default.

The two modes are the important choice, and the difference in effort is large. Stress testing runs random scenarios and lets the scheduler produce interleavings, so it is the cheap mode and it finds the bugs that are easy to hit. Model checking is the expensive mode: it searches the space of interleavings within a bound and, when it finds a violation, produces a short concurrent scenario that discovers the bug, with a detailed execution trace to reproduce it.

In the example the README gives, the same class is checked twice, once in each mode.

    // Run Lincheck in the stress testing mode
    @Test
    fun stressTest() = StressOptions().check(this::class)

    // Run Lincheck in the model checking testing mode
    @Test
    fun modelCheckingTest() = ModelCheckingOptions().check(this::class)

A team that runs both gets the cheap detection in the inner loop and the exhaustive search in a slower job. The model checking mode is also the one that finds the shallow bug, because it does not need luck to reach a rare interleaving.

Declarative operation lists are how data structures are tested

For a concurrent data structure you do not describe how to test it, you describe what to test. Instead of writing the test procedure, you declare all the data structure operations to examine, and Lincheck takes it from there by generating random concurrent scenarios and checking the results against the correctness property.

Each operation is marked with an annotation, and the class under test is handed to the checker. The example in the README is a test for the standard Java ConcurrentLinkedDeque, and it declares the six operations that matter: adding and removing at both ends, and peeking at both ends.

    @Operation
    fun addFirst(e: Int) = deque.addFirst(e)
    @Operation
    fun addLast(e: Int) = deque.addLast(e)
    @Operation
    fun pollFirst() = deque.pollFirst()
    @Operation
    fun pollLast() = deque.pollLast()
    @Operation
    fun peekFirst() = deque.peekFirst()
    @Operation
    fun peekLast() = deque.peekLast()

The README states that this test easily finds a bug in the standard Java ConcurrentLinkedDeque, and the failure it reports is the interesting part. The model checking run prints an invalid execution result first, the small table of the two threads and their operations, followed by the interleaving that leads to the error, with the internal calls visible, down to the compareAndSet on the node item and the unlink of the node.

The declaration approach is what makes the framework usable on a structure you did not write. You are not modelling the implementation, you are describing the interface, and the framework searches for a way to break the contract.

Adding the dependency and writing the first test

The artifact is published to Maven Central under the org.jetbrains.lincheck group ID, and for a Gradle project the dependency goes into the test configuration.

repositories {
   mavenCentral()
}

dependencies {
   // Lincheck dependency
   testImplementation("org.jetbrains.lincheck:lincheck:3.7")
}

The first test is short. You wrap the concurrent logic in the runConcurrentTest function, and the test is an ordinary JUnit test, so it runs in your existing test task with no separate runner to configure.

@Test // JUnit test
fun test() = Lincheck.runConcurrentTest {
    var counter = 0
    // Increment the counter concurrently
    val t1 = thread { counter++ }
    val t2 = thread { counter++ }
    // Wait for the threads to finish
    t1.join()
    t2.join()
    // Check both increments have been applied
    assertEquals(2, counter)
}

The version in the snippet is 3.7, which matches the latest release in the repository. The counter example is deliberately broken, and the README says the test finishes with an error, with Lincheck providing a step-by-step execution trace to reproduce it.

What the trace looks like when the counter test fails

The failure output is a table with one column per thread, and the rows are the steps. The counter test prints the assertion failure first, expected 2 but was 1, and then the interleaving that produced it.

| ------------------------------------------------------------------------------- |
|                   Main Thread                   |   Thread 1    |   Thread 2    |
| ------------------------------------------------------------------------------- |
| thread(block = Lambda#1): Thread#1              |               |               |
| thread(block = Lambda#2): Thread#2              |               |               |
| switch (reason: waiting for Thread 1 to finish) |               |               |
|                                                 |               | run()         |
|                                                 |               |   counter ➜ 0 |
|                                                 |               |   switch      |
|                                                 | run()         |               |
|                                                 |   counter ➜ 0 |               |
|                                                 |   counter = 1 |               |
|                                                 |               |   counter = 1 |
| Thread#1.join()                                 |               |               |
| Thread#2.join()                                 |               |               |

Reading it, the cause is visible without running anything: both threads read the counter as 0 before either writes 1, so one increment is lost. The switch reason is printed too, which is the kind of detail that makes a report reproducible rather than merely descriptive.

The model checking failure in the data structure example has a different shape. It shows the invalid execution results first, the operations that were performed, and then a second table with the internal calls of the implementation, where the losing update is visible as the compareAndSet that succeeds on a node another thread has already unlinked.

This is the artefact that changes how a team works. A report that names the exact operations and the exact interleaving can be turned into a regression test by hand, and the README points to the official tutorial on the Kotlin site for the full feature tour, plus a paper on Lincheck as a practical framework for testing concurrent data structures on the JVM.

Version 3.0 moved the package and the group ID, and the API with them

The upgrade note at the top of the README is a list of three changes, and all three affect the import lines in your test sources. The API has been moved from org.jetbrains.kotlinx.lincheck to org.jetbrains.lincheck, the artifact is now published to Maven Central under the org.jetbrains.lincheck group ID, and the framework now focuses on testing arbitrary concurrent code while still providing a declarative API for testing concurrent data structures.

The package move is the one that breaks a build. A project that upgrades the dependency coordinate but leaves the imports pointing at the old package will not compile, and the fix is mechanical, but there is no way to leave the old package in place and have both work, because the two are not aliases for each other.

The scope change is the one that changes how the tool is used. A framework that only handled data structures forced you to restructure a test as a list of operations. With arbitrary concurrent code in scope, the same instrumentation applies to a block of logic that mutates shared state, which is what the counter example shows: a plain block of code with two threads, a join, and an assertion, and nothing else to declare.

The debug story is the part that the IDE integration supports. The README describes a reproducible execution trace and the ability to debug it step by step in IntelliJ IDEA, which is the difference between reading a report and replaying it. The repository layout backs that up, with separate directories for the tracer, the trace representation, the trace recorder, the live debugger and a JVM agent, so the trace is a first class output of the tool rather than a formatted string.

MPL-2.0, a steady 3.x line, and a repository built like a toolchain

The licence is MPL-2.0, the file level copyleft licence, and the repository ships a LICENSE.txt. For a test dependency that is a comfortable position: a library distributed in this way can be used in a proprietary project without the whole product falling under the licence, which is a different situation from a test framework under GPL.

The release cadence is regular. Version 3.7 was published on 2026-07-29, 3.6 on 2026-05-26 and 3.5 on 2026-03-30, and the repository is not archived with the last push on 2026-10-13. A dependency that ships a minor version every couple of months is normal for an actively used tool, and the versioning also means the API surface moves: the 3.0 change above shows that a major bump can relocate packages, so an upgrade is worth reading rather than bumping blindly.

The repository structure describes how the tool is put together. There is the lincheck module, a common module, a tracer module, a trace module, a trace recorder, a live debugger, a jvm-agent module, and a bootstrap directory, which is the pattern of a tool that has to start up inside the target JVM before the test code runs. There is also an examples directory with its own Gradle build, an integration-test directory, and a lincheck-test-project directory, plus buildSrc and settings files, so the project is a multi module Gradle build rather than a single library.

The upgrade cost for an adopting team is therefore mostly in the test sources: an import change at version 3.0, and a minor version cadence that means the dependency coordinate moves often enough to be worth pinning deliberately.

Editorial conclusion

Lincheck fits a team that has a concurrent data structure or a lock-based component and is tired of flaky tests, because its value is the failure report rather than the detection: the interleaving trace turns a nondeterministic failure into something you can read and step through in the IDE. It does not fit a codebase with no shared mutable state, and it does not fit an environment that cannot run a JVM agent, since the framework ships its own agent and tracer components. Verify two things before you adopt it: that the correctness property you need is the default one, linearizability, or whether you must state a different property, and that the 3.0 package move, from org.jetbrains.kotlinx.lincheck to org.jetbrains.lincheck, has been applied in your test sources, since the older coordinates no longer match the published artifact.

Frequently asked questions

Official sources

1. Issues
2. JetBrains/lincheck on GitHub
3. License: MPL-2.0
4. README
5. Releases