数据结构约束

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:

【Kotlin】

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

【Groovy】

1. dependencies {
2. // jctools dependency
3. testImplementation "org.jctools:jctools-core:3.3.0"
4. }

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:

1. import org.jctools.queues.atomic.*
2. import org.jetbrains.kotlinx.lincheck.annotations.*
3. import org.jetbrains.kotlinx.lincheck.check
4. import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.*
5. import org.jetbrains.kotlinx.lincheck.strategy.stress.*
6. import org.junit.*

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

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

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

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

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

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

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

1. = Iteration 15 / 100 =
2. | --------------------- |
3. | Thread 1  | Thread 2  |
4. | --------------------- |
5. | poll()    |           |
6. | poll()    |           |
7. | peek()    |           |
8. | peek()    |           |
9. | peek()    |           |
10. | --------------------- |
11. | offer(-1) | offer(0)  |
12. | offer(0)  | offer(-1) |
13. | peek()    | offer(-1) |
14. | offer(1)  | offer(1)  |
15. | peek()    | offer(1)  |
16. | --------------------- |
17. | peek()    |           |
18. | offer(-2) |           |
19. | offer(-2) |           |
20. | offer(2)  |           |
21. | offer(-2) |           |
22. | --------------------- |

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.