数据结构约束

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.

To meet the single-consumer restriction, ensure that all poll() and peek() consuming operations are called from a single thread. For that, declare a group of operations for non-parallel execution:

  1. Declare @OpGroupConfig annotation to create a group of operations for non-parallel execution, name the group, and set nonParallel parameter to true.
  2. Specify the group name in the @Operation annotation to add all non-parallel operations to this group.

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.stress.*
import org.junit.*

// Declare a group of operations that should not be executed in parallel:
@OpGroupConfig(name = "consumer", nonParallel = true)
class MPSCQueueTest {
    private val queue = MpscLinkedAtomicQueue<Int>()

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

    @Operation(group = "consumer") 
    fun poll(): Int? = queue.poll()

    @Operation(group = "consumer")
    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 =
Execution scenario (init part):
[offer(1), offer(4), peek(), peek(), offer(-6)]
Execution scenario (parallel part):
| poll()   | offer(6)  |
| poll()   | offer(-1) |
| peek()   | offer(-8) |
| offer(7) | offer(-5) |
| peek()   | offer(3)  |
Execution scenario (post part):
[poll(), offer(-6), peek(), peek(), peek()]

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

Get the full code.

Next step

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