配置测试策略

Lincheck 支持测试策略的各种配置选项，包括场景生成、停滞执行检测、验证等。

如何启用选项

要为测试策略启用选项，请在策略类中进行设置：

@Test
fun modelCheckingTest() = ModelCheckingOptions()
    .iterations(100) // 指定生成的场景数量
    .check(this::class)

场景最小化

默认情况下，Lincheck 会尝试通过移除不改变测试行为的操作来最小化失败场景。

将 minimizeFailedScenario 选项设置为 false 可以查看完整的失败场景。

场景生成

选项	默认值	描述
iterations	100	生成的并发场景数量。
invocationsPerIteration	10_000	每个并发场景的调用次数。
threads	2	每个场景中的线程数。
actorsBefore	5	在场景并行部分之前调用的操作数量。
actorsPerThread	5	场景并行部分中每个线程的操作数量。
actorsAfter	5	在场景并行部分之后调用的操作数量。
customScenarios	–	自定义并发场景列表。自定义场景会在随机生成的场景之前执行。

定义自定义场景

Lincheck 使用一种领域专用语言来定义自定义场景：

@Test
fun test() = StressOptions()
    .customScenarios {
        initial {
            actor(SomeClass1::foo)
        }
        parallel {
            thread {
                actor(SomeClass1::buzz, 1)
                actor(SomeClass1::buzz, 2)
            }
            thread {
                actor(SomeClass1::buzz, 3)
            }
        }
        post {
            actor(SomeClass1::foo)
        }
    }
    .check(this::class)

每个场景由三个可选部分组成：

• initial – 在并行部分之前执行的操作。
• parallel – 线程定义。线程使用 thread 块定义。并行部分可能包含多个 thread 块。
• post – 在并行部分之后执行的操作。

操作使用 actor(function, arg1, arg2, ...) 函数定义。单个块内的操作按顺序执行。

停滞执行检测

选项	默认值	描述
timeoutMs	3000	调用超时（以毫秒为单位），超过此时间后 Lincheck 将报告停滞执行。
loopBound	50	循环迭代次数，超过此次数后 Lincheck 将报告停滞执行。 如果 Lincheck 为长循环错误地报告了停滞执行，请增加 loopBound 的值。 此选项仅适用于 模型检查。
recursionBound	20	递归调用次数，超过此次数后 Lincheck 将报告停滞执行。 loopIterationsBeforeThreadSwitch 的值应小于 loopBound。 此选项仅适用于 模型检查。

循环中的线程切换

选项	默认值	描述
loopIterationsBeforeThreadSwitch	10	线程在尝试切换到另一个线程之前可以执行的循环迭代次数。 loopIterationsBeforeThreadSwitch 的值应小于 loopBound。 此选项仅适用于 模型检查。

验证

选项	默认值	描述
verifierClass	LinearizabilityVerifier	在 验证过程 中使用的验证器类： LinearizabilityVerifier SerializabilityVerifier QuiescentConsistencyVerifier
sequentialSpecification	与测试的数据结构相同。	测试数据结构的顺序版本。该结构在 验证过程 中使用。

进度保证

选项	默认值	描述
checkObstructionFreedom	false	将此选项设置为 true 以验证数据结构操作的 无阻碍（obstruction-freedom）保证。 此选项仅适用于 模型检查。

库分析

选项	默认值	描述
stdLibAnalysisEnabled	false	默认情况下，Lincheck 不会验证标准库操作的行为，将其视为线程安全。将此选项设置为 true 以启用对标准库函数/类的分析。 此选项仅适用于 模型检查。
addGuarantee	–	使用 addGuarantee 选项为线程安全或与分析无关的方法 定义保证，以将它们从模型检查中排除。 此选项仅适用于 模型检查。

定义保证

要定义保证，请使用构建器链：先选择类，然后选择方法，最后选择保证类型。

@Test
fun modelCheckingTest() = ModelCheckingOptions()
        .addGuarantee(
            forClasses("java.util.concurrent.ConcurrentHashMap")
                .allMethods()
                .treatAsAtomic()
        )
        .check(this::class)

1. 使用 forClasses 重载之一选择类：

   • forClasses(vararg fullClassNames: String) — 如果类的全名存在于 fullClassNames 字符串中，则匹配。
   • forClasses(vararg classes: KClass<*>) — 通过引用匹配类。
   • forClasses(classPredicate: (fullClassName: String) -> Boolean) — 使用类全名上的谓词匹配类。

2. 选择要应用保证的方法：

   • methods(methodNames: String) – 如果方法名存在于 methodNames 字符串中，则匹配。
   • methods(methodPredicate: (methodName: String) -> Boolean) – 使用谓词匹配方法。
   • allMethods() – 匹配所选类的所有方法。

3. 选择保证类型：

   • treatAsAtomic() — 将每个方法视为原子操作。Lincheck 不会在方法调用内部插入切换点，但可能会在调用之前或之后添加。

     对于已知线程安全的方法，请使用 treatAsAtomic()。

   • ignore() — 从分析中排除这些方法。Lincheck 不会在方法调用内部、之前或之后插入切换点。

     如果方法内部使用了同步原语（例如 synchronized 块），忽略该方法可能会导致 Lincheck 死锁。

     对于与分析无关的方法（例如日志或调试实用程序），请使用 ignore()。

下一步

了解如何为 Lincheck 执行场景中使用的操作配置实参生成。

相关阅读

• 配置操作执行选项
• 检查非阻塞进度保证
• 定义算法的顺序规范