用 Lincheck 编写第一个测试

This tutorial demonstrates how to write your first Lincheck test, set up the Lincheck framework, and use its basic API. You will create a new IntelliJ IDEA project with an incorrect concurrent counter implementation and write a test for it, finding and analyzing the bug afterward.

Create a project

Open an existing Kotlin project in IntelliJ IDEA or create a new one. When creating a project, use the Gradle build system.

Add required dependencies

  1. Open the build.gradle(.kts) file and make sure that mavenCentral() is added to the repository list.
  2. Add the following dependencies to the Gradle configuration:

【Kotlin】

  1. repositories {
  2. mavenCentral()
  3. }
  4. dependencies {
  5. // Lincheck dependency
  6. testImplementation("org.jetbrains.kotlinx:lincheck:2.23")
  7. // This dependency allows you to work with kotlin.test and JUnit:
  8. testImplementation("junit:junit:4.13")
  9. }

【Groovy】

  1. repositories {
  2. mavenCentral()
  3. }
  4. dependencies {
  5. // Lincheck dependency
  6. testImplementation "org.jetbrains.kotlinx:lincheck:2.23"
  7. // This dependency allows you to work with kotlin.test and JUnit:
  8. testImplementation "junit:junit:4.13"
  9. }

Write a concurrent counter and run the test

  1. In the src/test/kotlin directory, create a BasicCounterTest.kt file and add the following code with a buggy concurrent counter and a Lincheck test for it:

    1. import org.jetbrains.kotlinx.lincheck.annotations.*
    2. import org.jetbrains.kotlinx.lincheck.*
    3. import org.jetbrains.kotlinx.lincheck.strategy.stress.*
    4. import org.junit.*
    5. class Counter {
    6. @Volatile
    7. private var value = 0
    8. fun inc(): Int = ++value
    9. fun get() = value
    10. }
    11. class BasicCounterTest {
    12. private val c = Counter() // Initial state
    13. // Operations on the Counter
    14. @Operation
    15. fun inc() = c.inc()
    16. @Operation
    17. fun get() = c.get()
    18. @Test // JUnit
    19. fun stressTest() = StressOptions().check(this::class) // The magic button
    20. }

    This Lincheck test automatically:

    • Generates several random concurrent scenarios with the specified inc() and get() operations.
    • Performs a lot of invocations for each of the generated scenarios.
    • Verifies that each invocation result is correct.
  2. Run the test above, and you will see the following error:

    1. = Invalid execution results =
    2. | ------------------- |
    3. | Thread 1 | Thread 2 |
    4. | ------------------- |
    5. | inc(): 1 | inc(): 1 |
    6. | ------------------- |

    Here, Lincheck found an execution that violates the counter atomicity – two concurrent increments ended with the same result 1. It means that one increment has been lost, and the behavior of the counter is incorrect.

Trace the invalid execution

Besides showing invalid execution results, Lincheck can also provide an interleaving that leads to the error. This feature is accessible with the model checking testing strategy, which examines numerous executions with a bounded number of context switches.

  1. To switch the testing strategy, replace the options type from StressOptions() to ModelCheckingOptions(). The updated BasicCounterTest class will look like this:

    1. import org.jetbrains.kotlinx.lincheck.annotations.*
    2. import org.jetbrains.kotlinx.lincheck.check
    3. import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
    4. import org.junit.*
    5. class Counter {
    6. @Volatile
    7. private var value = 0
    8. fun inc(): Int = ++value
    9. fun get() = value
    10. }
    11. class BasicCounterTest {
    12. private val c = Counter()
    13. @Operation
    14. fun inc() = c.inc()
    15. @Operation
    16. fun get() = c.get()
    17. @Test
    18. fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
    19. }
  2. Run the test again. You will get the execution trace that leads to incorrect results:

    1. = Invalid execution results =
    2. | ------------------- |
    3. | Thread 1 | Thread 2 |
    4. | ------------------- |
    5. | inc(): 1 | inc(): 1 |
    6. | ------------------- |
    7. The following interleaving leads to the error:
    8. | --------------------------------------------------------------------- |
    9. | Thread 1 | Thread 2 |
    10. | --------------------------------------------------------------------- |
    11. | | inc() |
    12. | | inc(): 1 at BasicCounterTest.inc(BasicCounterTest.kt:18) |
    13. | | value.READ: 0 at Counter.inc(BasicCounterTest.kt:10) |
    14. | | switch |
    15. | inc(): 1 | |
    16. | | value.WRITE(1) at Counter.inc(BasicCounterTest.kt:10) |
    17. | | value.READ: 1 at Counter.inc(BasicCounterTest.kt:10) |
    18. | | result: 1 |
    19. | --------------------------------------------------------------------- |

    According to the trace, the following events have occurred:

    • T2: The second thread starts the inc() operation, reading the current counter value (value.READ: 0) and pausing.
    • T1: The first thread executes inc(), which returns 1, and finishes.
    • T2: The second thread resumes and increments the previously obtained counter value, incorrectly updating the counter to 1.

Get the full code.

用 Lincheck 编写第一个测试 - 图1

Test the Java standard library

Let’s now find a bug in the standard Java’s ConcurrentLinkedDeque class. The Lincheck test below finds a race between removing and adding an element to the head of the deque:

  1. import org.jetbrains.kotlinx.lincheck.*
  2. import org.jetbrains.kotlinx.lincheck.annotations.*
  3. import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
  4. import org.junit.*
  5. import java.util.concurrent.*
  6. class ConcurrentDequeTest {
  7. private val deque = ConcurrentLinkedDeque<Int>()
  8. @Operation
  9. fun addFirst(e: Int) = deque.addFirst(e)
  10. @Operation
  11. fun addLast(e: Int) = deque.addLast(e)
  12. @Operation
  13. fun pollFirst() = deque.pollFirst()
  14. @Operation
  15. fun pollLast() = deque.pollLast()
  16. @Operation
  17. fun peekFirst() = deque.peekFirst()
  18. @Operation
  19. fun peekLast() = deque.peekLast()
  20. @Test
  21. fun modelCheckingTest() = ModelCheckingOptions().check(this::class)
  22. }

Run modelCheckingTest(). The test will fail with the following output:

  1. = Invalid execution results =
  2. | ---------------------------------------- |
  3. | Thread 1 | Thread 2 |
  4. | ---------------------------------------- |
  5. | addLast(22): void | |
  6. | ---------------------------------------- |
  7. | pollFirst(): 22 | addFirst(8): void |
  8. | | peekLast(): 22 [-,1] |
  9. | ---------------------------------------- |
  10. ---
  11. All operations above the horizontal line | ----- | happen before those below the line
  12. ---
  13. Values in "[..]" brackets indicate the number of completed operations
  14. in each of the parallel threads seen at the beginning of the current operation
  15. ---
  16. The following interleaving leads to the error:
  17. | --------------------------------------------------------------------------------------------------------------------------------- |
  18. | Thread 1 | Thread 2 |
  19. | --------------------------------------------------------------------------------------------------------------------------------- |
  20. | pollFirst() | |
  21. | pollFirst(): 22 at ConcurrentDequeTest.pollFirst(ConcurrentDequeTest.kt:17) | |
  22. | first(): Node@1 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:915) | |
  23. | item.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917) | |
  24. | next.READ: Node@2 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:925) | |
  25. | item.READ: 22 at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:917) | |
  26. | prev.READ: null at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:919) | |
  27. | switch | |
  28. | | addFirst(8): void |
  29. | | peekLast(): 22 |
  30. | compareAndSet(Node@2,22,null): true at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:920) | |
  31. | unlink(Node@2) at ConcurrentLinkedDeque.pollFirst(ConcurrentLinkedDeque.java:921) | |
  32. | result: 22 | |
  33. | --------------------------------------------------------------------------------------------------------------------------------- |

Get the full code.

用 Lincheck 编写第一个测试 - 图2

Next step

Choose your testing strategy and configure test execution.

See also