企业官网建设流程全解析

Dagger dagql 缓存并发内核的 TLA+ 模型检查：从 CacheLifecycle.tla 到 dagger check tla-check:cache-lifecycle

【免费下载链接】daggerAutomation engine to build, test and ship any codebase. Runs locally, in CI, or directly in the cloud项目地址: https://gitcode.com/GitHub_Trending/da/dagger

本文围绕 dagql/tla/README.md 展开，介绍 Dagger 引擎中 dagql 结果缓存（GetOrInitCall）的并发内核如何被翻译成一份 TLA+ 规格说明，并通过 TLC 模型检查器做回归验证。读完后，你将掌握：这份模型到底对哪些 Go 代码做了形式化抽象、每个.cfg配置如何圈定一个可独立回答的并发问题、如何运行检查命令，以及当缓存实现出现回归时模型检查会如何精确指认问题所在。

模型检查的是什么：dagql 缓存的结果生命周期

Dagger 引擎的核心执行路径是GetOrInitCall：一次调用从缓存查询开始，命中则复用已有结果，未命中则执行函数并把结果发布回缓存供后续等价调用共享。这个过程中会交织大量并发参与者——在途调用去重、结果发布、所有权计数、释放级联、读路径上的依赖附加屏障、会话释放与持久化边修剪、懒求值、持久化导入/解码/冲刷/重启，以及从脱离的调用执行器（detached call executor）内部发起的嵌套调用。

dagql/tla/CacheLifecycle.tla 的模块头（第 2–59 行）给出了建模边界的完整声明，模型覆盖：

• 缓存查询、命中与未命中；
• 在途调用去重（对应Cache.ongoingCalls的 singleflight 语义）；
• 结果发布（initCompletedResult的两个分支）；
• 所有权计数与释放级联（release cascade）；
• 读路径上的依赖附加屏障（dependency-attachment barrier）；
• 会话释放（ReleaseSession）与持久化边修剪；
• 懒求值（Cache.Evaluate，由ModelLazy常量开关）；
• 持久化解码、导入、冲刷、重启（由ModelPersistence控制）；
• 从调用执行器内部发起的嵌套调用——它们不被服务端的 drain（排空）计数，也不会被其拒绝（ModelNestedCalls）；
• 每会话操作计数：对释放墓碑（release tombstone）的准入检查、返回边界的迟到拒绝、由最后退出操作者兜底的延迟释放清理、懒回调尝试令牌、以及关闭静默（Cache.Close）。

规格是自包含的（self-contained）：头部解释建模规则，每个动作的注释都会写明它建模的是哪段 Go 代码，被建模的主实现位于 dagql/cache.go 及其同族文件（如持久化导入路径 dagql/cache_persistence_import.go）。

建模规则：粒度、抽象与刻意的过度近似

规格头中的GRANULARITY与ABSTRACTIONS小节定义了模型的三个关键约定，理解它们才能正确解读检查结果：

粒度：一个模型动作 = 一个 Go 临界区。每个原子模型动作代表一个 Go 临界区（critical section）或一次无锁原子迁移，竞态只存在于这些动作之间。

抽象一：等价类是静态划分。常量ClassOf是一张查找表，声明每个调用身份（recipe digest）属于哪个等价类；同类调用的结果在缓存命中时可互换。e-graph 的类合并机制本身没有被建模。规格同时声明了一条只假设、不验证的公理（MODEL AXIOM）：缓存认为等价的结果可以互换。

抽象二：查询可能"假性未命中"。即使候选结果存在，模型也允许查询未命中。这是对该规格未建模的候选/会话过滤逻辑的过度近似（over-approximation），并且恰好压测了引擎已经接受的一个重复执行窗口——规格注释指向 dagql/cache.go 的第 3889–3893 行。

明确不建模的部分（规格头逐条列出，并说明由 Go 测试覆盖）：

• 会话资源、TTL/过期、DoNotCache、recipe-replay 污点，以及任意值缓存（acquireSessionArbitraryLocked，与已建模的结果占位遵循同一"原子记录并计数"契约）；
• e-graph 变更辅助函数中的锁时长注册守卫（TeachCallEquivalentToResult、TeachContentDigest、AddExplicitDependency、WithSessionResourceHandle）。由于数值结果 ID 在引擎生命周期内唯一，这些守卫只对已收集的结果拒绝变更；
• 一个值得注意的对称性说明：每个被建模的缓存操作都带会话元数据，而实现里在元数据缺失时还会使用一个缓存级的操作计数；关闭逻辑把两种计数同等对待，所以模型用单一计数即可覆盖两种情况。

配置矩阵：一个 .cfg 只回答一个问题

规格定义了全部机制，但"哪些机制启用、哪些外部事件可以发生"由 25 个CacheLifecycle_*.cfg配置文件选择——README 中强调的关键设计原则是：配置只选择场景，绝不选择替代实现（"Configurations select scenarios: which machinery is active and which external events and failures can happen. They never select alternative implementations."）。

每个.cfg文件顶部注释说明两个信息：该配置在问什么问题，以及运行预期通过还是预期违反某一条具名不变量。当前 25 个配置全部是绿色回归门（green regression gates）——预期违反只保留给刻意接受的模型发现，当前配置集中不存在任何预期失败的配置。

以一个典型配置为例，CacheLifecycle_core.cfg：

\* The core kernel with no external events and no injected failures: two \* sessions, two calls, every safety property. Expected: pass. SPECIFICATION Spec CONSTANTS Sessions = {s1, s2} ... Calls = {cA, cB} ... ClassOf <- OneClass MaxInvocations = 2 MaxResults = 2 AllowRelease = FALSE DrainOnRelease = FALSE AllowPruneCut = FALSE ModelLazy = FALSE MaxEvals = 0 ModelPersistence = FALSE ImportInit = FALSE ModelNestedCalls = FALSE FnCanFail = FALSE AttachCanFail = FALSE LeaseCanFail = FALSE ReaderCanCancel = FALSE LazyCanFail = FALSE DecodeCanFail = FALSE SYMMETRY Symm INVARIANTS TypeOK OwnershipExact NoUnderflow NoResurrection ReturnedLive ReturnedOwned NoHalfAttachedRead PersistableIntentDurable NoSpuriousErrors NoOrphanEdgesAtQuiescence

这套常量分四类，理解它就理解了整个配置体系：

几个配置注释还携带了值得记录的工程信息。例如 CacheLifecycle_lazy.cfg 的注释提到：一次性的三调用者穷举运行在合并模型上以 78,792,507 个不同状态通过（2026-08-21），CI 里保持两个调用者是因为成本不成比例——这是"穷举式验证一次性做、常态运行控制在 CI 成本内"的取舍记录。

状态空间裁剪还利用了规格中声明的对称性：会话之间、调用之间相互可互换，Symm == Permutations(Sessions) ∪ Permutations(Calls)允许 TLC 跳过仅靠改名差异的状态。规格头特别注明只用于安全性配置：TLC 的对称化削减对活性性质会给出错误结果。

不变量：每条都锚定一条可观测的并发契约

规格尾部（第 1976 行起）按主题组织全部性质，且明确说明为什么每个.cfg只检查性质子集："在每个配置里检查每个性质会把独立的问题搅在一起：一个场景里注入的某类故障，会用无关性质的违反淹没正在测试的性质。"

核心安全性不变量（每个都是可独立引用的并发契约）：

• TypeOK：基本形态健全性——长度不超过上界、计数非负、"每条被计数的边都有对应记录"、sessionRelease各阶段字段自洽（如phase = "deferred" => active > 0）。
• OwnershipExact：所有权计数精确——每个已注册结果的增量维护计数own恒等于其边集合的重新计数（被计数的会话边 + 依赖父节点 + 交接保留 + 持久化边）。
• NoUnderflow：所有权计数永不为负；NoResurrection：已收集（OnRelease钩子已跑）的结果永不重新注册回缓存。
• ReturnedLive/ReturnedOwned/NoHalfAttachedRead：调用完成时，返回的结果仍然存活；返回瞬间调用会话的边已记录且结果已固定（不会从调用者脚下消失）；没有读者会拿到依赖附加尚未干净收尾的结果。
• PersistableIntentDurable：持久化意图永不丢失——成功调用的准入关闭且交接保留释放后，被准入的可持久化请求蕴含持久化边存在，包括被拒绝或取消的最后一个等待者（因为最终交接先提交边）。
• LeaseFailureClean、NoSpuriousErrors：操作租约失败必须在任何在途调用/结果/所有权边发布之前终止；且没有启用任何故障注入时，竞态本身永远不会"制造"执行失败。
• NoOrphanEdgesAtQuiescence：所有会话释放且一切活动静止后，不允许残留任何会话所有权边。
• RefusedOnlyAfterRelease：被拒绝的认领必须由会话墓碑解释——这是嵌套调用穿过 drain 场景（CacheLifecycle_drain_escape.cfg 等）的核心断言。
• 毒化相关：NoRetainedPoisonedEntry（附加失败永不获得持久化边）、NoErroredLookupSelection（选择时标记区分"在附加错误后发起的非法查询"与"选择时屏障尚开、附加之后才失败"的合法查询）。

懒求值性质逐条对应 Go 代码中lazyMu协调的契约：LazyMutualExclusion（每个结果至多一个回调在跑——evaluateOne的每结果 singleflight）、EvalDoneComplete（成功的Evaluate返回蕴含求值完成；注释点明修复前的快速路径曾在此违反：在回调的缓存侧簿记仍在运行时就信任已消费的对象侧回调而提前报告成功）、LazyCompleteSettled（完成只在与所有阶段都结算时记录）、LazySuccessPermanent（成功是永久的，回调被清除且每个启动路径先检查lazyEvalComplete）、LazyAttemptDefersCollection（正在运行的回调或其关闭后的令牌尾巴会让属主会话免于收集）、NoStaleCancelError（Evaluate 调用者永不返回由另一个等待者造成的取消错误——被取消回调的结果被锁存到其保留的等待者上，健康等待者返回继续索取时必须重试而不是失败）。

导入/冲刷性质：DecodeMutualExclusion（每个结果至多一个解码在跑——persistDecodeWaitChsingleflight）、FlushCleanCapture（优雅关闭快照只捕获干净且完全被保留的状态）、FlushReferentialIntegrity（每个写入结果都归属以某条被写入持久化边为根的完整干净依赖闭包——由 Go 侧闭包遍历snapshotPersistedRootClosureLocked构造性提供，import 的显式引用检查在重启时拒绝悬空行）、NoLaunderedServe（快照时处于打开或附加错误状态的结果永不被导入并对外服务）。

活性性质（对照LiveSpec检查，而非普通Spec）：EventuallyTerminal（每个已发起调用最终终结——被服务、失败或被取消，永不永久卡死）、EvalEventuallyTerminal（每个 Evaluate 调用者最终终结）、DeferredReleaseEventuallyCompletes（一旦某次释放的操作计数静默，公平的进度事件最终会消费其清理计划并删除会话记录；此性质刻意是条件式的——真正卡死的操作会让 active 保持非零，以关闭上下文失败的形式暴露，而不是静默快照）。

活性检查依赖规格第 1884–1972 行精心刻画的公平性约定：弱公平只加在"系统进度"上（函数完成、发布链、注销、每个等待者的自身前进步），这些对应引擎会跑到完成的 goroutine——没有它们，TLC 会把"调度器从未运行那个 goroutine"误报为真死锁。而Spawn/SpawnNested、所有等待者取消分支、失败注入分支、ReleaseSession与PruneCut均不加公平性：它们是可能性而非义务，或属于外部事件。规格还记录了两处公平性放置的微妙之处：FnComplete的公平保证"某个结局"而非"成功结局"；公平挂在附加结局的析取上（PubFinishOk ∨ PubAttachFailDropHold）而非成功臂上——只挂成功臂会错误地禁止持续性失败。

运行检查：dagger check tla-check:cache-lifecycle

README 给出的入口是一条 DAG 检查命令：

dagger check tla-check:cache-lifecycle

它并行运行全部配置，并把每个配置的实际结果与 .dagger/modules/tla-check/main.go 中的expectedOutcome映射表比对；新增配置必须同步加入该映射表，否则不会被检查。该模块在 dagger.toml 中注册为[modules.tla-check]（源.dagger/modules/tla-check）。

检查的实现细节在 .dagger/modules/tla-check/main.go：

环境固定。模块在容器里运行 TLC，Java 基础镜像为eclipse-temurin:21-jre，TLC 发布版被钉在 v1.7.4（tla2tools.jar），并且以 SHA256 校验和（936a26...e88）验证 jar 完整性后挂载dagql/tla规格目录——注释说明这是为了让本地与 CI 运行完全一致。

执行命令。每个配置都跑：

java -XX:+UseParallelGC -cp /tla2tools.jar tlc2.TLC -workers auto -deadlock \ -config CacheLifecycle_<name>.cfg CacheLifecycle.tla

-workers auto让 TLC 自动并行化，-deadlock额外检查死锁。由于 TLC 在发现违反时退出码非零，模块用... 2>&1 | tee /tmp/out.txt; true吞掉退出码，改为解析输出文本判定结果。

结果判定（runOne，第 196–233 行）分四种情形：

顶层CacheLifecycle方法（带+check标记，即dagger check的可发现入口）把所有配置名排序后用 goroutine 并行执行，失败行汇总排序后返回，错误信息指明"哪些配置、其结果如何偏离期望"，并提示每个配置的dagql/tla/注释描述了场景与预期。

单独跑一个配置：同模块还暴露了One(config, invariant?, define?)方法，与检查使用同一固定 jar 和同一调用方式，但不施加期望——违反直接原样返回给调用者阅读。两个参数支持"不改仓库、隔离追问"：

• invariant：把配置里的INVARIANTS行替换为单个不变量，SPECIFICATION强制为安全性的Spec，并丢弃PROPERTY行——一个安全性问题被隔离运行；
• define：把一条 TLA+ 算子定义（如ProbeX == ...）插入规格模块体末尾（最后一个====终止线之前）——例如运行一个"预期会被违反"的临时可达性探针，而不需要编辑仓库文件。

为什么这样组织：配置即问题、违反即指认

这套模型检查体系的设计逻辑可以从 README 与配置注释中读出三层意图：

1. 状态空间预算。25 个配置各自裁剪规模（MaxInvocations = 2居多）、关闭无关机制、注入最少必要故障，使得每个配置都能在 CI 成本内跑完；真正的大爆炸半径验证（如三调用者穷举）以一次性运行 + 注释记录形式存档在配置头里。
2. 违反必须可读。故障注入默认关闭意味着任何违反都指向被测机制；每条不变量的 TLA+ 定义注释都写明了它保护的具体并发契约及其对应的 Go 机制（singleflight、lazyEvalComplete、persistDecodeWaitCh、闭包遍历函数名等），所以一条Error: Invariant OwnershipExact is violated.可以直接映射到所有权计数的维护代码。
3. 回归门而非一次性证明。expectedOutcome当前 25 项全绿，检查是常态化的回归防线：改动 dagql/cache.go 一族的并发逻辑后重跑dagger check tla-check:cache-lifecycle，若某个原本绿色的配置开始违反其不变量，即提示被建模行为或规格需要重新核对。

规格与检查器的配合关系可以概括为一条闭环：CacheLifecycle.tla定义"引擎承诺了什么"，.cfg文件定义"这次问什么"，expectedOutcome映射表定义"答案必须是什么"，而One方法提供了对规格追问的逃生通道——整个目录只读地放在 dagql/tla/ 中，任何人都可以在本地复现相同的检查。

【免费下载链接】daggerAutomation engine to build, test and ship any codebase. Runs locally, in CI, or directly in the cloud项目地址: https://gitcode.com/GitHub_Trending/da/dagger