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这套常量分四类理解它就理解了整个配置体系常量组代表常量作用运行范围Sessions、Calls、ClassOf、MaxInvocations、MaxResults界定一次检查的状态空间规模ClassOf决定调用间是否互为等价OneClass或DistinctClasses两个便捷值外部事件AllowRelease、DrainOnRelease、AllowPruneCut分别启用会话释放、服务端 drain 行为TRUE 表示释放被延迟到 handler 来源调用终结、修剪动作可选机制ModelLazy/MaxEvals、ModelPersistence/ImportInit、ModelNestedCalls关闭即把对应动作从状态空间中整体移除让问不相干问题的配置保持小型故障注入FnCanFail、AttachCanFail、LeaseCanFail、ReaderCanCancel、LazyCanFail、DecodeCanFail每个常量启用一个环境可注入的非确定事件配置默认全关除非它的问题需要——这样任何违反都能指向被测机制本身几个配置注释还携带了值得记录的工程信息。例如 CacheLifecycle_lazy.cfg 的注释提到一次性的三调用者穷举运行在合并模型上以 78,792,507 个不同状态通过2026-08-21CI 里保持两个调用者是因为成本不成比例——这是穷举式验证一次性做、常态运行控制在 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正在运行的回调或其关闭后的令牌尾巴会让属主会话免于收集、NoStaleCancelErrorEvaluate 调用者永不返回由另一个等待者造成的取消错误——被取消回调的结果被锁存到其保留的等待者上健康等待者返回继续索取时必须重试而不是失败。导入/冲刷性质DecodeMutualExclusion每个结果至多一个解码在跑——persistDecodeWaitChsingleflight、FlushCleanCapture优雅关闭快照只捕获干净且完全被保留的状态、FlushReferentialIntegrity每个写入结果都归属以某条被写入持久化边为根的完整干净依赖闭包——由 Go 侧闭包遍历snapshotPersistedRootClosureLocked构造性提供import 的显式引用检查在重启时拒绝悬空行、NoLaunderedServe快照时处于打开或附加错误状态的结果永不被导入并对外服务。活性性质对照LiveSpec检查而非普通SpecEventuallyTerminal每个已发起调用最终终结——被服务、失败或被取消永不永久卡死、EvalEventuallyTerminal每个 Evaluate 调用者最终终结、DeferredReleaseEventuallyCompletes一旦某次释放的操作计数静默公平的进度事件最终会消费其清理计划并删除会话记录此性质刻意是条件式的——真正卡死的操作会让 active 保持非零以关闭上下文失败的形式暴露而不是静默快照。活性检查依赖规格第 1884–1972 行精心刻画的公平性约定弱公平只加在系统进度上函数完成、发布链、注销、每个等待者的自身前进步这些对应引擎会跑到完成的 goroutine——没有它们TLC 会把调度器从未运行那个 goroutine误报为真死锁。而Spawn/SpawnNested、所有等待者取消分支、失败注入分支、ReleaseSession与PruneCut均不加公平性它们是可能性而非义务或属于外部事件。规格还记录了两处公平性放置的微妙之处FnComplete的公平保证某个结局而非成功结局公平挂在附加结局的析取上PubFinishOk ∨ PubAttachFailDropHold而非成功臂上——只挂成功臂会错误地禁止持续性失败。运行检查dagger check tla-check:cache-lifecycleREADME 给出的入口是一条 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环境固定。模块在容器里运行 TLCJava 基础镜像为eclipse-temurin:21-jreTLC 发布版被钉在 v1.7.4tla2tools.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 在发现违反时退出码非零模块用... 21 | tee /tmp/out.txt; true吞掉退出码改为解析输出文本判定结果。结果判定runOne第 196–233 行分四种情形期望实际判定通过期望值为输出含No error has been found绿色通过解析出Error: Invariant X is violated.回归被建模的缓存行为或规格本身出了回归违反具名不变量恰好该不变量被违反绿色记录已知发现其他组合干净、或违反了别的不变量配置漂移/无法识别的结果失败信息带上输出尾部顶层CacheLifecycle方法带check标记即dagger check的可发现入口把所有配置名排序后用 goroutine 并行执行失败行汇总排序后返回错误信息指明哪些配置、其结果如何偏离期望并提示每个配置的dagql/tla/注释描述了场景与预期。单独跑一个配置同模块还暴露了One(config, invariant?, define?)方法与检查使用同一固定 jar 和同一调用方式但不施加期望——违反直接原样返回给调用者阅读。两个参数支持不改仓库、隔离追问invariant把配置里的INVARIANTS行替换为单个不变量SPECIFICATION强制为安全性的Spec并丢弃PROPERTY行——一个安全性问题被隔离运行define把一条 TLA 算子定义如ProbeX ...插入规格模块体末尾最后一个终止线之前——例如运行一个预期会被违反的临时可达性探针而不需要编辑仓库文件。为什么这样组织配置即问题、违反即指认这套模型检查体系的设计逻辑可以从 README 与配置注释中读出三层意图状态空间预算。25 个配置各自裁剪规模MaxInvocations 2居多、关闭无关机制、注入最少必要故障使得每个配置都能在 CI 成本内跑完真正的大爆炸半径验证如三调用者穷举以一次性运行 注释记录形式存档在配置头里。违反必须可读。故障注入默认关闭意味着任何违反都指向被测机制每条不变量的 TLA 定义注释都写明了它保护的具体并发契约及其对应的 Go 机制singleflight、lazyEvalComplete、persistDecodeWaitCh、闭包遍历函数名等所以一条Error: Invariant OwnershipExact is violated.可以直接映射到所有权计数的维护代码。回归门而非一次性证明。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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考