Lincheck声明式测试并发数据结构：@Operation注解从入门到实战的完整教程

Lincheck声明式测试并发数据结构：@Operation注解从入门到实战的完整教程

【免费下载链接】lincheckFramework for testing concurrent code on JVM languages项目地址: https://gitcode.com/gh_mirrors/li/lincheck

Lincheck 是 JetBrains 开源的 JVM 语言并发代码测试框架，让你用声明式方式编写并发测试：只需在方法上标注@Operation注解，Lincheck 就会自动生成并发执行场景、运行不同调度组合，并验证数据结构是否满足线性一致性。本教程面向新手，带你从第一个测试到参数定制、策略选择，完整掌握 @Operation 注解的用法。

一、为什么需要 Lincheck：告别“睡一会儿再断言”

测试并发代码的传统写法是：开几个线程、sleep一段时间、再检查最终状态。这种写法不仅不可靠，而且几乎永远抓不到真正的竞态条件。

Lincheck 换了一种思路——声明式测试🎯：

传统手写并发测试	Lincheck 声明式测试
你手动创建线程、控制时序	框架自动生成执行场景
只能覆盖你想到的一种时序	每个场景运行多种调度组合
断言靠运气	默认按线性一致性自动验证结果

框架入口在 lincheck/src/jvm/main/org/jetbrains/lincheck/Lincheck.kt，核心注解定义在 lincheck/src/jvm/main/org/jetbrains/lincheck/datastructures/Operation.kt。官方文档中的讲解见 docs/topics/lincheck-how-to-test-data-structures.md。

二、快速上手：4 步测试一个 Counter

以这个最简单的计数器为例：

class Counter { var value = 0 fun inc(): Int = ++value fun dec(): Int = --value }

只需 4 步就能为它写一个声明式并发测试：

1. 建测试类，声明一个被测试结构的属性作为初始状态：private val c = Counter()
2. 声明操作：把要测试的方法包一层，加上@Operation注解
3. 写测试函数：用ModelCheckingOptions().check(this::class)一行启动
4. 运行测试：失败时 Lincheck 会自动输出导致错误的具体场景和线程执行轨迹

完整示例可参考 examples/src/test/kotlin/org/lincheck/docs/CounterStructureTest.kt：

@Operation fun inc() = c.inc() @Operation fun dec() = c.dec() @Test fun test() = ModelCheckingOptions().check(this::class)

@Operation注解告诉 Lincheck：生成执行场景时，哪些方法可以被并发调用。

三、@Operation 注解参数速查表

@Operation并不只有"标记方法"这一个作用，它的 6 个参数覆盖了大多数并发测试需求（定义见 Operation.kt）：

参数	默认值	作用
params	[]	绑定自定义参数生成器（配合@Param使用）
runOnce	false	整个测试中该操作最多执行一次
nonParallelGroup	""	同组操作永远不会并发执行
cancellableOnSuspension	true	挂起时该操作是否可被取消（协程场景）
blocking	false	标记阻塞操作，检测非阻塞进度保证时对其挂起不判失败
promptCancellation	false	该可取消操作是否支持及时取消

两个实用技巧：

• 用runOnce = true测试"只能初始化一次"的方法；
• 用nonParallelGroup = "writer"把单写者接口约束声明出来，让框架按真实使用方式生成场景。

四、@Param：为操作定制随机参数

默认情况下 Lincheck 按类型自动生成参数。如果你想控制取值范围或分布，可以用@Param注解声明自定义参数生成器（定义见 lincheck/src/jvm/main/org/jetbrains/lincheck/datastructures/Param.kt）：

• 在测试类上用@Param(name = "key", gen = KeyGenerator::class)命名一个生成器
• 在操作上用@Operation(params = ["key"])把生成器绑定到指定参数

这样push(key: String)这类操作就能拿到你指定分布的测试数据，而不再是框架默认值。

五、选择测试策略：模型检查 vs 压力测试

check(this::class)之前的 Options 决定了"怎么测"，两种常用策略：

策略	原理	适合场景
模型检查ModelCheckingOptions	穷举线程间的交错调度，像"白盒"遍历状态空间	定位隐蔽竞态，能给出最小失败反例
压力测试StressOptions	大量随机场景 + 真实线程并行运行	快速冒烟、验证长时间运行行为

理解二者差异，关键是分清执行场景与执行调度：

• 场景：操作被分配到哪些线程、各自的顺序（"剧本"）；
• 调度：操作在每条指令边界如何交错（"导演节奏"）。

模型检查会对每个场景反复运行不同调度，直到找到违反一致性的交错；压力测试则让真实线程自由并发。策略详解见 docs/topics/lincheck-testing-strategies.md。

六、测试失败时你得到什么：可读的反例报告

这是 Lincheck 最"香"的部分：失败时它会打印一个精确的最小反例报告——哪个线程、以什么顺序、执行了哪些操作、各操作返回了什么。模型检查还会结合线性一致性验证器（如 lincheck/src/jvm/main/org/jetbrains/lincheck/datastructures/verifier/LinearizabilityVerifier.kt）把并发结果与顺序语义对比，甚至能把数据结构行为压缩成 LTS 状态图帮助定位。

一个真实场景：用声明式测试测ConcurrentHashMap.computeIfAbsent，Lincheck 直接输出了三条线程互锁的死锁执行轨迹，每一格都是方法级事件，排查时一目了然：

七、实战案例：一行注解抓出 TreiberStack 的 ABA 竞态

看官方示例 examples/src/test/kotlin/org/lincheck/docs/TreiberStackTest.kt：push/pop各标一个@Operation，测试函数一行模型检查。原实现pop()没做 CAS 重试，两个线程可能同时弹出同一个元素——模型检查会稳定地跑出反例报告，并告诉你"在 Thread 1 的 pop 读走 head 后、Thread 2 抢先入栈"这一交错如何导致重复出栈。按报告提示补上 CAS 循环后，测试通过。整个过程你只写了 4 行测试代码。

八、上手清单

1. 在测试项目中加入对 Lincheck 的依赖，或克隆源码查看各模块：git clone https://gitcode.com/gh_mirrors/li/lincheck
2. 测试类持有被测试结构的初始实例
3. 每个对外方法包一层并标注@Operation
4. ModelCheckingOptions().check(this::class)先行，稳定后再加StressOptions()长跑
5. 失败时先读报告里的场景和调度，通常能直接定位到出错代码行

掌握@Operation的声明式写法后，你就不再需要手写任何线程管理代码——把测试的"体力活"交给框架，把精力留给业务逻辑本身 💪。

【免费下载链接】lincheckFramework for testing concurrent code on JVM languages项目地址: https://gitcode.com/gh_mirrors/li/lincheck