Configuring a testing strategy

Lincheck supports various configuration options for testing strategies, including scenario generation, detection of stalled execution, verification, and others.

How to enable options

To enable an option for a testing strategy, set it in the strategy class:

@Test
fun modelCheckingTest() = ModelCheckingOptions()
    .iterations(100) // Specify the number of generated scenarios
    .check(this::class)

Scenario minimization

By default, Lincheck tries to minimize the failed scenario by removing the operations that do not change the behavior of the test.

Set the minimizeFailedScenario option to false to see the full failed scenario.

| ------------------------- |
|    Thread 1    | Thread 2 |
| --------------------------|
| inc(): 1       |          |
| get(): 1       |          |
| get(): 1       |          |
| --------------------------|
| inc(): 4 [0,1] | inc(): 2 |
| get(): 4 [1,1] | inc(): 4 |
| get(): 4 [2,1] | get(): 4 |
| --------------------------|
| get(): 4       |          |
| get(): 4       |          |
| get(): 4       |          |
| --------------------------|

| ------------------- |
| Thread 1 | Thread 2 |
| ------------------- |
| inc(): 1 | inc(): 1 |
| ------------------- |

Scenario generation

Option	Default value	Description
`iterations`	`100`	The number of generated concurrent scenarios.
`invocationsPerIteration`	`10_000`	The number of invocations for each concurrent scenario.
`threads`	`2`	The number of threads in each scenario.
`actorsBefore`	`5`	The number of operations called before the parallel section of a scenario.
`actorsPerThread`	`5`	The number of operations in each thread in the parallel section of a scenario.
`actorsAfter`	`5`	The number of operations called after the parallel section of a scenario.
`customScenarios`	–	A list of custom concurrent scenarios. The custom scenarios are executed before the randomly generated ones.

Defining a custom scenario

Lincheck uses a domain-specific language for defining custom scenarios:

@Test
fun test() = StressOptions()
    .customScenarios {
        initial {
            actor(SomeClass1::foo)
        }
        parallel {
            thread {
                actor(SomeClass1::buzz, 1)
                actor(SomeClass1::buzz, 2)
            }
            thread {
                actor(SomeClass1::buzz, 3)
            }
        }
        post {
            actor(SomeClass1::foo)
        }
    }
    .check(this::class)

Each scenario consists of three optional sections:

initial – operations executed before the parallel part.
parallel – thread definitions. Threads are defined using the thread block. The parallel section might contain multiple thread blocks.
post – operations executed after the parallel part.

Operations are defined using the actor(function, arg1, arg2, ...) function. Operations within a single block are executed sequentially.

Stalled execution detection

Option	Default value	Description
`timeoutMs`	`3000`	Invocation timeout in milliseconds after which Lincheck reports a stalled execution.
`loopBound`	`50`	The number of loop iterations after which Lincheck reports a stalled execution. Increase the value of `loopBound` if Lincheck falsely reports stalled execution for long loops. This option can only be applied to model checking.
`recursionBound`	`20`	The number of recursive calls after which Lincheck reports a stalled execution. The value of `loopIterationsBeforeThreadSwitch` should be less than `loopBound`. This option can only be applied to model checking.

Thread switching in loops

Option	Default value	Description
`loopIterationsBeforeThreadSwitch`	`10`	The number of loop iterations a thread can perform before trying to switch to another thread. The value of `loopIterationsBeforeThreadSwitch` should be less than `loopBound`. This option can only be applied to model checking.

Verification

Option	Default value	Description
`verifierClass`	`LinearizabilityVerifier`	The verifier class used during the verification process: `LinearizabilityVerifier` `SerializabilityVerifier` `QuiescentConsistencyVerifier`
`sequentialSpecification`	Same as the tested data structure.	The sequential version of the tested data structure. This structure is used during the verification process.

Option

Default value

Description

verifierClass

LinearizabilityVerifier

The verifier class used during the verification process:

LinearizabilityVerifier
SerializabilityVerifier
QuiescentConsistencyVerifier

sequentialSpecification

Same as the tested data structure.

The sequential version of the tested data structure. This structure is used during the verification process.

Progress guarantees

Option	Default value	Description
`checkObstructionFreedom`	`false`	Set this option to `true` to verify the obstruction-freedom guarantee of the data structure operations. This option can only be applied to model checking.

Library analysis

Option	Default value	Description
`stdLibAnalysisEnabled`	`false`	By default, Lincheck does not verify the behavior of the operations from the standard library, treating them as thread-safe. Set this option to `true` to enable analysis of standard library functions/classes. This option can only be applied to model checking.
`addGuarantee`	–	Define guarantees for thread-safe or irrelevant to analysis methods using the `addGuarantee` option to exclude them from model checking. This option can only be applied to model checking.

Defining a guarantee

To define a guarantee, use a builder chain: select classes, then methods, then the guarantee type.

@Test
fun modelCheckingTest() = ModelCheckingOptions()
        .addGuarantee(
            forClasses("java.util.concurrent.ConcurrentHashMap")
                .allMethods()
                .treatAsAtomic()
        )
        .check(this::class)

Select classes using one of the forClasses overloads:
- forClasses(vararg fullClassNames: String) — matches classes if their full name is present in the fullClassNames string.
- forClasses(vararg classes: KClass<*>) — matches classes by reference.
- forClasses(classPredicate: (fullClassName: String) -> Boolean) — match classes using a predicate on full class names.
Select methods to apply the guarantee to:
- methods(methodNames: String) – matches methods if their name is present in the methodNames string.
- methods(methodPredicate: (methodName: String) -> Boolean) – matches methods using a predicate.
- allMethods() – match all methods of the selected classes.
Choose the guarantee type:
- treatAsAtomic() — treat each method as an atomic operation. Lincheck will not insert switch points inside the method call, but might add them before or after the call.
  Use treatAsAtomic() for methods that are known to be thread-safe.
- ignore() — exclude the methods from analysis. Lincheck will not insert switch points inside, before, or after the method calls.
  If a method uses synchronization primitives internally (for instance, synchronized blocks), ignoring the method may cause Lincheck to deadlock.
  Use ignore() for methods that are irrelevant to analysis, such as logging or debugging utilities.

What’s next

Learn how to configure argument generation for operations used in Lincheck's execution scenarios.

Kotlin Help