Data structure constraints

Some data structures may require a part of operations not to be executed concurrently, such as single-producer single-consumer queues. Lincheck provides out-of-the-box support for such contracts, generating concurrent scenarios according to the restrictions.

Consider the single-consumer queue from the JCTools library. Let's write a test to check correctness of its poll(), peek(), and offer(x) operations.

In your build.gradle(.kts) file, add the JCTools dependency:

dependencies {
    // jctools dependency
    testImplementation("org.jctools:jctools-core:3.3.0")
}

dependencies {
    // jctools dependency
    testImplementation "org.jctools:jctools-core:3.3.0"
}

To meet the single-consumer restriction, ensure that all poll() and peek() consuming operations are called from a single thread. For that, we can set the nonParallelGroup parameter of the corresponding @Operation annotations to the same value, e.g. "consumers".

Here is the resulting test:

import org.jctools.queues.atomic.*
import org.jetbrains.kotlinx.lincheck.annotations.*
import org.jetbrains.kotlinx.lincheck.check
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
import org.jetbrains.kotlinx.lincheck.strategy.stress.*
import org.junit.*

class MPSCQueueTest {
    private val queue = MpscLinkedAtomicQueue<Int>()

    @Operation
    fun offer(x: Int) = queue.offer(x)

    @Operation(nonParallelGroup = "consumers") 
    fun poll(): Int? = queue.poll()

    @Operation(nonParallelGroup = "consumers")
    fun peek(): Int? = queue.peek()

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

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

Here is an example of the scenario generated for this test:

= Iteration 15 / 100 =
| --------------------- |
| Thread 1  | Thread 2  |
| --------------------- |
| poll()    |           |
| poll()    |           |
| peek()    |           |
| peek()    |           |
| peek()    |           |
| --------------------- |
| offer(-1) | offer(0)  |
| offer(0)  | offer(-1) |
| peek()    | offer(-1) |
| offer(1)  | offer(1)  |
| peek()    | offer(1)  |
| --------------------- |
| peek()    |           |
| offer(-2) |           |
| offer(-2) |           |
| offer(2)  |           |
| offer(-2) |           |
| --------------------- |

Note that all consuming poll() and peek() invocations are performed from a single thread, thus satisfying the "single-consumer" restriction.

Next step

Learn how to check your algorithm for progress guarantees with the model checking strategy.

Last modified: 08 May 2024