Getting started with Lincheck

Create a project

Open an existing Kotlin project in IntelliJ IDEA or create a new one.

Add dependencies

To use Lincheck in the project, add the corresponding dependencies to your build configuration:

Write your first test

For a basic concurrent test, create a test function that describes what operations should be executed in each thread and the expected assertions. Lincheck explores possible thread interleavings of the program using model checking and provides an error report in case of incorrect behavior.

1. In the src/test directory, create a CounterTest.kt file.

2. Import the org.jetbrains.lincheck, kotlinx.concurrent, and kotlin.test libraries:

   import org.jetbrains.lincheck.* import kotlin.concurrent.* import kotlin.test.*

3. Write a test that creates a variable and two threads manipulating that variable:

   class CounterTest { @Test // Test function declaration fun test() = Lincheck.runConcurrentTest { var counter = 0 // Increments the counter concurrently val t1 = thread { counter++ } val t2 = thread { counter++ } // Waits for the threads to finish t1.join() t2.join() // Checks that both increments have been applied assertEquals(2, counter) } }

4. Run the test. Lincheck generates a report with a thread interleaving that led to incorrect behavior:

   | ------------------------------------------------------------------------------- | | Main Thread | Thread 1 | Thread 2 | | ------------------------------------------------------------------------------- | | thread(block = Lambda#2): Thread#1 | | | | thread(block = Lambda#3): 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() | | | | counter.element ➜ 1 | | | | assertEquals(2, 1): threw AssertionFailedError | | | | ------------------------------------------------------------------------------- |

   Lincheck found a thread interleaving where one of the inc() operations overwrites the counter value.

   Step-by-step report explanation

   1. In Thread 2, the JVM reads the initial counter value.

   2. The execution switches from Thread 2 to Thread 1.

   3. In Thread 1, the JVM increments the counter. All steps of the inc() operation are performed without interruptions: reading the value from the variable, incrementing the value, and writing the value back to the variable.

   4. The execution switches back to Thread 2.

   5. In Thread 2, the JVM increments the value acquired at step 1 and writes the result to the counter variable.

Write a test for a data structure

In addition to basic concurrent tests, Lincheck supports a declarative approach to testing concurrent data structures.

To test a data structure in Lincheck, you only need to declare the concurrent methods of the structure and a test function. Lincheck generates random concurrent scenarios, executes them using the specified testing strategy, and provides error reports.

In this section, you will test a simple counter:

1. In the src/test directory, create a CounterStructureTest.kt file.

2. Import the lincheck.datastructures and kotlin.test libraries:

   import org.jetbrains.lincheck.datastructures.* import kotlin.test.*

3. Create a Counter structure:

   class Counter { @Volatile private var value = 0 fun inc(): Int = ++value fun get() = value }

4. Create a CounterStructureTest class. Set the initial state of the structure and mark the concurrent operations of the structure with the @Operation annotation:

   class CounterStructureTest { // Initial state private val c = Counter() // Concurrent operations @Operation fun inc() = c.inc() @Operation fun get() = c.get() }

5. In the CounterTest class, declare a test function using ModelCheckingOptions():

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

6. Run the test. Lincheck generates an error report with the concurrent scenario and the specific thread interleaving that led to incorrect behavior:

   | ------------------- | | Thread 1 | Thread 2 | | ------------------- | | inc(): 1 | inc(): 1 | | ------------------- |
   | ------------------------ | | Thread 1 | Thread 2 | | ------------------------ | | | inc(): 1 | | | c.inc(): 1 | | | value ➜ 0 | | | switch | | inc(): 1 | | | | value = 1 | | | value ➜ 1 | | | result: 1 | | ------------------------ |

What's next

Read more about the declarative approach to testing data structures and supported testing strategies in the Testing strategies article.