Results verification and validation

After executing the scenarios generated for a concurrent data structure, Lincheck verifies the results against the specified verification model (for example, linearizability) and optionally checks the final state of the data structure against the user-provided validation function.

Verification

During the verification process, Lincheck tries to find a sequential execution of the operations in the concurrent scenario that achieves the same results as the concurrent execution:

Depending on the verification model, there might be additional restrictions on sequential execution. If no sequential execution matching the verification property can produce the observed results, Lincheck reports an error.

Sequential specification

By default, during the verification process, Lincheck constructs a sequential execution using the operations of the concurrent data structure.

You can specify a sequential data structure with matching operations to:

Make sure that the concurrent data structure provides the same results as the sequential one.
Typically, single-threaded implementations are simpler than thread-safe implementations, and therefore can be much more easily verified for correctness (for example, HashMap and ConcurrentHashMap, LinkedList and ConcurrentLinkedQueue).
By comparing the execution results of two versions of a structure, you can make sure that the more complex concurrent structure behaves similarly to a simpler structure in a single-threaded environment.
Verify both sequential correctness and concurrency safety in a single test.

A diagram of the verification process in Lincheck. Lincheck compares a concurrent execution to
different sequential executions. Sequential executions use the operations of the specified
sequential version of the structure.

To specify a sequential version of a data structure:

Implement a data structure with sequential versions of all concurrent functions tested by Lincheck.
Specify the data structure using the sequentialSpecification() option:
@Test fun stressTest() = StressOptions() .sequentialSpecification(SequentialStructure::class) .check(this::class)

An example of a Lincheck test that uses a single-threaded LinkedList as the sequential specification of ConcurrentLinkedQueue:

class ConcurrentLinkedQueueTest {
    private val s = ConcurrentLinkedQueue<Int>()

    @Operation
    fun add(value: Int) = s.add(value)

    @Operation
    fun poll(): Int? = s.poll()

    @Test
    fun stressTest() = StressOptions()
        .sequentialSpecification(SequentialQueue::class.java)
        .check(this::class)
}

class SequentialQueue {
    private val s = LinkedList<Int>()

    fun add(x: Int) = s.add(x)
    fun poll(): Int? = s.poll()
}

Verification models

By default, Lincheck verifies the results of the concurrent execution against the linearizability model. To apply a different verification model, use the verifierClass option:

@Test
fun modelCheckingTest() = ModelCheckingOptions()
   .verifierClass(SerializabilityVerifier::class)
   .check(this::class)

Lincheck provides the following verifier classes:

LinearizabilityVerifier – the default option. Concurrent execution is valid if there is a sequential execution that preserves the "happens-before" relations among the operations in the concurrent execution.
QuiescentConsistencyVerifier – uses the quiescent consistency model which works similarly to the linearizability model, but the "happens-before" constraints are not applied to the operations annotated with @QuiescentConsistent:
@Operation @QuiescentConsistent fun someOperation() = { ... }
QuiescentConsistencyVerifier does not track actual quiescent points. The verifier can potentially miss bugs that occur across the boundaries of quiescent points.
SerializabilityVerifier – uses the serializability model where the concurrent execution is valid if there is some sequential execution (in any order) that leads to the same results as the concurrent execution, regardless of the "happens-before" constraints. It can be used for structures where the relative order of concurrent operations does not matter.

Compare serializability and linearizability

To understand the difference between the two models, see how a data structure can be serializable but not linearizable:

Consider the following data structure:
class ConcurrentQueue { private val elements: MutableList<Int> = ArrayList() fun put(x: Int) = synchronized(this) { elements += x } fun poll(): Int? = synchronized(this) { if (elements.isEmpty()) return null elements.shuffle() elements.removeAt(0) } }
This concurrent structure behaves incorrectly: it stores elements like in a typical queue, but returns them randomly.
Implement a sequential version of the queue that correctly stores and returns the elements:
class SequentialQueue { private val elements: MutableList<Int> = ArrayList() fun put(x: Int) { elements += x } fun poll(): Int? = if (elements.isEmpty()) null else elements.removeAt(0) }
Create a test class and declare the put() and poll() operations:
@Param(name = "value", gen = IntGen::class, conf = "1:2") class ConcurrentQueueTest { private val q = ConcurrentQueue() @Operation fun put(@Param(name = "value") x: Int) = q.put(x) @Operation fun poll(): Int? = q.poll() }
Declare and run a serializability test:
@Test fun serializabilityTest() = ModelCheckingOptions() .actorsBefore(0) .actorsAfter(0) .actorsPerThread(2) .threads(2) // Verify against serializability .verifier(SerializabilityVerifier::class.java) // Specify the sequential version of the structure .sequentialSpecification(SequentialQueue::class.java) .check(this::class.java)
It should pass successfully.
Declare and run a linearizability test:
@Test fun linearizabilityTest() = ModelCheckingOptions() .actorsBefore(0) .actorsAfter(0) .actorsPerThread(2) .threads(2) // Show the full failed scenario .minimizeFailedScenario(false) // Specify the sequential version of the structure .sequentialSpecification(SequentialQueue::class.java) .check(this::class.java)
The test should fail with the following report:
| -------------------- | | Thread 1 | Thread 2 | | -------------------- | | | put(2) | | | put(1) | | put(3) | | | poll(): 1 | | | -------------------- |
Analyze the results.
Because the serializability test passes, there exists some sequential order of SequentialQueue operations that produces poll(): 1, for example:
However, linearizability further restricts the operation order: if operation A finishes before operation B begins in the concurrent execution, then A must be executed before B in the sequential execution. An example of a linearizable execution would look like this:
Because Lincheck cannot reorder the put() operations during verification, it cannot find a sequential execution that complies with linearizability restrictions. This results in a failed test.

Validation

By default, Lincheck does not validate the state of the concurrent data structure after executing a generated scenario. To check the final state, use the @Validate annotation on your validation function in the test class:

@Validate
fun validate() {
    // Check some property of the data structure
    // Throw an exception if the invariant is violated
    check(size >= 0) { "Size must be non-negative, but was $size" }
}

The validation function should:

Accept no arguments.
Throw an exception if the data structure is in an invalid state.

What's next

24 July 2026