拆穿系统设计里的两种抽象：TLA+建模靠削减，Java封装靠隐藏！
计算机专业白学了四年，大多数人根本分不清两种抽象！
计算机系学生一进校门就学抽象数据类型，学接口封装，学分层层设计，学了一整套“抽象”的功夫。但一毕业去做分布式系统，还是翻车。代码写得再漂亮，系统一上线就崩。
这到底是为什么？
图灵奖得主莱斯利·兰伯特（Leslie Lamport）说过一句话：“抽象，抽象，再抽象，这就是你拿图灵奖的方法。”他重复了三次。但兰伯特说的抽象，跟计算机课本上教的抽象，压根不是同一个东西。课本教的是藏东西，兰伯特说的是砍东西。藏东西是把内部实现藏起来只露个接口。砍东西是把跟核心问题无关的细节全部扔掉只留骨架。两件事，方向完全相反。你以为是同一个词，其实是两门手艺。而很多人，一门都没练明白。
系统设计里的抽象分两种：模块化抽象靠隐藏内部细节，建模抽象靠削减无关信息。计算机课程只教前者，TLA+形式化方法和分布式系统协议全靠后者，Paxos、逻辑时钟、线性一致性都是削减出来的产物。
模块化抽象的核心就一个字，藏！
你写代码的时候，一定用过抽象数据类型。比如栈（Stack），你只需要知道有push和pop两个操作，底下是用数组还是链表实现的，完全不用管。这就是模块化抽象的标准案例。操作系统里更多：虚拟内存把物理内存和磁盘的细节藏起来了，让你以为内存是无限大的。TCP协议把IP包的路由和重传藏起来了，让你以为网络是可靠的。文件系统把旋转的磁盘磁道和扇区藏起来了，让你只用文件名就能读写数据。SQL数据库把查询计划和索引扫描藏起来了，你写个SELECT就行了。这些东西的核心操作都是封装。
模块化抽象的祖师爷是大卫·帕纳斯（David Parnas），他在1972年发表论文《On the Criteria To Be Used in Decomposing Systems into Modules》，第一次把"信息隐藏"当成拆分软件的标准：每个模块把容易变的设计决策藏在自己肚子里，只对外露出一个稳定的接口。两年后，图灵奖得主芭芭拉·利斯科夫（Barbara Liskov）在CLU语言里落实了抽象数据类型，简称ADT：你只能通过定义好的操作去碰数据，看不见里面是数组还是链表。
这条路线一路走到1995年诞生的Java：你写一个 interface，用 private 把字段锁起来，用 synchronized 把多线程的交错盖住，调用方看到的每个方法都像一口气做完的原子操作。这套做法的目标很纯粹，让模块好用，让模块好换，让模块好维护，调用者知道得越少越好。
它的核心动作是画一条竖线：线上面是接口，线下面是实现，线下面的东西对上面不可见。TCP把IP的丢包藏起来；文件系统把磁盘的磁道藏起来；SQL把查询计划藏起来。全都是这条竖线在起作用。
但是这条竖线有个副作用：它顺手把并发也藏起来了，一旦你想知道两个请求同时到达时到底发生了什么，接口不会告诉你，它的设计初衷就是不让你知道。好用和看得清，在这里是一对矛盾，对吗？
乔尔·斯波尔斯基（Joel Spolsky）在2002年写过一篇特别有名的博客叫“抽象漏洞定律”。他列举了一大堆例子。他说TCP偶尔会超时重传，这个细节会漏出来影响你的程序。字符串类偶尔会出现性能问题，你得知道底层字符数组是怎么存的。虚拟内存偶尔会卡顿，你得理解分页机制。NFS文件系统偶尔会因为网络问题卡住，你以为读写本地文件，其实网络断了一切都停了。他的结论是：所有不平凡的抽象在某个时刻都会泄漏。
你藏得越彻底，你就越看不见系统里真正会出事的那些东西。模块化抽象把并发操作包装成原子的、把网络包装成可靠的、把分布式状态包装成单机内存。这个做法在单机软件里非常好使，但一旦放到分布式系统里，它就成了灾难的温床。因为出问题的那些东西，全被你藏掉了。
建模抽象的核心也是一个字，砍！
跟模块化抽象对着干的，还有另一门抽象手艺。它不藏东西，它砍东西。它的目标是从复杂的系统里把跟当前问题无关的部分全部砍掉，只留下最核心的一小截骨架。这个骨架长什么样不重要，重要的是它能用来做精确的推理。
物理学家和数学家一直这么干：伽利略研究落体时把空气阻力砍掉，只留质量和加速度，因为他关心的性质是落体规律，空气阻力和这条性质无关。建模抽象的核心动作是先定一个你关心的性质，然后砍掉一切和这个性质无关的东西，剩下的骨架越小越好。
分布式系统里最经典的一刀，是兰伯特1978年的论文《Time, Clocks, and the Ordering of Events in a Distributed System》。多台机器的物理时钟对不齐，这是工程事实，兰伯特的处理方式是把物理时间整个扔掉，只保留"事件A发生在事件B之前"这一种关系，也就是 happens-before（先行发生）。一个计数器就够了：本地事件加一，收到消息取最大值再加一。他关心的性质是事件顺序，钟表读数和这条性质无关，所以砍。
后来的每一步都在重复这个动作：2014年提出的混合逻辑时钟（Hybrid Logical Clock，HLC）把物理时间捡回来一部分，同时保留因果关系，其余照砍；2012年谷歌在Spanner论文里提出TrueTime，直接把"现在几点"改成"现在在这个区间内"，区间宽度通常只有几毫秒，不确定性被明明白白写进模型，而没有被塞进接口后面。
再看共识问题：你要让一组节点对同一个值达成一致。莱斯利·兰伯特设计Paxos的过程就是抽象的大师课。他先抽象出“共识”这个核心问题，然后抽象出“投票”这个机制，最后一步一步精化到最终的协议。每一步都在砍东西，每一步都在扔掉跟核心问题无关的细节。
线性一致性（Linearizability）这个一致性模型，它的抽象做法是把复制、缓存、重试全部扔掉，只保留“所有操作看起来像是瞬间完成的，并且严格按全局时间顺序排列”这个行为特征。
“日志即数据库”这个想法是怎么来的？把物化状态作为事实来源这件事扔掉，只保留有序的、只能追加的事件序列。
MapReduce和Spark的抽象思路也一模一样，把编排、并行、调度、容错这些细节全部扔掉，只保留一个确定性变换的有向无环图（DAG）。
有时候你会看到同一个概念被两边都拿来用。比如线性一致性，比如共识协议，比如“日志即数据库”，再比如MapReduce。这不是说两种抽象重合了，而是说一个设计得好的工件可以同时服务两个目的。它既是一份可以直接精化成代码的规约，又是一个可以从中做推理的骨架。但抽象的角色依然是分开的。你不能因为一个东西同时干了两个活，就说这两件事是一回事。
莱斯利·兰伯特发明的TLA+就是一种形式化规约语言，专门用来对并发和分布式系统进行建模和验证。但TLA+真正教给你的不是语法，而是一种全新的看系统的方式。兰伯特在2019年的一场演讲里又重复了那句话：“抽象，抽象，抽象，这就是你拿图灵奖的方法。”他说的这个抽象，是“砍掉一切无关细节”的抽象。他有一个特别形象的比喻：你把一个复杂系统想象成一块石头，你要验证某个性质，比如“这块石头会不会碎”，那你就得把石头的颜色、纹理、产地全部砍掉，只留下硬度和受力点。建模抽象干的就是这个活。
戴克斯特拉（Edsger W. Dijkstra）也表达过类似的意思，他说抽象的目的不是把东西变模糊，而是创造一个全新的、干净的语义层面，让你可以在那个层面上做绝对精确的推理。模块化抽象把并发藏起来让你省心，建模抽象恰恰相反。它故意把并发的细粒度动作全部摆到桌面上，一个交错一个交错地检查，然后证明在这些交错发生的情况下系统的不变量依然成立。这件事很累，很费脑子，但做完了之后你能从系统里榨出最大程度的安全并发。兰伯特还说过一句更狠的话，他说计算机科学家集体患有一种叫“沃尔夫综合征”的病，症状就是把语言和现实搞混了。你写代码写久了，就会误以为代码就是系统本身。但代码只是描述，系统才是现实。建模抽象让你跳出代码，用数学重新描述系统。
这一刀切下去的方向和模块化抽象完全不同：它是横着切的。逻辑时钟不属于任何一层，网络层用它，操作系统层用它，应用层也用它，它切出来的骨架和系统原本的分层结构长得一点都不像。
一个竖着藏，一个横着砍，同一个词，两个动作，方向垂直！
一个抽象把并发藏起来，另一个逼你把交错写出来
并发是两种抽象分道扬镳最明显的地方，也是你最能亲手试出来的地方。在Java里，你给方法加上 synchronized，交错就消失了，调用者永远看不到两个线程各执行到一半的中间状态，这是隐藏的胜利。
在TLA+里你做的事正好反过来。TLA+规格的核心是一个叫 Next 的公式，它把系统所有可能的动作用"或"连起来：节点发消息；节点收消息；节点崩溃；消息丢失。配套的模型检查器TLC由Yuan Yu在1999年写出，它会把这些动作的所有交错顺序全部穷举一遍，每一种顺序下都检查你写的不变量还成不成立。你想藏都藏不住，工具就是专门来翻你中间状态的！
亚马逊2015年在《Communications of the ACM》上发表论文《How Amazon Web Services Uses Formal Methods》，给了一个数字：他们用TLA+在DynamoDB的一个协议里找到一个bug，触发它最短需要35步高层动作的特定交错，代码评审没抓到，测试也没抓到，因为人脑和测试用例都不会主动去枚举35步的交错。同一篇论文还提到，亚马逊在S3、DynamoDB、EBS等十几个系统上用了TLA+，每一次都找到了之前没发现的设计缺陷。
转折来了。
暴露并发的目的是榨取：只有把交错全部摆出来并证明不变量扛得住，你才敢放心让更多操作并行跑，而用不着给一切加锁。隐藏并发换来的是好用，暴露并发换来的是安全的最大并发度，两种抽象各自收了不同的账，这两笔账没法互相替代，是不是？
Spolsky的抽象泄漏清单，为什么全是同一类东西
抽象泄漏这个说法来自乔尔·斯波尔斯基（Joel Spolsky），他在2002年11月11日的博客里提出"泄漏抽象定律"：所有不平凡的抽象在某种程度上都会漏。他举的例子一字排开：TCP藏IP，可网线一拔延迟就暴露；字符串库藏字符数组，可性能问题一来内存布局就暴露；虚拟内存藏分页，可换页一发生卡顿就暴露；SQL藏查询计划，可慢查询一来索引就暴露；NFS藏网络，可断网一来文件操作就挂。
把这份清单逐个看过去，一个规律浮出来：每一条都是模块化抽象，都是一条竖线下面的东西漏到了线上面。斯波尔斯基把泄漏当成抽象的敌人，整篇文章的情绪是无奈，工程师不得不回头学习被藏起来的那一层。
但是站在建模抽象这边看，泄漏是原材料。兰伯特写逻辑时钟时，正是抓住了"机器之间的顺序关系会漏出来"这个事实，然后专门为这个漏出来的东西造了模型。建模抽象的第一步就是问：哪些东西应该漏，漏出来的东西里哪一个决定了我关心的性质。
再看两个例子：线性一致性由莫里斯·赫利希（Maurice Herlihy）和珍妮特·温（Jeannette Wing）在1990年提出，它规定每个操作看起来都在调用和返回之间的某一瞬间完成，它砍掉了复制，砍掉了缓存，砍掉了重试，砍掉了网络分区，只留下"看起来一瞬间完成"这一条性质。
2013年杰伊·克雷普斯（Jay Kreps）在领英写的《The Log》，把数据库砍到只剩一个有序追加的事件序列，物化状态成了派生品。
2004年谷歌的MapReduce论文，把调度、并行、容错全砍掉，只留 map 和 reduce 两个确定性变换。
同一个词，一边把泄漏当敌人，一边把泄漏当原料，这已经是两个概念了！
大部分工程师为啥学不会这门手艺
计算机专业教了整整四年的抽象，教的全是模块化抽象。你学ADT，学接口，学分层模式，这些东西的核心全是藏。你藏得好，老师给你高分。但建模抽象的核心是砍。你砍得好，你的模型才能用。这两个技能树的根上就不一样。一个精通封装的人，真不一定知道该砍掉什么。
建模抽象最难的环节恰恰就在这里。你得判断什么东西是“正交”的、可以安全砍掉的。这个判断需要非常扎实的领域知识，需要设计直觉，很多时候还需要反复试错。砍多了，你要验证的那个核心性质丢了。砍少了，模型太复杂，状态空间直接爆炸，没法分析。莱斯利·兰伯特在TLA+的课程里说过，编程语言本身没法在代码层面之上做抽象。代码就是实现，你站在实现里谈抽象，永远跳不出来。你得用数学语言，用状态机，用谓词，用不变量，在代码之上的那个层面做推理。
很多工程师根本不知道还有“建模抽象”这回事。他们以为自己在做抽象，其实只是在做封装。他们以为自己在简化系统，其实只是在藏东西。而分布式系统里最要命的问题就是网络分区、节点宕机、时钟漂移、消息乱序这些东西。模块化抽象把这些全藏了，建模抽象把这些全摆出来了。
你以为你懂抽象？你可能只是懂了前半段。
Paxos同时干两份活，两种抽象又合体了吗
Paxos是分布式共识算法，兰伯特1998年正式发表，2001年又写了《Paxos Made Simple》。共识问题本身就是建模抽象的产物：多台机器，任意崩溃，消息任意延迟，最后要对一个值达成一致，其他一切砍掉。兰伯特在TLA+教学页面上把Paxos分三层写：最顶层是Consensus，只说"最终选出一个值且不再改变"；中间层是Voting，引入投票和法定人数；最底层才是带消息收发的Paxos。每一层都比上一层多一点"怎么做"，每一层都被证明是上一层的细化。
这里出现一个看似打脸的现象：Paxos的Consensus规格既是拿来推理的骨架，也是工程师照着实现的接口。线性一致性也一样，既是砍出来的最小性质，也是数据库对客户端的承诺。MapReduce更明显，那个只剩两个变换的骨架同时也是程序员写代码的API。两种抽象好像重合了？
但是重合发生在产物上，没发生在动作上。一份写得足够好的规格可以同时被两拨人使用：实现者拿它当竖线上面的接口，往下填代码；推理者拿它当横切出来的骨架，往上证明性质。同一张纸，两种读法，产生它的动作仍然是削减，拿它去封装则是另一件事。
判断点到了。
区分两种抽象的标准落在动作上：你在画边界，还是在选性质并砍掉无关项？画边界的产物可能恰好被拿来推理，砍出来的骨架也可能恰好成为接口，但动作本身不会互相转化。
学校四年教的是第一个动作，形式化方法要求的是第二个，缺口就在这儿，不在智商！
工业界早就拿真金白银在投票了
有些人觉得形式化建模是学术界的小打小闹，离工业界很远。实际情况完全相反。
亚马逊的AWS团队早在2014年就公开发表过TLA+在复杂系统设计中的成功经验；微软的Azure Cosmos DB团队用TLA+建模客户可见的一致性语义；他们只建模“历史即日志”这个抽象层，把数据库内部细节当成环境来处理，最后五个一致性级别变成了操作历史上一组清晰的谓词。整个规约只有390行。就这么几百行的模型，帮助他们找到了一个持续了28天的高优先级故障的根本原因。
MongoDB在用TLA+，Oracle Cloud在用，谷歌在用，LinkedIn在用，Datadog在用，英特尔也在用。这些公司不是学术机构，他们是真金白银往里砸的。他们用TLA+不是为了发论文，是为了在写第一行代码之前就把设计错误揪出来。
IBM的研究员在2014年就发表过一篇经验论文，标题是“商业系统开发中的形式化规约”，里面详细记录了TLA+如何帮助工程师在设计阶段发现那些用测试几乎不可能找到的并发缺陷。分布式系统里有些bug，你代码写得再好、测试覆盖率再高，跑不出来就是跑不出来，只能在模型层面抓出来。
这就是建模抽象在工业界的价值。它不是锦上添花，它是在救命。
写模型前的三个动作，和Chubby没堵上的缺口
第一个动作：你先用一句话写下要保住的性质，再动手写模型。逻辑时钟保的是事件顺序；线性一致性保的是单点瞬时完成；Paxos保的是选出且只选出一个值。性质一句话写不出来，说明你还在描述系统，还没开始建模。写出来之后，逐个变量问：删掉它，这条性质的判断会变吗，不变就删。
第二个动作：你把模块边界当实现工具，别当思考工具。建模时允许自己跨层横切，把网络层的消息丢失和应用层的状态更新写进同一个 Next 公式里，这在Java代码里是坏味道，在TLA+模型里是常规操作，因为你关心的性质本来就跨层。
第三个动作：你在模型里故意把并发写成"或"，把每个动作拆到可以交错的最小粒度，然后让TLC去穷举。亚马逊那个35步的bug证明了一件事：交错只要没被枚举，就等于没被检查，synchronized 能让代码好用，但它不会替你证明不变量。
但是砍到最小的骨架，落回真实系统时会不会重新长满肉。谷歌2007年在PODC会议上发表《Paxos Made Live》，讲的是把Paxos做进锁服务Chubby的经历，图沙尔·钱德拉（Tushar Chandra）等作者写道：算法论文和生产系统之间存在显著差距，他们不得不加入磁盘损坏处理；主节点租约；快照；成员变更等一整套机制，而这些都不在被证明过的骨架里，最后系统仍然依赖大量测试，而且测试确实抓出了bug。
一边是兰伯特三层细化、每层可证的Paxos，一边是谷歌工程师说证明过的算法只是起点。砍出来的骨架越干净，回填的时候漏得越多吗，还是回填的每一块本来都该再砍一遍单独建模，Chubby的论文没有回答，TLA+社区到今天也没有一份公认的答案。
原文期刊：muratbuffalo.blogspot.com / 发表日期：May 08, 2026 / 原文标题：The Two Abstractions of System Design: Hide or Reduce / 作者单位背景：独立博客作者，分布式系统与TLA+实践者