Lincheck

Lincheck is a practical and user-friendly framework for testing concurrent algorithms on the JVM. It provides a simple and declarative way to write concurrent tests.

With the Lincheck framework, instead of describing how to perform tests, you can specify what to test by just declaring all the data structure operations to examine. After that, Lincheck automatically generates a set of random concurrent scenarios, examines them using either stress-testing or bounded model checking, and verifies that the results of each invocation satisfy the required correctness property (linearizability by default).

Documentation and Presentations

Please see the official tutorial that showcases Lincheck features through examples.

You may also be interested in the following public talks:

• "How we test concurrent algorithms in Kotlin Coroutines" by Nikita Koval: Video. KotlinConf 2023
• "Lincheck: Testing concurrency on the JVM" workshop by Maria Sokolova: Part 1, Part 2. Hydra 2021

Using in Your Project

To use Lincheck in your project, you need to add it as a dependency. If you use Gradle, add the following lines to build.gradle.kts:

repositories {
   mavenCentral()
}

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

Java 9+

To use model checking strategy for Java 9 and later, add the following JVM properties:

--add-opens java.base/jdk.internal.misc=ALL-UNNAMED
--add-exports java.base/jdk.internal.util=ALL-UNNAMED
--add-exports java.base/sun.security.action=ALL-UNNAMED

They are required if the testing code uses classes from the java.util package since some of them use jdk.internal.misc.Unsafe or similar internal classes under the hood.

If you use Gradle, add the following lines to build.gradle.kts:

tasks.withType<Test> {
    jvmArgs(
        "--add-opens", "java.base/jdk.internal.misc=ALL-UNNAMED", 
        "--add-exports", "java.base/jdk.internal.util=ALL-UNNAMED", 
        "--add-exports", "java.base/sun.security.action=ALL-UNNAMED"
    )
}

Example

The following Lincheck test easily finds a bug in the standard Java's ConcurrentLinkedDeque:

import org.jetbrains.kotlinx.lincheck.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.junit.*
import java.util.concurrent.*

class ConcurrentDequeTest {
    private val deque = ConcurrentLinkedDeque<Int>()

    @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()

    // 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)
}

When running modelCheckingTest(), Lincheck not only detects a bug but also provides a comprehensive interleaving trace that explains it:

= Invalid execution results =
| -------------------------------------- |
|     Thread 1     |      Thread 2       |
| -------------------------------------- |
| addLast(4): void |                     |
| -------------------------------------- |
| pollFirst(): 4   | addFirst(-4): void  |
|                  | peekLast(): 4 [-,1] |
| -------------------------------------- |

---
All operations above the horizontal line | ----- | happen before those below the line
---
Values in "[..]" brackets indicate the number of completed operations
in each of the parallel threads seen at the beginning of the current operation
---

The following interleaving leads to the error:
| addLast(4): void                                                                                          |                      |
| pollFirst()                                                                                               |                      |
|   pollFirst(): 4 at ConcurrentLinkedDequeTest.pollFirst(ConcurrentLinkedDequeTest.kt:29)                  |                      |
|     first(): Node@1 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:915)                    |                      |
|     item.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917)                    |                      |
|     next.READ: Node@2 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:925)                  |                      |
|     item.READ: 4 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917)                       |                      |
|     prev.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:919)                    |                      |
|     switch                                                                                                |                      |
|                                                                                                           | addFirst(-4): void   |
|                                                                                                           | peekLast(): 4        |
|     compareAndSet(Node@2,4,null): true at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:920) |                      |
|     unlink(Node@2) at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:921)                     |                      |
|   result: 4                                                                                               |                      |

Contributing

See Contributing Guidelines.

Acknowledgements

This is a fork of the Lin-Check framework by Devexperts.