《Java 并发编程·性能诊断与事故》8.2 Lincheck 的线性一致性检查

承接的问题

8.1 的 JCStress 靠概率采样碰交错：两轮各 2 亿多个样本，命中率 8.25% 和 7.65%。这种方法的优点是贴近真实硬件，缺点是不保证覆盖——如果那个窗口再窄十倍，你可能跑一晚上也看不到一次。

Lincheck 走另一条路：它不靠碰，而是系统地枚举有限的线程交错，并在发现「结果无法对应任何合法的串行执行」时，直接给出一个最小化的失败场景。它回答的问题也更精确：不是「有没有奇怪的结果」，而是「这个并发对象是否线性一致（linearizable）」。

这一节讲三件事：线性化点到底指什么、Lincheck 怎么生成和缩小场景、以及一个 Kotlin + Maven 的最小工程长什么样。必须先说明：本节未在本机执行。本机没有 Kotlin 编译器，按卷三的数据口径，下面所有运行输出都标注为「预期结构」而不是「本机输出」，具体原因在「为什么本节没有实跑」一节交代。

线性化点是什么

线性一致性的定义可以不用公式讲：

每个并发操作都像是在它的调用与返回之间的某个瞬间原子地生效，并且所有操作能排成一个与真实时间顺序一致的串行序列。

那个「原子生效的瞬间」就是线性化点（linearization point）。它不一定在代码的某一行上，但好的实现总能指出一个位置。

以库存扣减为例：

borrow():
  cur = stock.get()          // ① 读
  if (cur == 0) return -1    // ② 判断
  stock.compareAndSet(cur, cur - 1)  // ③ CAS

CAS 成功的那一次就是线性化点：在这一刻之前，其他线程看到的是旧库存；在这一刻之后，看到的是新库存。CAS 失败时操作没有生效，会重试，线性化点顺延到下一次成功的 CAS。

而 8.1 里的错误写法：

if (stock.get() > 0) {       // ① 读 + 判断
    stock.decrementAndGet(); // ② 写
}

找不到一个点能让整个操作原子生效：① 和 ② 之间可以插入另一个线程的完整操作。两个线程都读到 1、都通过判断、都执行 ②，结果就是库存 -1、成功两次。这个执行无法对应任何串行历史——串行执行两次 borrow()，第二次必然看到 0 并返回 -1。所以它不满足线性一致性。

线性一致性和「原子性」的区别也在这里：AtomicInteger.decrementAndGet() 自身是原子的，但「判断 + 扣减」这个复合操作不是。Lincheck 检查的是复合操作的线性化，而不是单个原子指令。

Lincheck 怎么生成场景

Lincheck 的核心输入是一个带 @Operation 注解的类。它把每个 @Operation 方法当成一个可被并发调用的操作，然后：

1. 生成场景（scenario）：一个场景由三部分组成——actorsBefore 个顺序执行的操作、若干线程并行执行的操作、actorsAfter 个顺序执行的操作。并行部分每个线程的操作数由 actorsPerThread 控制。
2. 执行并记录结果：每个线程按场景调用操作，记录返回值或异常。
3. 验证：检查这组「调用历史 + 返回值」是否存在一个合法的串行顺序。默认验证器是线性一致性；也可以用 sequentialSpecification 指定一个串行参考实现。
4. 缩小失败场景：发现违反后，Lincheck 会尝试删减操作、减少线程，给出能复现问题的最小场景（minimizeFailedScenario，默认开启）。

两种策略：

模型检验更接近「证明」，但状态空间随线程数和操作数指数增长；压力测试更接近「高强度抽样」。本节显式使用 ModelCheckingOptions；如果调用 LinChecker.check(Class) 不传 options，Lincheck 会去读测试类上的 @ModelCheckingCTest / @StressCTest 注解，一个都没有时直接报 No Lincheck test configuration to run。

场景参数的决定性很强，给一组起点：

两个线程、每线程两个操作，已经足以暴露大多数「检查再动作」问题；把线程数直接拉到 8，往往只是让运行时间爆炸，而不是发现更多 bug。

最小示例：Kotlin + Maven

Lincheck 是 Kotlin 项目，注解和 API 都是 Kotlin 类型。最小工程需要三样东西：Kotlin 编译插件、lincheck-jvm 依赖、一个带 main 的 runner。

先给 pom.xml。这里有一个容易踩的坐标问题：Maven 要用 lincheck-jvm，不是 lincheck。org.jetbrains.kotlinx:lincheck 是 Kotlin Multiplatform 的元数据包，2.39 的 jar 只有 767 字节；真正的 JVM 实现在 lincheck-jvm，同一版本约 1.1 MB。用错坐标时编译能过，运行时才报找不到类。

<project xmlns="http://maven.apache.org/POM/4.0.0">
  <modelVersion>4.0.0</modelVersion>
  <groupId>com.plume.conc</groupId>
  <artifactId>conc-lab-lincheck</artifactId>
  <version>1.0.0</version>

  <properties>
    <kotlin.version>2.2.20</kotlin.version>
    <lincheck.version>2.39</lincheck.version>
    <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
  </properties>

  <dependencies>
    <dependency>
      <groupId>org.jetbrains.kotlin</groupId>
      <artifactId>kotlin-stdlib</artifactId>
      <version>${kotlin.version}</version>
    </dependency>
    <dependency>
      <groupId>org.jetbrains.kotlinx</groupId>
      <artifactId>lincheck-jvm</artifactId>
      <version>${lincheck.version}</version>
    </dependency>
  </dependencies>

  <build>
    <sourceDirectory>src/main/kotlin</sourceDirectory>
    <plugins>
      <plugin>
        <groupId>org.jetbrains.kotlin</groupId>
        <artifactId>kotlin-maven-plugin</artifactId>
        <version>${kotlin.version}</version>
        <executions>
          <execution>
            <id>compile</id>
            <phase>compile</phase>
            <goals><goal>compile</goal></goals>
          </execution>
        </executions>
        <configuration>
          <jvmTarget>21</jvmTarget>
        </configuration>
      </plugin>
      <plugin>
        <groupId>org.codehaus.mojo</groupId>
        <artifactId>exec-maven-plugin</artifactId>
        <version>3.5.0</version>
      </plugin>
    </plugins>
  </build>
</project>

jvmTarget 取 21 是保守选择：21 字节码在 JDK 25 上可以直接运行，而 25 这个 target 需要对应版本的 Kotlin 编译器显式支持。本节未在本机验证这个组合；如果你的插件版本明确支持 25，可以改成 25，改完先跑一次空 runner 确认能启动。

被测类故意保留竞态：

package com.plume.conc.lab

import org.jetbrains.kotlinx.lincheck.annotations.Operation

class StockCounter {
    private var stock = 1

    @Operation
    fun borrow(): Int {
        if (stock <= 0) {
            return -1
        }
        stock -= 1
        return stock
    }

    @Operation
    fun stock(): Int = stock
}

borrow() 返回扣减后的库存，卖光返回 -1；stock() 是只读操作。串行语义很清楚：初始 1，第一次 borrow() 返回 0，第二次返回 -1。

runner 只需要两行有效代码：

package com.plume.conc.lab

import org.jetbrains.kotlinx.lincheck.LinChecker
import org.jetbrains.kotlinx.lincheck.strategy.managed.modelchecking.ModelCheckingOptions

fun main() {
    val options = ModelCheckingOptions()
        .iterations(50)
        .threads(2)
        .actorsPerThread(2)
        .minimizeFailedScenario(true)

    LinChecker.check(StockCounter::class.java, options)
}

启动命令：

export JAVA_HOME=~/.jdks/jdk-25.0.5+8/Contents/Home
export PATH="$JAVA_HOME/bin:$PATH"
mvn -q compile
mvn -q exec:java -Dexec.mainClass=com.plume.conc.lab.StockCounterRunnerKt

再次强调：以上命令本节没有在本机执行。 下面的报告结构是 Lincheck 2.39 的格式说明，不是本机输出。

报告怎么读

如果代码按上面的写法跑起来，预期会失败，因为 borrow() 的读和写在两个线程之间没有原子性。报告的第一段是「非法执行结果」表：

= Invalid execution results =
| ---------------------------------- |
| Thread 1        | Thread 2         |
| ---------------------------------- |
| borrow(): 0     |                  |
|                 | borrow(): 0      |
| ---------------------------------- |

读法是：两个线程都拿到 borrow(): 0。串行语义下，初始库存 1，第一个 borrow() 返回 0 之后库存已经是 0，第二个 borrow() 只能返回 -1。两个 0 不可能来自任何串行顺序，所以这组结果非法。

第二段是导致该结果的交错轨迹（interleaving trace），通常会逐步列出每个线程的读、写、CAS 或方法调用。这一段才是修 bug 的依据：它直接告诉你「线程 2 的读发生在 线程 1 的写之前」。如果报告只给结果表不给轨迹，通常是场景太小、或者操作没有被正确拦截。

第三段是最小化后的场景。Lincheck 会尝试删掉不相关的操作，最后可能只剩两个 borrow()。这比 JCStress 的 2 亿个样本好读得多：它给的是一个确定的、可复现的失败序列，而不是一个概率。

修复后（把 borrow() 换成 CAS 循环），预期输出是一行通过信息，不再打印结果表。注意：Lincheck 不打印「跑了多少次」的样本数，它打印的是迭代数和场景数；这与 JCStress 的计数口径不同，报告里不能混用。

如果跑起来看到的是「没有发现任何违反」，先别高兴，按顺序检查：

1. @Operation 方法是不是 public，类是不是 public 且有公开无参构造器；
2. 操作里的字段是不是被 Lincheck 的拦截机制看见了（纯 Kotlin 私有字段在某些优化下可能被内联）；
3. 初始状态是不是真的为 1（构造器里写死，别依赖外部注入）；
4. iterations 和 actorsPerThread 是不是太小。

为什么本节没有实跑

按卷三的数据口径，没跑过的工具不能写成跑过。这一节的情况有三层，逐层交代。

第一层：版本号对不上。 三卷契约里写的是 Lincheck 2.44，但 Maven Central 上并不存在这个版本。2026-10-29 实测：

curl -s https://repo1.maven.org/maven2/org/jetbrains/kotlinx/lincheck/maven-metadata.xml
# <latest>2.39</latest>
# <release>2.39</release>
# <lastUpdated>20250409124304</lastUpdated>

curl -s -o /dev/null -w '%{http_code}\n' \
  https://repo1.maven.org/maven2/org/jetbrains/kotlinx/lincheck/2.44/
# 404

所以本节用 2.39。如果团队内部镜像确实有 2.44，把版本号替换即可，API 以对应版本文档为准；但「2.44 在 Maven Central 可下载」这句话是不成立的。

第二层：Kotlin 运行时不在本机。 which kotlinc 返回空，本机没有安装 Kotlin 命令行编译器。Maven 理论上可以下载 kotlin-maven-plugin 代劳，但那会引入一整套未经验证的工具链；在 load average 常年 70–170 的机器上，把「没跑过」写成「跑过」的风险远大于收益。

第三层：没有可引用的真实输出。 本机只做了两件可核对的事：用 javap 确认 2.39 的 LinChecker.check(Class, Options)、ModelCheckingOptions、@Operation、@Param 签名存在；用 curl 确认版本与坐标。没有执行 LinChecker.check，没有生成过报告，也没有最小化场景的真实输出。

跑不起来时的典型报错，和「跑起来应该看到什么」，要分开记：

最后一行是关键：LincheckAssertionError 是 Lincheck 发现 bug 的正常方式，不是「环境没配好」。把它和依赖错误混在一起，就会把真正的竞态当成工具故障忽略掉。

在 libraryd-conc 里落地

Lincheck 适合放在 conc-lab 的算法级测试里，和 JCStress 分工：

给 StockCounter 这类小对象写 Lincheck 测试时，把「串行参考实现」单独写一份，用 sequentialSpecification(...) 指过去，比让 Lincheck 自己推断更可靠：

class SequentialStockCounter {
    private var stock = 1
    fun borrow(): Int {
        if (stock <= 0) return -1
        stock -= 1
        return stock
    }
    fun stock(): Int = stock
}

然后在 options 里加 .sequentialSpecification(SequentialStockCounter::class.java)。这样验证器比较的是「你的并发实现」与「一份明显正确的串行实现」，而不是从调用历史反推语义。

常见错误与边界

什么时候不要用 Lincheck：当被测逻辑依赖数据库、网络或真实时钟时。Lincheck 的模型检验需要在操作边界插入抢占点，阻塞调用会把「枚举交错」变成「等待超时」；这类问题应该用压测和故障注入，而不是模型检验。

小结

Lincheck 的价值在于把「碰运气」换成「枚举 + 最小化」：线性化点定义了每个操作何时原子生效，场景生成把调用历史摊开，验证器判断这组历史能否排成合法串行序列，最小化则把失败缩到两三个操作。它给出的不是命中率，而是一个确定的失败序列——这正是回归测试最需要的输入。

代价是它只适用于内存中的并发对象，而且需要 Kotlin 工具链。本节没有在本机执行，所有报告结构都按 2.39 的格式描述；版本、坐标与 API 签名是核实过的，运行结果不是。

下一节处理最后一公里：拿到一个失败用例之后，怎么把它缩小、固定成回归测试，并放进 CI 而不把构建时间拖垮。

阅读导航：上一节 8.1 JCStress 的测试模型 ｜ 下一节 8.3 竞态复现、最小化与回归