antithesis-workload

Antithesis 工作负载

技能版本： 2026-10-21 4f8d80b

用途和目标

实现或改进 Antithesis 工作负载。成功意味着：

• 将 antithesis-research 技能中的属性映射为具体断言，并同时使用属性目录和每个属性的证据文件
• 在 antithesis/test/ 下创建测试命令，以验证正确的行为
• 完成设置后创建首批真实测试模板，或扩展现有模板
• 将分类结果转化为工作负载或属性更新，而不是只停留在隐含结论

首先使用 antithesis-research 技能构建属性目录。使用 antithesis-setup 技能搭建基础设施。使用 antithesis-triage 技能审查运行结果，然后返回此处改进工作负载。如果用户要求提交或启动一次运行，请使用 antithesis-launch 技能——不要直接运行 snouty launch。

前置条件

• 如果 Antithesis 工作草稿（通常位于 antithesis/scratchbook/）不存在，请勿继续。使用 antithesis-research 技能创建它。
• 如果不存在 Antithesis 的 docker-compose.yaml，请勿继续。使用 antithesis-setup 技能创建它。
• 如果未安装 snouty，请勿继续。请参阅 https://raw.githubusercontent.com/antithesishq/snouty/refs/heads/main/README.md 了解安装选项。
• 如果 snouty 版本低于 0.8.0，请勿继续。使用 snouty --version 查看版本，并使用 snouty update 更新。

确定范围

下面的“实现下一个属性”工作流每次只关注一个属性，以便控制上下文规模并保证质量。（分类后的迭代则根据分类结果确定范围。）

如果用户要求处理多个属性，建议一次处理一个——说明随着上下文累积，实现质量会下降，而且每个属性所需的工作量难以预测。询问用户想先从哪个属性开始。如果用户坚持要处理多个属性，则继续执行，但要先提醒用户。

如果用户指定了要处理的属性，则跳过完整目录扫描——但仍须先根据该属性的证据文件评估其状态。如果该属性已经完全实现，告知用户，不要重复处理。

如果用户未指定属性，则运行下面完整的检测和建议流程。

检测实现状态

以下检测工作需要大量上下文（读取每个证据文件，并扫描代码库中的断言）。如果你的 Agent 支持子 Agent，请将此任务委派给子 Agent，并要求其返回每个属性的摘要（状态及简要理由）。这样可以保持主要实现 Agent 的上下文整洁。

检测任务：针对目录中的每个属性，搜索现有测试代码和 SUT 代码中的 Antithesis SDK 断言调用，并与该属性在 antithesis/scratchbook/properties/{slug}.md 中的证据文件交叉核对。评估现有断言是否覆盖证据文件描述的代码路径、失败场景和插桩点。将每个属性归类为：

• 已实现 — 断言覆盖了证据文件描述的内容
• 部分实现 — 存在一些断言，但覆盖不完整
• 未实现 — 未找到相关断言

展示并推荐

读取目录中现有的所有来源信息，并在展示状态时一并说明。使用你找到的字段——架构可能会随时间演进，因此不要把不完整或较旧的来源信息视为错误。用通俗易懂的语言描述现有信息。示例：

• 完整架构：“正在使用目录中的提交 abc12345abcd（2026-05-05），SUT 路径为 /foo，外部引用：A、B。”
• 部分信息：“正在使用目录中的提交 abc12345abcd（2026-05-05）——未记录 SUT 路径或外部引用。”
• 缺失信息：“正在使用目录（未记录来源信息；早于该约定）。”

每个属性周期都会运行工作负载，因此不要每次运行都要求用户重新确认来源信息——将其作为上下文展示，然后继续。如果信息不再符合用户正在使用的系统，用户会主动说明。面向用户展示的提交使用短哈希（前 12 个字符），以提高可读性；frontmatter 中仍存储完整 SHA。

每次只推荐一个属性——不要罗列整个目录。 一个目录可能轻易就有几十或几百个属性，穷举状态清单会让人难以招架，而且很少是用户真正需要的。默认做法是挑选一个，说明原因，然后等待确认。

例外情况是用户明确表示想讨论接下来要做什么，而不是只想听一项推荐。这种情况下，提供高层次概述（按状态统计数量、值得注意的分类、任何异常情况），然后展开讨论。只有在对话需要时，才列出具体属性。

选择推荐项的策略：

• 刚开始时——尚未实现或仅实现了少数属性时——推荐一个简单属性：其测试不涉及太多复杂环节。优先级最高的属性往往需要最多的设置和协调，不适合作为起点。简单属性有助于积累进展，端到端地运行 SDK 和测试框架，让你和用户逐步熟悉工作流。告诉用户你采用了这种策略，并说明原因。
• 进展顺利后——已实现多个属性，且测试框架已通过端到端验证——改为按优先级排序：先处理需要完成的部分实现属性，然后处理与近期已实现属性相关的未实现属性（参见 antithesis/scratchbook/property-relationships.md），再处理其他高优先级的未实现属性。切换策略时告诉用户。

解释你为何选择该属性，并等待用户确认或另选其他属性后再继续。

对于选定的属性，读取目录条目及其证据文件。

其他范围界定问题

仅在遇到无法安全推断的阻碍或范围决策时询问用户，例如：

• 属性目录的位置（如果不是标准路径 antithesis/scratchbook/property-catalog.md）
• 项目语言或 SDK 选择（如果仓库中没有明显线索）
• 分类结果或已知缺口（如果是在迭代现有工作负载）

定义和概念

• SUT： 被测系统。
• 测试模板： 位于 /opt/antithesis/test/v1/{name}/ 的测试命令目录。每条时间线都会运行一个测试模板中的命令。Antithesis 会忽略以 helper_ 为前缀的文件或子目录，因此可用此前缀标记与命令放在一起的辅助脚本。
• 测试命令： 测试模板中带有有效前缀的可执行文件：parallel_driver_、singleton_driver_、serial_driver_、first_、eventually_、finally_、anytime_。
• 时间线： 对 SUT 和工作负载的一次线性执行。Antithesis 会并行运行许多条时间线，并从中分支，以搜索有趣的行为。
• Always / AlwaysOrUnreachable： 用于断言安全性和正确性属性。
• Sometimes(cond)： 用于断言至少应出现一次的活性或非平凡语义状态。
• Reachable / Unreachable： 用于断言是否触发了有意义的结果或被禁止的路径。

文档依据

使用 antithesis-documentation 技能访问这些页面。优先使用 snouty docs。

• 测试命令参考：https://antithesis.com/docs/product/test_templates/test_composer_reference.md
• SDK 参考：https://antithesis.com/docs/reference/sdk.md
• 属性和断言：https://antithesis.com/docs/concepts/properties_assertions/assertions.md
• 故障注入：https://antithesis.com/docs/product/fault_injection.md

参考文件

参考文件	何时阅读
references/component-implementation.md	实现工作负载侧组件或封装器
references/assertions.md	将属性转换为 SDK 断言
references/test-commands.md	编写命令并组织测试模板
references/interesting-values.md	为被测属性选择值菜单
references/iteration.md	分类排查后改进覆盖率和断言

推荐工作流

实现下一个属性

1. 检测实现状态，然后推荐一个属性并说明原因（参见上文“检测实现状态”和“介绍并推荐”）
2. 确认用户要实现哪个属性
3. 阅读 references/component-implementation.md
4. 阅读 references/assertions.md
5. 阅读 references/test-commands.md
6. 阅读 references/interesting-values.md
7. 确定该属性的值菜单——边界值以及已配置限制的值族。发现过程和示例请参见 interesting-values.md
8. 实现所选属性：断言、测试命令和支持代码
9. 将 Sometimes 断言写成工作负载旨在驱动的行为的可达性声明（参见 references/assertions.md 中的“将 Sometimes 断言用作工作负载可达性声明”）。断言前置条件，而不是违规行为。使用 antithesis-launch 运行测试，然后使用 antithesis-triage 检查触发了哪些断言——未触发的断言表明工作负载尚未达到目标，也是开始迭代的起点

分类排查后的迭代

1. 阅读 references/iteration.md
2. 如果需要更改断言，阅读 references/assertions.md
3. 如果需要更改命令覆盖范围，阅读 references/test-commands.md
4. 同时更新工作负载和相关的 Antithesis 工作记录文件

通用指导

• 不要将仅供 Antithesis 使用的代码放入生产路径。如果必须修改共享代码，请确保改动精准且易于隔离。
• 优先使用简单的工作负载代码，而非高度可配置的抽象。
• 设计工作负载时要考虑容错能力。与错误意味着存在缺陷的理想路径测试不同，工作负载会在故障注入和并发活动下运行——瞬时错误是意料之中的情况，并非异常。应朝着目标持续推进，而不是遇到第一个错误就退出。
• 假设 antithesis-setup 已让系统在基本空闲的状态下可以运行；此技能负责系统启动后的工作负载行为。
• 假设 antithesis-setup 已安装相关 SDK，并在 SUT 中添加了一条最简引导断言。此技能负责初始集成检查之外的更广泛属性目录。
• 使用项目所用的语言编写测试命令，而不是 Bash，以便复用项目的客户端、辅助程序和库。

输出

• 为范围内的每项属性添加断言，放在工作负载代码中或经过审慎选择的 SUT 位置
• 将测试命令和配套工作负载代码放在 antithesis/test/ 下
• 当已实现的属性发生变化时，更新 antithesis/scratchbook/property-catalog.md

自我审查

在宣布此技能完成之前，请根据以下标准审查你的工作。如果你的 Agent 支持生成子 Agent，请创建一个全新上下文的 Agent 来执行审查——将此技能文件的路径交给它，并让它读取所有输出产物。全新上下文的审查者能发现上下文内审查容易忽略的问题。如果你的 Agent 不支持子 Agent，请自行审查：重新阅读此文件顶部的成功标准，然后逐项对照以下标准，系统检查实际输出。

• 对于范围内的每项属性，实现都涵盖其证据文件中描述的代码路径、故障场景和检测点，而不仅仅是“存在断言”，而是“断言涵盖了证据所要求的内容”
• 每项断言都使用与属性语义相符的 SDK 断言类型（安全性使用 Always/AlwaysOrUnreachable，活性或有意义的语义状态使用 Sometimes(cond)，路径和结果检查使用 Reachable/Unreachable）
• 应将 Sometimes(true, ...) 断言改写为 Reachable(...)。
• 断言属性名称必须是内联的常量字符串字面量，在整个项目中唯一——绝不能在运行时构造或通过变量传递（静态分析必须预先编录这些名称；参见 references/assertions.md 中的 "Naming"）；不得在多个不相关的调用点复用同一条消息来实现宽泛的属性
• 如果在被测工作负载中加入检测点无法为罕见、危险或对时序敏感的内部状态提供更有价值的搜索指引，则不要只在工作负载中加入检测点，而应在被测系统（SUT）侧进行有针对性的断言
• 工作负载遇到暂时性错误时，应继续朝既定目标推进，而不是在首次失败时就退出
• 工作负载应同时记录已尝试和已确认的操作，以便后续断言检查边界（例如，“计数器的变化量在 [acknowledged, attempted] 范围内”）
• 使用重试时，重试行为必须符合被测系统（SUT）的幂等性约定
• Reachable(...) 标记应附加到不同的结果或分支结果上，而不是在同一条直线流程中过早且冗余地标记路径入口
• 对于测试命令中的有界输入，取值应来自特定属性的值菜单（包括输入类型的边界值，以及该属性代码路径中的配置限制值系列），而不是任意范围；或者，测试命令应说明该菜单维度不适用。参见 interesting-values.md。
• 测试命令应位于 antithesis/test/ 下，并使用有效前缀（parallel_driver_、singleton_driver_、serial_driver_、first_、eventually_、finally_、anytime_）
• 测试命令应使用项目所用的语言编写，而非 Bash，并尽可能复用项目的客户端和库
• 不得让任何测试命令负责发送 Antithesis 生命周期信号；必须在测试命令开始前发出 setup_complete
• 测试模板必须在正确的路径下采用正确结构，以便映射到容器中的 /opt/antithesis/test/v1/{name}/
• 辅助文件或目录必须以 helper_ 为前缀，以便 Antithesis 忽略它们
• 展示状态时，应显示目录中存在的所有来源信息前置元数据，以便用户发现它与自己正在使用的系统是否不匹配
• 更新 antithesis/scratchbook/property-catalog.md，使其反映范围内每项属性的实现状态；来源信息前置元数据应反映当前代码库状态（刷新 commit 和 updated；保留现有目录中的 sut_path 和 external_references）。前置元数据格式定义于 antithesis-research 技能的 references/scratchbook-setup.md。
• 对于工作负载旨在驱动的行为，应存在作为可达性声明的 Sometimes 断言，并将测试运行中未触发的可达性声明用作迭代信号（参见 references/assertions.md 中的 "Sometimes Assertions as Workload Reach Claims"）
• 不得在同一位置将可达性声明设为 Always 或 AlwaysOrUnreachable 的否定；系统正确运行时，每项可达性声明仍须触发（参见 references/assertions.md 中的 "A Reach Claim Asserts The Precondition, Never The Violation"）
• 断言应位于工作负载代码或经过精确选择的被测系统（SUT）位置，而不是散布在生产代码路径中
• 对 antithesis/config 使用 snouty validate，确保 compose 配置能够到达 setup complete，并且所有已配置的测试模板都能正常工作。运行 validate 前，务必先构建最新镜像。