Kotlin Help

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: 15 April 2024