数据结构约束
有些数据结构可能要求一部分操作不能并发执行, 例如单生成者(single-producer)/单消费者(single-consumer) 队列. Lincheck 对这样的约束提供了现成的支持, 会根据约束条件生成并发场景.
以 JCTools 库 中的 单消费者队列 为例. 我们来编写一个测试, 检查它的 poll()
, peek()
, 以及 offer(x)
操作的正确性.
在你的 build.gradle(.kts)
文件中, 添加 JCTools 依赖项:
dependencies {
// jctools 依赖项
testImplementation("org.jctools:jctools-core:3.3.0")
}
dependencies {
// jctools 依赖项
testImplementation "org.jctools:jctools-core:3.3.0"
}
为了满足单消费者约束条件, 需要确保所有的 poll()
和 peek()
消费操作都只会从单个线程中调用. 为了做到这一点, 我们可以将对应的 @Operation
注解的 nonParallelGroup
参数设置为相同的值, 例如, "consumers"
.
下面是测试代码:
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)
}
下面是为这个测试生成的并发场景的例子:
= 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) | |
| --------------------- |
注意, 所有的消费操作 poll()
和 peek()
的调用, 都通过单个线程执行, 因此满足了 "单消费者" 约束.
下一步
学次如何使用模型检查策略来 检查你的算法的进度保证.
最终更新: 2024/10/17