数据结构约束
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, 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.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 =
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.
Next step
Learn how to check your algorithm for progress guarantees with the model checking strategy.