大规模有状态服务的高保真模型（OSDI 2026）
原题：High Fidelity Models for Large Scale Stateful Services (Operational Systems)
一句话总结：S3 面对超过 500 万亿对象、每秒超过 2 亿请求和持续重写时，作者用可执行参考模型、谓词抽象和状态感知的系统测试，把不可枚举的请求—状态空间压缩为可度量的抽象场景；该工具已在 CI/CD 中阻止超过 300 个潜在回归。
问题与动机
S3 的 API 已演化二十年，包含 96 个操作、众多可选参数、对象元数据和桶配置。实现可能用不同代码库、语言和硬件重写，但客户依赖成功响应、错误码、响应头和错误优先级的稳定行为。仅靠单元测试和人工集成测试，难以说明覆盖了哪些行为。
论文将问题定义为 API sameness：在实现演进或出现第二个实现时，验证可观察的顺序输入输出行为保持一致。作者聚焦单请求顺序执行；一致性、并发和性能不在范围内。
关键观察 / 隐含假设
- 观察 1：请求参数与服务状态的组合呈指数增长。 GetObject 有 21 个输入参数，论文估计至少存在
10^25个质性不同的请求—状态组合（§1）。- 依赖假设：同一特征等价类中的值会产生相同的可观察行为。
- 可能失效场景：未被谓词表达的值（例如特殊对象大小或内部路径触发值）仍可能改变实现路径。
- 观察 2：错误通常短路，但错误检查顺序本身也是兼容性的一部分。 0-error、1-error 和 2-error 场景分别覆盖成功行为、单错误行为和错误优先级（§5.2）。
- 依赖假设：SUT 遵循 first-error hypothesis；三个及以上错误不会暴露新的行为。
- 可能失效场景：实现累积多个错误、执行副作用后才报错，或错误顺序依赖未建模的运行时条件。
- 假设 1：参考模型可以成为正确性判定标准。 模型由工程师维护，且模型错误与 SUT 错误都可能导致 deviation；论文未给出独立规格证明。
- 证据强度：中。模型已在真实 S3 流程中发现问题，但其正确性主要依赖持续审阅和与既有行为的交叉验证。
- 假设 2：顺序行为足以覆盖本文目标。 模型是内存中、单线程且不反映延迟和吞吐的状态机（§2.1）。
- 证据强度：强。作者明确把并发一致性留给专门机制处理，但这限制了结论范围。
核心方法
系统把 SUT、可执行模型、响应验证器和请求生成器组成模型测试流程（图 1）。每个请求先执行于 SUT，再把响应中的不可预测字段作为 prophecy 值输入模型。像 request ID、时间戳这类字段可按格式检查；ETag 等会影响后续条件请求的字段则被写回模型状态。
作者用谓词抽象把请求特征和可观察状态特征划分为类别。例如桶名分为语法无效、合法但不存在、合法且存在；对象是否存在、版本是否存在则是状态谓词。SAT all-sat 引擎枚举满足状态不变量和测试配置的抽象场景，避免枚举具体字符串与全部状态组合（§4–§5.1）。
API-planner 根据场景需要的目标状态合成前置操作。例如测试存在对象的 GetObject 前，先生成 CreateBucket 和 PutObject，并把这些操作也放入同一模型—SUT 验证流程。随后从模型状态查询满足类别的具体桶名、键名和参数，执行目标请求（§5.3）。
测试配置允许按相关特征分组，并限制 num_errors。开发者可针对正在修改的路径选择场景组合；异步任务再轮换未覆盖的组合。这是在可接受 CI 时间内换取覆盖广度的工程折中（§5.4）。
设计取舍
- 完整响应比较换取强 oracle：比较响应的每个元素，能发现弱断言遗漏的错误；代价是模型必须精确描述大量字段，并正确区分 prophecy。
- 黑盒模型换取实现独立性：模型不依赖 SUT 内部结构，适合重写和多实现；代价是无法区分具有相同输入输出行为的内部状态，如缓存状态（§2.1）。
- 谓词由工程师维护换取可控预算：谓词可覆盖不可观察但值得测试的实现路径；代价是抽象设计和模型维护仍是人工负担。
- 跳过高阶错误组合换取 CI 可行性：在 first-error 假设下重点测试至多两个错误；该假设若不成立，覆盖结论会变弱。
实验与结果
- S3 Express One Zone 发布前发现并阻止 171 个 deviation，其中 12 个为高严重度问题；修复后才上线（§6）。
- S3 前端重写项目的 CI/CD 发现 92 个其他单元和集成测试漏掉的问题，均在生产部署前修复（§6）。
- 持续 S3 CI/CD 检查至今发现 109 个 deviation，其中 24 个为高严重度问题；三项工作合计超过 300 个潜在回归（表 3、§6）。
- 每个 validation campaign 预算约 3 小时，可执行约 432,000 个请求；Ranges 特征组约含 212,400 个场景，约 1.5 小时执行完（§6.1，表 6）。
- 在 28,457 个 property-based testing 请求中，仅覆盖 9,040 个唯一场景，重复请求 19,417 个。针对 3 个特征的 8 个场景，随机测试平均需 3,200 个请求，而系统生成器直接生成 8 个请求（§6.2）。
论断—证据表
| 论断 | 证据 | 评测边界 | 置信度 |
|---|---|---|---|
| 抽象场景能在有限预算内覆盖大量可观察行为 | 约 432,000 请求/3 小时；Ranges 组 212,400 请求/1.5 小时（§6.1，表 6） | S3 GetObject，工程师指定的特征分组和类别 | 强 |
| 模型测试能发现传统测试漏掉的回归 | 重写项目发现 92 个问题；线上持续流程发现 109 个问题（表 3） | S3 真实 CI/CD，问题数依赖人工分类和部署项目 | 强 |
| 系统生成器比随机 PBT 更少重复 | 28,457 次请求只得 9,040 个唯一场景；8 场景对比为 3,200 次随机请求 vs 8 次系统生成 | 主要是 GetObject；不能直接外推全部 S3 API | 中 |
| 该模型可支持不同实现的兼容性验证 | Express One Zone 发布前阻止 171 个 deviation（§6） | 严格兼容 regional S3 的 API，允许有意偏差 | 中 |
批判性分析
论证链条
从“客户依赖完整可观察行为”到“用模型作为 oracle，再系统枚举抽象场景”的链条是闭合的。工程结果也说明方法能进入真实发布流程。论文没有证明谓词抽象对所有 S3 行为都 adequate；其覆盖是相对于人工定义的谓词集合，而不是整个 API 语义空间。
假设压力测试
first-error 假设是主要压力点。若某 API 的校验并非短路，或错误产生副作用，2-error 截止策略可能漏掉行为。谓词等价类也可能把极少数边界值错误合并。对象大小、时间、加密配置和权限组合虽然可加入抽象，但论文没有给出谓词遗漏的系统性测量。
实验可信度
实验同时包含真实 S3 项目结果、请求预算和与 PBT 的受控比较。PBT 对比清楚展示重复率，但只覆盖 GetObject，且没有报告两种方法的完整运行成本、并发配置和失败诊断质量。问题数量证明了实用价值，却不能单独证明模型对未触发场景的正确性。
系统性缺陷
模型和谓词需要随 API 演进维护，模型错误可能产生误报或漏报。API-planner 还依赖写操作与模型一致；状态设置失败会使目标场景无法执行。论文未讨论模型服务本身的故障恢复、测试账号和数据隔离成本，也未量化请求对被测环境的负载影响。黑盒方法不能观察缓存、内部副本或并发调度状态。
局限与后续工作
- 局限 1：核心谓词目前由工程师手工定义，维护成本随 API 特征和实现路径增长。
- 局限 2：模型只覆盖顺序、单线程、功能性输入输出行为，不覆盖并发一致性、性能 SLO 和持久化故障。
- 后续工作 1：作者计划从服务交互和源代码中学习或挖掘谓词，减少抽象维护工作（§8）。
- 后续工作 2：应在真实生产 trace 上测量谓词遗漏率，并对不满足 first-error 假设的 API 做独立覆盖验证。
- 后续工作 3：将状态模型扩展到故障、并发和恢复场景，检验模型 oracle 是否仍能区分可接受的非确定性。