企业官网建设流程全解析

Apache Cassandra 中的 TLA+ 不变量（Invariants）与属性（Properties）实战指南

【免费下载链接】cassandraOpen source transactional distributed database. Linear scalability and proven fault-tolerance on commodity hardware or cloud infrastructure without compromising performance.项目地址: https://gitcode.com/GitHub_Trending/cassa/cassandra

本篇指南围绕 TLA+ 形式化规格中的**不变量（Invariants）与属性（Properties）**体系展开：从安全属性（Safety）、活性属性（Liveness）、时序算子组合到公平性（Fairness）假设，再到基于 TLC 模型检查器的调试手段。文中所有模式均以 invariants.md 为骨架，并以 Apache Cassandra 仓库中formalise/accord/的真实 TLA+ 规格（AccordExec.tla、AccordNotify.tla）作为实战佐证。读完本文，你将掌握如何为分布式系统编写类型不变量、互斥与一致性安全属性、基于[][...]_vars的动作属性、~>leads-to 活性属性，并理解为何公平性是活性验证不可或缺的前提，以及如何用覆盖探针（Coverage Probes）避免"绿色表格但从未真正检验"的假阳性。

属性（Property）的四大类型

TLA+ 中一个系统由Init /\ [][Next]_vars定义的状态机刻画，而"要证明系统是对的"则体现为对状态、对转换、对行为序列的各种断言。理解这些断言的类型是第一步：

简记之：不变量检查"每一个状态都健康"，动作属性检查"每一步转换都合法"，安全属性检查"坏序列永远不会出现"，活性属性检查"系统一定会取得进展"。死锁（deadlock）是安全属性，活锁（livelock）与饥饿（starvation）是活性属性，二者在 TLC 中需要用不同的机制去发现。

类型不变量（Type Invariants）：永远第一个写

类型不变量是所有不变量中最先、也最应该先写的一个：它把每个变量约束到其合法值域上，用于尽早捕获规格自身的笔误（例如把queue的更新写错了类型、把函数作用域写反）。

TypeInvariant == /\ counter \in 0..MaxVal /\ lock \in Processes \union {NULL} /\ queue \in Seq(MessageType) /\ state \in [Nodes -> {"idle", "active", "done"}] /\ seen \subseteq AllItems /\ pc \in [Processes -> {"Init", "Work", "Done"}]

规则：

• 尽量紧（tight）：counter \in 0..MaxVal优于counter \in Int——类型不变量越紧，越能早期暴露规格 bug；
• 需要基于标签（label）推理时，务必包含pc：pc刻画每个进程当前所在程序点，是后续写"当且仅当在某个阶段时"类条件不变量的基础；
• 类型不变量能在建模早期就抓住规格 bug，因此永远是第一个写的。

仓库实例：AccordExec.tla的TypeOK

Cassandra 的 Accord 执行队列规格 AccordExec.tla（L504-L513）给出了一个贴近生产的类型不变量：它逐个变量声明类型，其中plog（每个 entry 的实际处理顺序日志）是逐元素定型的——因为Seq(Tasks)是无限集合，不能直接对 TLC 断言"属于某个无限序列类型"，只能退而检查每个元素属于Tasks：

TypeOK == /\ cfg \in [Tasks -> ConfigDomain] /\ phase \in [Tasks -> Phases] /\ pending \in [Tasks -> SUBSET KeyEntries] /\ adopted \in [Tasks -> SUBSET KeyEntries] /\ fifoAt \in [Tasks -> Nat] /\ DOMAIN plog = Entries /\ \A e \in Entries : \A i \in 1..Len(plog[e]) : plog[e][i] \in Tasks /\ clock \in Nat /\ loading \subseteq Entries

注释明确说明其目的："every variable, so that an arithmetic or Append bug in Run/Adopt is named here rather than surfacing as a confusing Inv_Isolation failure"——即让 Run/Adopt 动作里的算术或Append笔误以TypeOK失败的形式直接暴露出来，而不是伪装成某个不相关的隔离性不变量失败。这正是"类型不变量先写"哲学在生产级规格中的体现。

安全不变量（Safety Invariants）：断言危险状态永不出现

安全不变量断言危险的全局状态永远不会出现。以下四种是最常见的范式。

互斥（Mutual Exclusion）

MutualExclusion == \A p1, p2 \in Processes: (in_cs[p1] /\ in_cs[p2]) => p1 = p2 \* 等价写法：用基数（cardinality） MutualExclusion == Cardinality({p \in Processes : in_cs[p]}) <= 1

两种写法等价，但基数写法在"同时进入临界区的进程数"本身就需要被约束（如最多 2 个）时更易推广。

无透支（No Overdraft）

NoOverdraft == \A a \in Accounts: balance[a] >= 0

这是金融/资源类系统的经典约束：任何账户余额永不为负。

守恒（Conservation，封闭系统）

\* 系统中的钱的总量永远不变 Conservation == LET total == SumAll(balance) IN total = InitialTotal

封闭系统的总量守恒通常是一个"应该"成立而非"必须"成立的属性——转账时若守恒被破坏，往往是舍入或漏记账导致的。

跨副本一致性（Consistency Across Replicas）

\* 若一个值已提交，则所有副本必须一致 Consistency == \A k \in Keys: committed[k] => \A r1, r2 \in Replicas: data[r1][k] = data[r2][k]

这是分布式数据库最关心的属性：提交（committed）是"可对外宣布"的强前提，一旦宣布，任何副本上的读都必须看到同一值。Cassandra 的最终一致性模型无法在所有时刻满足这个强不变量，因此这类属性通常会被弱化为"最终一致"的活性属性（见后文EventualConsistency）。

仓库实例：Accord 的互斥不变量Inv_AtMostOneLock与可证伪性设计

AccordExec.tla（L550-L552）把互斥提升到锁维度：

Inv_AtMostOneLock == \A e \in Entries : \A t, u \in Tasks : (HoldsLock(t, e) /\ HoldsLock(u, e)) => t = u

值得学习的是它处理不变量空洞（vacuity）的手法。模型中的CanRun直接假定（ASSUME）了NoForeignLock守卫（对应实现lockExclusive开头的require(!isLocked())），因此若没有控制开关，这个不变量在任何 profile 下都不可能失败，是重言式（tautology）。为了让这一行有实际证据价值，规格引入PAllowDoubleLock控制常量：把它设为 TRUE（即ctl-double-lockprofile）会移除CanRun中的假设，使Inv_AtMostOneLock真正可被证伪（INVARIANTS.md §2 A3）。这是"每个不变量都必须在某个模型实例上真的可能被违反"这一方法论的可执行化。

条件不变量：用=>（蕴含）限定适用范围

很多属性只在特定条件下才成立——算法未完成时结果字段当然是"任意值"。用蕴含把不变量限定到适用场景，避免"不变量过强"的假失败：

\* 只在算法完成后检查 Correct == pc = "Done" => result = ExpectedResult \* 只在特定条件下检查 QueueBound == is_running => Len(queue) <= MaxQueueSize \* 进程级条件 WorkerCorrect == \A w \in Workers: pc[w] = "Done" => output[w] = f(input[w])

仓库实例：Inv_LockerIsFifo与阈值关系

AccordExec.tla（L519-L520）的条件不变量把"跨轮次持有锁的任务必须是 fifo 声明（claim）"这一规则无条件陈述：

Inv_LockerIsFifo == \A t \in Tasks : (phase[t] = "Started" /\ HoldsAcrossRuns(t)) => IsFifo(t)

对应实现是prepareExclusiveMayThrow的 O7 规则：INCR 任务若跨轮次持锁、或负有 ATOMIC 隔离义务，则必须先被打上 fifo 戳（stamp）再取锁（见 INVARIANTS.md §4 O7）。同样的思路还体现在执行阈值上：SYNC 任务需要它持有的每一个key 都就绪，而非同步任务只需min(剩余, MIN_BATCH)个，因此"一个任务能运行"是阈值关系而非合取关系——这正是CanRun用>= Threshold(t)而不用/\的原因（L293-L300）。

动作属性（Action Properties）：检查转换而非状态

动作属性用[][A]_v语法——它断言每一步转换要么满足 A，要么保持变量 v 不变。注意原文档强调的要点：[][A]_v展开为[](A \/ UNCHANGED v)，停顿（stuttering）总是被允许的，因此写动作属性时务必包含变量列表v，否则模型会因"允许停顿"而误报或漏报。

\* 计数器单调不减 CounterMonotonic == [][counter' >= counter]_counter \* 锁的所有权不能在进程间直接跳变 LockNotStolen == [][lock \in Processes => (lock' = lock \/ lock' = NULL)]_lock \* 版本号只增不减 VersionMonotonic == [][\A n \in Nodes: version[n]' >= version[n]]_version

仓库实例：L3_HandlerTakesNoPosition

AccordNotify.tla（L614）给出了一个动作属性的绝佳范例——它断言通知处理器（handler）不改变任何队列位置，而这个属性没有任何状态不变量能够表达：

L3_HandlerTakesNoPosition == [][Deliver => UNCHANGED << holds, region >>]_vars

Deliver动作在派发一条通知时会更新state/wtxn/wkey/blocking/notBlk等簿记，但绝不能插入、删除或移动任何队列位置（holds、region）。只有动作属性能精确表达"转换本身的副作用边界"。注释也诚实指出：在该模块中它是按构造成立的（HandleTxn/HandleKey返回的holds原样不变、没有任何 handler 触碰region），因此它是对模型的回归检查，而运行时的重入守卫才是对代码的检查（INVARIANTS.md §6 L3）。

活性属性（Liveness Properties）：断言系统取得进展

活性属性回答"系统是否终将做该做的事"，是死锁之外的另一个核心关切。

终将完成（Eventually Done）

\* 所有进程最终都结束 Termination == <>(\A p \in Processes: pc[p] = "Done")

最终一致（Eventually Consistent）

EventualConsistency == <>(\A r1, r2 \in Replicas: data[r1] = data[r2])

这正是 Cassandra 最终一致性语义的 TLA+ 表述：不强求每个状态都一致，只要求某个时刻之后所有副本对齐。

Leads-to（~>）：P 总导致 Q

\* 每个请求最终都会得到响应 RequestHandled == \A r \in Requests: r \in pending ~> r \in completed \* 每个入队元素最终都会出队 QueueDrained == \A item \in Items: item \in Range(queue) ~> item \notin Range(queue)

无饥饿（Starvation Freedom）

\* 每个进程最终都能进入临界区 NoStarvation == \A p \in Processes: pc[p] = "Waiting" ~> pc[p] = "InCS"

仓库实例：NoStuck、Termination与G4_Drains

Accord 规格中活性属性的分级设计极具参考价值：

• AccordExec.tla（L452-L457）用递归最小不动点定义EventuallyRunnable，再定义NoStuck——"每个活任务最终都能运行"，这是对"无活锁/无相互阻塞"的直接刻画：

RECURSIVE EventuallyRunnable(_) EventuallyRunnable(S) == LET nxt == S \cup {t \in Live \ S : TxnReady(t, S) /\ KeyReady(t, S)} IN IF nxt = S THEN S ELSE EventuallyRunnable(nxt) NoStuck == Live \subseteq EventuallyRunnable({})

• 它的Termination == <>[](\A t \in Tasks : phase[t] = "Done")（L603）用"最终永远"算子表达全体任务收敛到完成态；
• AccordNotify.tla（L604）的G4_Drains == []<>(Quiescent)则是活性形式的"通知级联最终会排空"——注意它必须作为PROPERTY而非INVARIANT提交给 TLC，因为它是时序陈述；
• matrix.py（L36-L43）在--liveness模式下才检查Termination，并特意把它放在不变量循环之后单独跑一轮——因为 TLC 在搜索过程中遇到第一个活性违例就会停下，若与安全不变量混在一起检查，会导致剩余不变量的安全搜索不完整。

组合时序算子（Composing Temporal Operators）

四个基础时序算子组合出全部常用活性模式：

记忆要点：<>[]P是"最终稳定"，[]<>P是"永远周期性"，两者在"收敛"与"持续服务"之间构成语义分界；P ~> Q等价于[](P => <>Q)，是刻画请求-响应、饥饿自由的核心工具。

公平性要求（Fairness Requirements）：活性验证的必要前提

活性属性几乎总是需要公平性假设，否则会因平凡的停顿反例（stuttering counterexample）而平凡地失败——系统可以"合法地"永远停顿，从而不满足任何<>属性。TLA+ 提供两种公平性：

\* 弱公平（weak fairness）：动作一旦持续使能，终将执行 Spec == Init /\ [][Next]_vars /\ WF_vars(Next) \* 按动作施加公平性 Spec == Init /\ [][Next]_vars /\ \A p \in Processes: WF_vars(Process(p)) \* 强公平（strong fairness）：等待锁的动作用 SF Spec == Init /\ [][Next]_vars /\ \A p \in Processes: SF_vars(AcquireLock(p)) /\ \A p \in Processes: WF_vars(ReleaseLock(p))

何时用哪种：

• WF（弱公平）：动作处于"持续使能"状态（无条件进展），如普通的计算步骤；
• SF（强公平）：动作处于"反复使能与失能"状态（如等待一把被他人占用的锁——锁释放前AcquireLock不可使能，释放后又可能被抢走），此时只有强公平才能保证"终将轮到"。

仓库实例：Spec中的公平性合成

两个 Accord 模块的Spec都是标准的三段式：

\* AccordExec.tla (L425-L428) Fairness == /\ \A t \in Tasks : WF_vars(TaskNext(t)) /\ \A e \in Entries : WF_vars(LoadCompletes(e)) Spec == Init /\ [][Next]_vars /\ Fairness

\* AccordNotify.tla (L532) Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

注意 Baseline.cfg（L47-L48）中的配套做法：Spec里的公平性合取是为Termination活性检查服务的，matrix.py只在--liveness下检查它。而 cfg 同时写了CHECK_DEADLOCK FALSE——因为规格显式建模了"任务间等待"关系，TLC 的默认死锁检测会把"合法等待"误判为死锁，这与 Acccord 的"等待是有向无环图（DAG）而非环"论证相一致（INVARIANTS.md §2）。

调试属性（Debugging Properties）

当某个不变量失败、需要观察反例轨迹时，TLA+ 提供三类手段。

Print 与 Assert（PlusCal 中，需EXTENDS TLC）

\* 在 PlusCal 中（需 EXTENDS TLC） assert x > 0; print <<"x =", x, "y =", y>>;

print会在 TLC 反例轨迹中打印变量快照；assert失败会立即终止并报告当前状态。

金丝雀不变量（Canary Invariants）

金丝雀不变量是故意写反（否定）的探针：它本身"应该"被 TLC 报告为违反，一旦违反恰好证明目标状态被到达过，从而确认模型确实经历了你关心的场景：

\* 强制一条轨迹，观察都存在哪些状态 DEBUG_SeenAllStates == Cardinality(explored) < MaxStates \* 强制一条到达特定状态的轨迹 DEBUG_NeverReaches == ~(state = "target_state")

配置中的 ALIAS

ALIAS让 TLC 在每次状态转换时打印一个便捷快照，无需改动原规格：

\* 在 .cfg 文件中：ALIAS DebugAlias \* 在 .tla 文件中： DebugAlias == [ state |-> state, state_next |-> state', queue_len |-> Len(queue), msg_count |-> Cardinality(msgs) ]

仓库实例：覆盖探针（Coverage Probes）体系

Cassandra 的 Accord 规格把金丝雀不变量发展成了一套工程化的覆盖探针。其核心洞见记录在 AccordExec.tla（L605-L609）的注释中："TLC reporting one violated means the situation is reached. A green table over a model that never holds a lock or waits on a threshold establishes nothing."——一个从未持有锁、从未等待阈值的模型跑出全绿表格，什么也没证明。

因此每个探针都是否定式可达性声明：探针 =~\E ... 目标情形 ...，TLC 报告它被违反，恰恰证明该情形在状态空间中真的出现过。例如：

\* 争用确实发生：两个任务在同一 entry 上都有位置 Probe_Contention == ~\E t, u \in Tasks : \E e \in Entries : t # u /\ HoldsPos(t,e) /\ HoldsPos(u,e) \* 锁确实被持有且确实有等待者 Probe_LockHasWaiter == ~\E t, u \in Tasks : \E e \in Entries : t # u /\ HoldsLock(t,e) /\ HoldsPos(u,e) \* 隔离性有东西可保护：同一原子单元的两个成员都处理过同一 entry Probe_UnitRevisits == ~\E e \in Entries : \E i, j \in 1..Len(plog[e]) : /\ i < j /\ UnitOf(plog[e][i]) = UnitOf(plog[e][j]) /\ plog[e][i] # plog[e][j]

AccordNotify.tla（L633-L652）里同样有Probe_Nested（期望不可达：通知派发深度为 1）、Probe_StaleBatch（级联中途书签暂时落后于队列的瞬态）等探针。而 matrix.py（L17-L29）把"探针是否被触及"变成契约的一部分："An unreached probe means an unchecked row, not a passing one"——探针未到达 = 该行未被真正检验，而不是通过；--no-probes虽然更快，但跑出来的全绿表格可能是空洞的（vacuous）。

常见错误（Common Mistakes）

原文档总结了 TLA+ 不变量写作的五大经典陷阱，逐一对照仓库实践：

1. 把=>与\E混用：\E x: P(x) => Q(x)几乎必然是错的——量词作用于整个蕴含式时，只要存在一个不满足P的x，整个式子就平凡为真。应写\E x: P(x) /\ Q(x)。Accord 中CanRun的\E batch \in batches : ...（AccordExec.tla L360）使用合取式，正是此原则。
2. 忘记公平性：没有公平进程假设，活性属性会因停顿反例平凡失败。Accord 的Spec显式带WF_vars合取（见上文）。
3. 不变量过强：在全局断言result = expected，而它只在结束时成立——应改为pc = "Done" => ...。Accord 的Inv_LockerIsFifo、Correct类属性都遵循"用蕴含限定作用域"。
4. 纯 TLA+ 中遗漏UNCHANGED：每个动作必须声明所有变量的变化，否则出现"幽灵赋值"。AccordExec.tla的每个动作都以UNCHANGED << ... >>收尾（如Setup的 L335），正是此纪律。
5. 对索引使用全称量词：\A i, j \in 1..Len(s): s[i] # s[j]在i = j时必然失败——必须写成\A i, j \in 1..Len(s): i # j => s[i] # s[j]（或\A i, j \in 1..Len(s) : i < j => ...）。

仓库实战：如何把本文模式落地到 Cassandra 的 Accord 规格

要实际运行本文提到的真实规格，可遵循以下仓库内路径：

1. 阅读规格与文档：AccordExec.tla 建模 Accord 每个 CommandStore 执行队列（AccordCacheEntry、AccordCacheEntryQueue、SafeTask）诱导出的等待关系，证明"无活任务相互阻塞（NoStuck）"、"关系无环（NoCycle）"以及词典序秩（RankOK）作为与规模无关的证书（该证书与 AccordAcyclic.lean 的 Lean 证明衔接，TLC 只负责验证实现是否维持了假设）；AccordNotify.tla 单独建模通知簿记层，使前者可以假定其保证（G1-G4）而不必建模。配套的 INVARIANTS.md 是每条不变量对应的实现代码与依赖代码的索引。
2. 运行单跑示例：formalise/accord/execution/tla/examples/下的 Baseline.cfg 与 Notify.cfg 提供了免驱动的快速迭代入口（README 说明需先把模块复制到同目录再tlc -cleanup -config Baseline.cfg Baseline.tla）。注意两个 cfg 都不列出覆盖探针，因为每个探针都是否定式可达性声明，TLC 遇到第一个被违反的探针就会停止，单跑只能告诉你第一个结果。
3. 跑完整矩阵：使用 matrix.py（AccordExec 的驱动）与notify.py（AccordNotify 的驱动），它们按(topology x profile)跑 TLC 并制表。其中ctl-*控制 profile（如ctl-double-lock、ctl-defer-submit）分别关掉一条实现规则，必须恰好打破其对应的属性——矩阵的退出码就是契约：任何意外失败、缺失的预期失败或未完成的 cell 都导致非零退出（matrix.py --profiles baseline ctl-defer-submit --topologies keys-only是单跑某两列的快速用法）。
4. 动手实践建议：若你在自己的规格中复刻这套方法论，最小闭环是——先写TypeOK；再写核心安全不变量；为每条不变量准备一个"关掉实现它的代码"的控制开关，证明该行可被证伪；最后用否定式探针证明状态空间确实覆盖了你关心的场景。这正是 invariants.md 中"Common Mistakes"第 3 条（不变量过强）与金丝雀不变量思想的生产级延伸。

从 Baseline.cfg 可以看到一个生产级配置的完整面貌：CONSTANTS区给出拓扑（两个任务、一个命令 entry、两个 key entry、父子关系TaskParent <- <<0, 1>>）与全部 P* 建模开关；INVARIANT区列出九个不变量（TypeOK、Inv_LockerIsFifo、Inv_LockLeads、Inv_OneProspectiveLocker、Inv_AtMostOneLock、Inv_Isolation、RankOK、NoCycle、NoStuck）；PROPERTY Termination单独声明活性属性。这套"安全不变量 + 活性属性 + 公平性 + 覆盖探针 + 控制开关矩阵"的组合，就是 TLA+ 不变量方法论在真实分布式数据库代码库中的完整落地形态。

【免费下载链接】cassandraOpen source transactional distributed database. Linear scalability and proven fault-tolerance on commodity hardware or cloud infrastructure without compromising performance.项目地址: https://gitcode.com/GitHub_Trending/cassa/cassandra