"线程很简单" — 一个大到没人去核实的谎言

启动一个线程是一行代码 — new Thread(r).start() — 而这一行看起来和你写过的每一行代码一模一样。同样的字体。同样的分号。它没有任何地方在说：你刚刚改变了你的程序是什么。

但你确实改变了。一个顺序程序是一条路径 — 一个状态接一个状态，每一行的前置条件由它前面那一行建立。从上读到下，你就已经，在真实且严格的意义上，看到了它做什么。当第二个线程触碰同一片内存的那一刻，你的程序就不再是一条路径，而变成了一个空间：每个线程的每条指令的每种可能交错构成的集合，而你程序的正确性不再是文本的属性 — 它是那个空间里每个点同时的属性。你没有添加一个特性。你改变了你负责的数学对象。

一行 fork，一辈子推理

那个空间有多大？两个各仅一百条指令的线程能以"200 选 100"种方式交错 — 大约 9 × 10⁵⁸ 种不同执行。加第三个线程：超过 10¹⁴⁰。第四个：超过 10²³⁶。作为参照，可观测宇宙大约有 10⁸⁰ 个原子。而阶乘计数其实还是乐观模型 — 它假设硬件执行的是你的指令的某种诚实交错。现代 CPU 并非如此：存储缓冲区和乱序执行产生的行为不是程序文本的任何交错，这正是为什么内存模型存在的原因。

那些数字所谴责的 — 对此必须精确 — 是采样。测试套件是一次采样。把一个线程测试跑一百万次，一个英雄式的 CI 预算，面对 10⁵⁹ 种调度你检查的行为占比是小数点后跟五十个零的分数。一个十亿次调度中出现一次的竞争，在你负担得起的每次运行里都通过，然后遇到一台时机不同、负载不同、核数不同的生产机器 — 一台采样空间不同区域的机器 — 就触发了。这就是为什么并发 bug 是臭名昭著的heisenbug：挂上调试器，加一行日志，时序就偏移到足以让你离开致命点。bug 没有躲着你。是你看的时候移动了。

"但没人靠枚举来验证" — 没错。这正是起诉书

一位敏锐的读者已经在构思反驳：从来没人靠枚举状态验证过任何东西。 一个对两个 64 位输入的顺序函数有 2¹²⁸ 个输入状态 — 同样超过原子数 — 而我们眼都不眨，因为验证从来不是枚举。它是做商集：你陈述一个不变式，证明代码维护它，十亿个状态坍缩成一个等价类。一个互斥锁正是这样一步 — "这个临界区里的所有交错等价于一个" — 而一个锁纪律论证是一份证明草图，把 10⁵⁹ 种调度做商集到少数几种情况。所以空间的大小，单独地，谴责的是测试而非推理。不可判定性单独也不谴责线程 — "这个顺序程序会不会除以零"按同样的 Rice 定理也不可判定，而我们照样发布顺序程序。

那为什么顺序推理在与它庞大的空间的接触中存活下来，而线程推理却淹死在它的空间里？因为顺序不变式有三个属性，而共享内存线程恰好摧毁了它们：

它们是局部的。 关于一个变量的顺序不变式只被提及它的那些行威胁 — 你能找到它们，读它们，就完了。在共享内存下，任何线程，从代码库的任何地方，触碰任何共享字段，都能使你在这里做的推理失效。证明义务不再是"检查这个函数"，而变成"对照一切运行的东西检查这个函数"。

它们是可组合的。 两个正确的顺序模块在它们的接口是全部故事时组合成一个正确的程序 — 而这恰恰是一个类型系统能陈述和检查的条件（没有隐藏别名、没有共享全局变量；顺序语言花了五十年用机器强制执行这一点）。两个各自正确的加锁模块，当你以错误顺序调用它们的那一刻就会死锁 — 而没有任何接口能表达这个条件，因为锁顺序是动态执行的属性，不属于任何签名。文明用来从小的已验证部件构建大系统的那个工具，在 fork 调用面前活不下来。

而且没有东西检查它们。 这是致命的那条。你的商集 — 锁顺序、happens-before 边、"只在 lockX 下触碰"的约定 — 住在注释和文化里。忘记一个 volatile，在一条罕见分支里以错误顺序获取两把锁，编译器什么也不说，类型检查器什么也不说，测试（见上文）什么也不说。顺序代码的不变式被不断地检查 — 类型、边界、空值分析、borrow checker（如果你有的话）。线程代码的不变式是承重却不受强制的。语言把工程学里最大的证明义务交给你，并按荣誉系统来评分。

现在再看看那把锁，因为在这个光线下，互斥锁 — 那个体面的、教科书式的、经过代码审查的互斥锁 — 被揭示为这个谎言的缩影。一把锁做出一个诱人地局部的承诺："在这个区段里，你独处；顺序推理被恢复了。"但这个承诺是否成立是一个全局属性 — 它依赖于程序里的每一把其他锁，以每种顺序，在每条路径上获取，包括明年某个从未见过你的锁的人写的那些。这个承诺在它被做出之处无法检查，在任何别处可被打破；遵守它的代价恰恰是它存在所允许的并行性（一把竞争的锁是一个穿着并发外衣的串行化点）；而它的失败模式，死锁，恰恰是没有任何检查器会认证的活性属性。锁不是管理共享内存的工具。它是一份顺序性的租约，其条款无人执行。

在口号之前，做一个让步，因为每位审稿人都见过反例：一个叶模块里的单一粗锁 — 它下面没有调用、没有第二把锁在望、不变式能用一条注释陈述 — 在那个尺度上是诚实的；你确实能在局部验证它。麻烦在于锁的诚实性不扩展，而且没有东西告诉你何时你离开了诚实区：每加一把锁、每在持锁下加一个调用、每加一个新调用者都倍增全局义务，而语言在"一把锁，一杯咖啡就能验证"和"四十把锁，不可搜索的空间"之间不画任何线。外衣在小 n 时完美合身 — 这可以说比从不合身还糟，因为四十把锁的程序就是这样建起来的：一次一把诚实的锁。

诚实的出口

如果病根是非局部、非组合、且不被检查的不变式，一个诚实的疗法必须机械地而非文化地修复这三者中至少一个。三个家族认真试过。

让商集被机器检查。 这就是 Rust：Send/Sync 和 borrow checker 把"谁可以从哪里触碰这个"变成类型，把数据竞争变成编译错误。按诚实原则，这是不变式从文化移入检查器，它配得上这份功劳。注意它的边界，不过：Rust 证明的是无数据竞争，不是活性 — 死锁仍然可表达且不被检查 — 而一个无竞争的执行仍然是非确定性空间里的一个点。你的 bug 在调度器有心情的时候复现。

让组合代数成真。 这是软件事务内存，它值得公正的听证，恰恰因为它点名针对非组合性：可组合的原子块，带 retry/orElse，恢复了锁所摧毁的代数。在 Haskell 里它是真的且被类型约束。为什么它不是答案？因为性能故事在规模化时从未兑现；因为命令式语言的 STM 变成了弱原子的，在每个事务/非事务边界重新引入了走火；而即使一个工作的 STM 也把你留在和 Rust 一样的地方 — 在一个非确定性调度里竞争安全，没有日志。组合性是正确的目标。它底下的执行模型仍然是那个空间。

让空间无法表达。 这是 Erlang 的路，也是我们的路：SuperJ 没有线程。 没有 Thread、没有 synchronized、没有 volatile、没有内存模型 — 因为内存模型是我们拒绝接纳的构造的补丁。一个 SuperJ 进程是一个线程执行一条路径：从上到下读代码你就看到了它做什么。在运行时之上，10¹⁴⁰ 个点坍缩回一条线，而你写的每个不变式都是局部的、可组合的、而且 — 既然是顺序的 — 可检查的。

应该说一下，Rust 把第一条和第三条出口分开卖 à la carte — channel 和所有权转移是地道的 Rust，一个有纪律的团队可以只过消息传递的日子。区别在于 SuperJ 把第三条出口设为强制性，而原因是其他出口都没有的那张牌：不是安全，而是确定性 — 事件被排成一条记录的顺序，而这正是这整个设计的回报所在。

空间仍然住在哪儿 — 我们的忏悔，明白地说

让我们说诚实版本而非讨喜版本。不可搜索的空间仍然存在于我们的代码库中。 声称的从来不是它可以被废除 — 硬件是共享内存；必须有东西发 fence。声称的是关于它住在哪儿，谁暴露于它，以及它被允许采取什么形状。在 SuperJ 里，共享内存并发只被批准用于一个制品 — 无锁队列 — 别的什么都不行。不是"主要是队列"。一个制品，而且注意是什么让它成为诚实的那个：一把锁假装共享世界是顺序的；队列什么都不假装。它承认共享，把它限制在一个狭窄的协议里 — 一个槽位的环，单写者游标（所以它大部分根本不需要原子操作），一次 release store 来发布，一次 acquire load 来消费 — 而且为了一个目的而存在：把数据从共享内存世界移到消息世界，在那里推理又变成局部的。

它是两个模型之间的气闸，由写下了内存模型论证的人一次性工程设计，经过验证和回归门控，里面没有一把锁。在那层之上空间是无法表达的：没有应用程序员能重新打开它，因为语言没有为它准备词汇。Java 也做了专家层的举动，用 java.util.concurrent — 然后把裸 Thread、synchronized 和共享变异永远地卖给所有人，放在它旁边。两个设计之间的区别不是专家层是否存在。而是走火的枪是否也在货架上。每门有并发的语言都有一个祭司阶层；我们的只是不被允许分发反应堆的钥匙。

顺序是你画出的一种拓扑

取代线程模型的不是一句口号；它是一个有自己义务的具体架构。一个 SuperJ 系统是由队列连接的共享无关进程，它的规范形状是一个星：应用把命令发布到各自的应用队列；一个定序器 — 事件流的唯一写者 — 合并它们，给每条盖上一个单调递增的序列号，并发布一条每个应用独立消费的全序日志。在那个被定序的领域内保证是严格的：同一条日志，同一个状态，每次都是 — 从序列零重启一个应用，它一位一位地复现自己的状态。并行性来自跨核流水线各阶段以及来自分区成独立的被定序领域；需要全局顺序的流付定序器的代价，不需要的，就不付。

确定性必须以其真实强度来声称，而非其讨喜版本。 跨独立领域，跨领域到达顺序每次运行都变 — 所以强形式"相同输入，相同结果，每次运行"只在领域内成立，不是全局的。全局成立的是真正杀死 heisenbug 的属性：每次运行，无论它的跨领域时序如何落下，都是可重放的，因为每个领域的日志就是那个领域经历的调度。触发失败的那"十亿次之一"的排序不是你希望重新掷的骰子 — 它是一个文件。你再跑一次。它再发生一次。你修好它。

而残留的 bug 类是被命名的，不是被挥手dismiss的：消息传递让数据竞争无法表达 — 没有共享字段可撕裂 — 但协议竞争仍在（独立进程的消息仍以某种顺序到达），一个慢的消费者能像优先级反转饿死火星车一样饿死一条流水线，而带环和有界缓冲区的队列图能通过背压死锁。在 这个模型里，这些失败中的每一个都附带着它的日志。

而这篇文章自己的测试也必须对拓扑跑一遍。 队列图的无死锁性是局部的吗？不是 — 它是图属性。可组合的吗？不是 — 两条正确的流水线连起来时可以死锁。那它到底和 wiki 上的锁顺序约定有什么不同？这：锁顺序是动态执行的属性，散布在每条调用路径上，一般不可判定 — 而队列拓扑是静态的、有限的、可声明的，这把活性问题从 Rice 的领地移到一个你可以在图上跑的环检查。这是一个原则上的范畴性改进 — 可检查 vs 不可检查 — 而框架自带一个构建时的环和有界性检查，拒绝一个有界队列死锁并点名它的队列。规范的星通过，它的环被识别且以策略标注而非仅仅画出来。

收据

LMAX 的单线程事件溯源核心跑赢了锁调优的行业。Redis 到今天在一个线程上执行命令（I/O 在 6.0 得到了辅助线程；数据结构从来不需要它们）。Node 用一个循环接管了 web I/O。我们自己的：进程间 88 纳秒的框架往返，每秒 1060 万条消息，是它重新实现的多线程 JVM 系统的 2.1×，外加全序和可重放日志。在真实代价是缓存行争用和一致性流量的硬件上 — 恰恰是共享最大化而共享无关避免的东西 — 队列不是你为安全付的税。它常常就是快路径。

不是耻辱

有一种反射是把"我们移除了线程"听成软弱的自白 — 好像一门严肃的系统语言欠你那把走火的枪，拿走它意味着我们驾驭不了它。反过来想。每个成熟的工程领域都保留着一份它拒绝建造的设计目录，因为它们无法被验证，而拒绝本身就是成熟。当分析说这个制品的失败空间无法被有意义地采样，无法被一般地判定，并且剥夺了驯服其他所有大空间的不变式推理 — 成年人的举动是改变制品，不是更努力地搜索。

承认某物不可计算不是耻辱。耻辱是知道它 — 而照样发布那个空间。