Testing strategies

Lincheck provides two strategies for testing concurrent data structures: model checking and stress testing.

In this article, you will learn the difference between the strategies and what to keep in mind when choosing a testing strategy.

Model checking

With model checking, Lincheck simulates possible thread interleavings and reports those that cause incorrect behavior.

To use model checking for testing a data structure, declare a test function using ModelCheckingOptions():

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

When using the model checking strategy, Lincheck inserts explicit thread-switch instructions at points of shared-memory access (read and write) or at synchronization points, such as lock acquisition and release, park/unpark, wait/notify, and others.

Controlling the thread switching enables Lincheck to:

Deterministically explore different possible execution schedules of a program.
Provide detailed execution traces.

Currently, model checking requires Lincheck to assume a sequentially consistent memory model of the execution. This means that Lincheck does not simulate and cannot catch bugs related to instruction reordering, memory cache behavior, and other similar effects under the relaxed Java memory model.

Stress testing

With stress testing, Lincheck executes each scenario multiple times to increase the chances of finding an error.

To use stress testing, declare a test function using StressOptions():

@Test
fun stressTest() = StressOptions()
   .check(this::class)

Unlike with model checking, Lincheck does not control or track thread switches. This makes stress testing faster and does not require Lincheck to make any assumptions about the memory model. However, with stress testing, tests are not reproducible, and Lincheck cannot provide an execution trace.

Choose a strategy

When choosing a strategy, consider the following:

	Model checking	Stress testing
Speed	Slower.	Faster.
Reproducibility	The tests return exactly the same results if the input data has not changed.	The tests might return different results as the thread schedules might change from run to run.
Assumptions	Assumes a sequentially consistent memory model. Will miss bugs caused by incorrect behavior outside of that model.	Does not make any assumptions about a memory model. Has a chance to catch any incorrect behavior regardless of the underlying cause.
Verbosity	Reports both a concurrent scenario and an execution trace that led to incorrect behavior.	Reports only a concurrent scenario.
Standard library coverage	Does not simulate the behavior of some standard library features, such as weak references. Will miss bugs caused by such features.	Has a chance to catch a bug caused by the usage of any feature.

What’s next

Learn how to configure a testing strategy by customizing scenario generation, enabling stalled execution detection, and providing thread-safety guarantees for libraries.

Kotlin Help

Testing strategies

Model checking

Stress testing

Choose a strategy

What’s next

See also