Verification Checklist【免费下载链接】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/cassandraState MappingVariable X in spec → field Y in codeType constraints match (spec range ⊆ code type range)Action MappingAction A in spec → method M in codePrecondition (await/guard) correctly checkedState update matchesAtomicity level matchesAll UNCHANGED variables truly unchangedInvariant MappingTypeInvariant → type system assertionsSafetyInvariant → defensive checks / testsLiveness → timeout / retry / monitoringEdge CasesEmpty collections handled (spec:\A x \in {}: TRUE)Concurrent access protectedError/exception paths modeled把规约性质映射到工程手段是这条清单的精华**类型不变量对应类型系统与断言安全不变量对应防御性检查与测试活性对应超时/重试/监控**。每种性质在代码侧都有不同的落地载体。 ## 使用规约在代码中定位 Bug ### Step 1编写最小规约 **只聚焦疑似出问题的区域**不需要建模整个系统。这个原则在 Accord 规约工程中有直接体现——formalise/accord/execution 被拆成两层 一个引理每层只假设其下一层 | 层 | 模块 | 假设 | 建立 | |---|------|------|------| | 排序 | AccordExec.tla | 就绪信号正确G1/G2 | 证书与调度规则在可达状态中成立 | | 通知 | AccordNotify.tla | AccordExec 的区域分配与队列顺序 | G1 可靠性、G2 无丢失唤醒、G3 集合纪律、G4 有界投递、L3 | | 引理 | AccordAcyclic.lean | 秩证书 六条隔离调度规则 | 任意规模下的无环、无卡死、隔离 | ### Step 2用小常量运行CONSTANT NumNodes 3 MaxMsgs 5 NULL NULLTLC 是**穷举**模型检查器小状态空间完全足够。仓库的 Accord 模型就在 2–4 个任务、2–4 个条目上运行规模无关的部分交给 Lean 证明AccordAcyclic.lean 证明秩证书蕴含无环对任意任务数成立TLC 只负责证明证书在每个可达状态都成立——这正是 [README.md](https://link.gitcode.com/i/2e73d702c6c4e330490311f0e9378b54) 中证书 ⇒ 无环任意规模Lean 完成与证书在可达状态成立2–4 任务TLC 完成的分工设计。 ### Step 3观察这些症状 | TLC 反馈 | 可能的代码 Bug | |----------|---------------| | 死锁Deadlock | 缺失唤醒、锁顺序问题 | | 违反不变量Invariant violated | 逻辑错误、缺失检查 | | 违反活性Liveness violated | 饿死、缺失公平性、活锁 | | 状态空间爆炸 | 模型过细——需要进一步抽象 | | 断言失败Assert failed | 到达不可能状态——逻辑错误 | 仓库 [SKILL.md](https://link.gitcode.com/i/4aeddadbd8f08a11ed0c4a01312caccc) 补充了 TLC 输出的解读范式 - **成功**Model checking completed. No error has been found. - **不变量违反**Error: Invariant SafetyInvariant is violated. 状态序列反例State 1 → State 2变更值标红 - **死锁**Error: Deadlock reached. —— 检查 await 条件和进程完成逻辑 - **活性违反**Error: Temporal properties were violated. —— 检查公平性设置可能需要 WF_vars 或 SF_vars反例可能带 stuttering 后缀。 ### Step 4把错误轨迹翻译回代码路径 TLC 给出的是一步一步的状态序列——一个**具体的反例concrete counterexample**。逐状态映射到代码状态导致违反的那条转换就是 bug 位置。仓库 [README.md](https://link.gitcode.com/i/2e73d702c6c4e330490311f0e9378b54) 对反例的使用更进一步每个测试单元还报告**覆盖探针coverage probes**是否被真正到达——绿灯但模型从未持锁视为未检查的行且负面控制ctl-* 配置**必须**破坏对应性质缺失的失败与意外的失败同样算错EXPECT_FAIL 机制这防止了控制配置静默失效这一整套方案最想防住的失效模式。 ## 为已有协议建模 验证已知协议Raft、Paxos、2PC 等的实现时对应原文档 Modeling Existing Protocols 1. 从论文的伪代码或描述出发 2. **一次只建一步**每加一步就检查一次 3. 尽量使用与论文**相同的变量名** 4. 从论文的正确性声明中写出不变量 5. 先用小常量运行再逐步增大。 ### 界定模型规模 真实系统的状态是无界的TLA 模型必须是有限的。原文档给出的界约束示例完整保留 tla CONSTANTS MaxTerm 3 \* bound election terms MaxLogLen 4 \* bound log length MaxMsgs 10 \* bound messages in flight \* Use as state constraint in .cfg: \* CONSTRAINT StateConstraint StateConstraint /\ \A n \in Nodes: term[n] MaxTerm /\ \A n \in Nodes: Len(log[n]) MaxLogLen /\ Cardinality(msgs) MaxMsgs在.cfg中启用CONSTRAINT StateConstraint即可把状态空间限制在有限范围内。AccordExec的界约束设计同样值得参考模型用小常量跑可达性而把任意规模成立的部分交给AccordAcyclic.lean——该 Lean 文件证明了waitEdges_iff_rankOK四个WaitEdges假设等价于 TLC 检查的单个RankOK不变量从而一次 TLC 检查同时兑现了 Lean 定理的四个前提。这种TLC 证明可达性 证明助手证明规模无关性的组合正是 README.md 所阐述的核心方法论。完整工具链从规约到 TLC 运行仓库的 tla-plus 技能库提供了一套开箱即用的脚本首次使用先运行bash .claude/skills/tla-plus/scripts/setup.sh下载tla2tools.jarv1.8.0 并校验 Java 11# 一键完成翻译 PlusCal如有→ SANY 解析 → TLC 模型检查 bash .claude/skills/tla-plus/scripts/check.sh spec.tla --config spec.cfg # 分步工具 bash .claude/skills/tla-plus/scripts/parse.sh spec.tla # 仅语法检查 bash .claude/skills/tla-plus/scripts/translate.sh spec.tla -nocfg # PlusCal → TLA bash .claude/skills/tla-plus/scripts/tlc.sh spec.tla --config spec.cfg --workers auto bash .claude/skills/tla-plus/scripts/tlc.sh spec.tla --no-deadlock # 抑制死锁检查每个规约都需要一个.cfg文件配置示例同样来自 SKILL.mdSPECIFICATION Spec \* Properties to check INVARIANT TypeInvariant INVARIANT Safety \* Uncomment for liveness (slower) \* PROPERTY Liveness \* Constants CONSTANT NumNodes 3 MaxMsgs 5 NULL NULL \* Uncomment to bound state space \* CONSTRAINT StateConstraint \* Uncomment to ignore deadlocks \* CHECK_DEADLOCK FALSE【免费下载链接】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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考