企业官网建设流程全解析

Quickwit Simulation-First 开发工作流：从 TLA+ 规范到确定性模拟测试的强制验证流程

【免费下载链接】quickwitCloud-native OSS search engine for observability项目地址: https://gitcode.com/GitHub_Trending/qu/quickwit

本文基于 Quickwit 仓库中的 docs/internals/SIMULATION_FIRST_WORKFLOW.md 展开，系统讲解 Quickwit 团队为所有开发工作制定的强制性"先模拟、后实现"工作流：以验证金字塔为骨架，在写任何业务代码之前先阅读 TLA+ 规范、先编写确定性模拟（DST）测试，再逐层完成实现与验证。读完本文，你将掌握 Quickwit 的五个开发阶段、验证金字塔每一层的作用与命令、DST 测试的编写范式，以及这套工作流在quickwit-dst仓库中的真实落地形态。

验证金字塔：六层验证体系

SIMULATION_FIRST_WORKFLOW.md开篇定义了 Quickwit 开发工作流的哲学基础——验证金字塔（Verification Pyramid）。它把整个验证体系自底向上组织为六层，越靠近塔尖，验证越"形式化"、越昂贵；越靠近塔底，反馈越快速、越频繁：

^ /|\ / | \ / | \ TLA+ Specs (docs/internals/specs/tla/) / | \ - Mathematical model /----+----\ - Defines "what is correct" / | \ / | \ Stateright Models / | \ - Rust-native model checking /--------+--------\- Verifies state space / | \ / | \ DST Tests / | \- Deterministic simulation /------------+------------\- Fault injection / | \ / | \ Unit/Integration Tests / | \- Fast feedback /----------------+----------------\ / | \ / | \ Production Monitoring /-------------------+-------------------\- production invariant metrics

各层职责与仓库中的对应物如下：

值得强调的是：验证金字塔并不是六套互不相干的工具。在 Quickwit 的架构中，同一组不变量在 TLA+ 规范、Stateright 模型、DST 测试与生产代码之间共享同一份定义（详见后文"共享不变量"一节），这正是 docs/internals/VERIFICATION.md 所称的"单一事实来源"（single source of truth）。

强制工作流：写代码之前的五个阶段

该文档明确声明：这个工作流对 Quickwit 所有开发是强制性的（mandatory）。它把一次功能开发拆成五个阶段，且顺序不可协商。

Phase 1：先写规范（任何代码之前）

写代码之前，先做两件事：

1. 检查已有的 TLA+ 规范（位于docs/internals/specs/tla/）：若存在，则审阅其中与本次改动相关的不变量（invariants）；若不存在且本次是重要功能，则为它编写一份规范。
2. 检查已有的 Stateright 模型：若存在，则理解其状态机与属性；若不存在，评估是否需要模型检查。

从仓库现状看，这一阶段并非空谈。当前 docs/internals/specs/tla/ 目录下已存在四份正式规范及其配置：

Phase 2：先写测试（仍然没有实现）

第二阶段是 simulation-first 工作流的核心：在实现存在之前，先把不变量编码成可执行的 DST 测试。文档给出了标准骨架：

#[test] fn test_feature_invariant_holds() { let config = SimConfig::new(SEED); let mut sim = Simulation::new(config); sim.run(|env| async move { // Setup let component = create_component(); // Exercise (with fault injection) for _ in 0..iterations { perform_operation(&component).await?; } // Verify invariants from TLA+ spec verify_invariant_1(&component)?; // Maps to TLA+ line X verify_invariant_2(&component)?; // Maps to TLA+ line Y Ok(()) }); }

随后运行测试，预期结果是失败：

cargo test -p quickwit-dst -- your_feature_tests # Should fail: component doesn't exist yet

这一"预期失败"是整个工作流的信号装置：它证明测试确实锚定了尚不存在的行为，而不是一个永远通过的摆设。对应的运行环境为quickwit-dstcrate（见 Cargo.toml，其 description 即为 "Deterministic simulation testing and stateright model checking for Quickwit"）。

Phase 3：实现（让测试通过）

在 DST 测试就位并确认失败后，才进入实现阶段：

5. 编写最小实现使 DST 测试通过；同时为与 TLA+ 属性对应的不变量添加debug_assert!。

6. 遵循仓库编码风格：CODE_STYLE.md 与 RUST_STYLE.md。

7. 再次运行测试，预期通过：

cargo test -p quickwit-dst -- your_feature_tests # Should pass now

Phase 4：验证所有层级

实现通过 DST 测试后，逐层向上验证：

# 7. Run Stateright model (if applicable) cargo test -p quickwit-dst -- stateright_your_feature # 8. Run unit tests cargo nextest run -p your-crate -- your_feature # 9. Run integration tests # Rust integration tests cargo nextest run -p quickwit-integration-tests # REST API tests (if touching API surface) cd rest-api-tests && ./run_tests.py --engine quickwit # 10. Full verification cargo nextest run --all-features cargo clippy --workspace --all-features --tests

其中cargo nextest run --all-features与cargo clippy --workspace --all-features --tests是提交前的全量闸门。

Phase 5：只有全部验证通过才提 PR

11. 创建 PR 并附上验证证据：

• DST 测试结果；
• Stateright 探索统计（如适用）；
• 对应的 TLA+ 规范链接（如适用）；
• 集成测试结果。

实战对照：添加一个功能的 Bad 与 Good

文档用一个鲜明的对比说明工作流的价值：

错误示范（不要这样做）

1. Write implementation 2. Create PR 3. "Oh, should I write tests?" (asked by reviewer) 4. Write tests after the fact

正确示范（simulation-first）

1. Read TLA+ spec for invariants 2. Write DST test that verifies invariant 3. Run test -> FAILS (no implementation) 4. Write implementation 5. Run test -> PASSES 6. Run Stateright -> PASSES 7. Run unit + integration tests -> PASSES 8. Create PR with test evidence

关键差异在于：传统流程把测试当作实现的"事后补票"，而 simulation-first 把测试当作实现的"先行契约"——测试先失败再通过，恰好证明了测试与实现之间的对应关系。

何时必须使用 Simulation-First

文档明确划定了适用范围，这是团队决策的依据：

必须使用 simulation-first 的场景：

• 有状态组件（metastore、ingest 流水线、分片管理）；
• 并发协议（锁、事务、原子操作）；
• 分布式协调（control plane、集群成员管理）；
• 数据生命周期（ingest → index → compact → GC）；
• 恢复路径（崩溃恢复、WAL 回放）。

可以跳过 simulation-first 的场景：

• 纯函数（解析、格式化、序列化）；
• 简单 CRUD 端点；
• UI 改动；
• 配置改动；
• 文档。

即便如此，文档也补充了一条底线：即使跳过了 DST，只要实际可行，仍然应该在实现之前编写测试。

对照仓库，上述"必须"清单并非泛泛而谈。共享不变量模块 quickwit-dst/src/invariants/registry.rs 中登记的InvariantId枚举覆盖了排序模式（SS-1..SS-5）、时间窗口（TW-1..TW-3）、压缩作用域（CS-1..CS-3）、合并正确性（MC-1..MC-4）、数据模型（DM-1..DM-5）与合并流水线停机（MP-1..MP-11）共 31 个不变量——它们恰好对应"数据生命周期""恢复路径""并发协议"这些强制场景。

适配 Quickwit 的 Actor 模型

Quickwit 的并发组件基于 actor 框架 quickwit-actors，simulation-first 工作流为此给出了专门适配建议：

1. Actor 是天然的 DST 目标：每个 actor 都有 mailbox、消息类型与状态转移，非常适合模型检查；
2. 通过 mailbox 测试：发送消息，验证处理后的状态；
3. 在 actor 边界做故障注入：模拟消息丢失、慢处理、actor 崩溃；
4. 验证 supervisor 行为：测试 supervisor 能否正确重启失败的 actor。

文档给出的示例测试（以索引器 actor 为例）：

// Example: Testing an actor with DST #[test] fn test_indexer_actor_handles_storage_fault() { let config = SimConfig::new(SEED); let mut sim = Simulation::new(config) .with_fault(FaultConfig::new(FaultType::StorageWriteFail, 0.1)); sim.run(|env| async move { let indexer = IndexerActor::new(env.storage()); // Send messages through the mailbox indexer.send(IndexMessage::IndexBatch(batch)).await?; // Verify invariants hold despite faults assert!(indexer.state().splits_published >= expected_min); assert!(indexer.state().no_data_loss()); Ok(()) }); }

这段代码示范了 actor 场景下 DST 的三个要素：确定性种子（SEED）、概率化故障注入（FaultConfig::new(FaultType::StorageWriteFail, 0.1)，即 10% 概率触发存储写失败）以及"在故障下不变量仍然成立"的断言方式。

源码纵深：quickwit-dst 中验证栈的真实落地

工作流文档描述的是"应当如何开发"，而仓库中的 quickwit-dst crate 则是这套方法论的具体载体。其 lib.rs 明确写道：invariants模块是"整个验证金字塔共享的纯 Rust 不变量定义"（TLA+ 规范、Stateright 模型、DST 测试、生产debug_assert!检查全部复用），且零外部依赖；models模块则通过model-checkingfeature 启用 Stateright 模型检查。

共享不变量：单一事实来源

quickwit-dst/src/invariants/mod.rs 的模块文档定义了这一设计：不变量只定义一次，验证金字塔的所有层级共用。这与验证金字塔图（见 docs/internals/VERIFICATION.md）中"Shared Invariants ← SINGLE SOURCE OF TRUTH"的图示完全对应。

check_invariant! 宏：验证层的统一入口

quickwit-dst/src/invariants/check.rs 实现了check_invariant!宏，它是"预防"与"生产可观测性"两层之间的桥：

• 条件在 debug 与 release 构建中都会被求值；
• debug 构建下违反不变量会通过debug_assert!panic（开发期"大声失败"）；
• 所有构建下检查结果都会转发给已注册的InvariantRecorder用于指标上报（无记录器时为空操作）。

use quickwit_dst::check_invariant; use quickwit_dst::invariants::InvariantId; let duration_secs = 900u32; check_invariant!(InvariantId::TW2, 3600 % duration_secs == 0, ": duration={}", duration_secs);

记录器是可插拔的： recorder.rs 定义了set_invariant_recorder（进程启动时调用一次，首个写入者生效），并注明 OSS 二进制在quickwit_cli::logger中接入了 Prometheus 后端记录器。文档 docs/internals/VERIFICATION.md 进一步给出了生产监控的指标命名（如quickwit_invariant_checks.count、quickwit_invariant_checks_failed.count），用于在真实流量下证明"不变量在理论上的成立"。

Stateright 模型与穷举测试

model-checkingfeature（Cargo.toml 中定义，依赖 workspace 中的stateright）启用后，models/ 下的四个模型（sort_schema、time_windowed_compaction、parquet_data_model、merge_pipeline）会逐一镜像对应 TLA+ 规范的不变量，并以 Rust 测试形式跑穷举式 BFS 状态空间探索。

集成测试文件 stateright_models.rs 展示了实际运行方式（需--features model-checking）：

/// SS-1..SS-5: Sort schema invariants (ADR-002). /// Mirrors SortSchema_small.cfg: Columns={c1}, RowsPerSplitMax=2, /// SplitsMax=2, SchemaChangesMax=1. #[test] fn exhaustive_sort_schema() { let model = SortSchemaModel::small(); let result = model.checker().spawn_bfs().join(); result.assert_properties(); println!( "SortSchema: states={}, unique={}", result.state_count(), result.unique_state_count() ); }

该测试与SortSchema_small.cfg的配置一一对应（Columns={c1}、RowsPerSplitMax=2等），这正是工作流"DST 测试验证 TLA+ 属性"的直接证据。compaction与data_model两个穷举测试也分别镜像TimeWindowedCompaction_small.cfg与ParquetDataModel_small.cfg。

运行 TLA+ 模型检查器

正式规范的使用方法记录在 docs/internals/specs/tla/README.md 中。以小型配置快速验证为例（需 Java 与 TLA+ Toolbox /tla2tools.jar）：

TLA_JAR="/Applications/TLA+ Toolbox.app/Contents/Eclipse/tla2tools.jar" # ParquetDataModel (ADR-001): 8 states java -XX:+UseParallelGC -jar "$TLA_JAR" \ -config docs/internals/specs/tla/ParquetDataModel_small.cfg \ docs/internals/specs/tla/ParquetDataModel.tla # SortSchema (ADR-002): ~49K states java -XX:+UseParallelGC -jar "$TLA_JAR" \ -config docs/internals/specs/tla/SortSchema_small.cfg \ docs/internals/specs/tla/SortSchema.tla # TimeWindowedCompaction (ADR-003): ~938 states java -XX:+UseParallelGC -jar "$TLA_JAR" \ -config docs/internals/specs/tla/TimeWindowedCompaction_small.cfg \ docs/internals/specs/tla/TimeWindowedCompaction.tla

该 README 还记录了验证结果：三个小型配置全部通过、无违反不变量（ParquetDataModel 8 状态 <1s、SortSchema 49,490 状态 1s、TimeWindowedCompaction 938 状态 <1s），并通过 9 个变异测试（9 个全部被捕获）验证了不变量确实能检测出 LWW 去重、合成数据点注入、跨窗口合并等典型缺陷。创建新规范时，README 也提供了.tla与.cfg的标准模板，以及"先更新 TLA+ → 运行 TLC → 更新 Rust 实现 → 运行 DST 验证一致性"的规范与代码同步流程。

Runtime 抽象：为 DST 而约束生产代码

要支撑确定性模拟，生产代码本身必须做出让步。docs/internals/VERIFICATION.md 描述的 Runtime Trait 架构把四个维度抽象出来：

对应地，生产代码中被禁止直接使用Instant::now()、Utc::now()、tokio::time::sleep、thread_rng()，而必须经由runtime对象获取——这是 DST 能做到"同一种子完全复现故障"的前提。同时，quickwit-dst的 lib.rs 与 check.rs 中 "no external dependencies" / "条件总是被求值" 的设计，也都服务于同一目标：让验证层可以被安全地嵌入任何构建。

每个 PR 的检查清单

文档在结尾给出了适用于每个 PR 的强制检查清单：

• 已确认相关的 TLA+ 不变量
• 有状态组件的 DST 测试在实现之前编写
• DST 测试验证了 TLA+ 属性
• Stateright 模型通过（如适用）
• 单元 + 集成测试通过
• cargo clippy --workspace --all-features --tests通过
• cargo +nightly fmt -- --check通过
• PR 附带验证证据

延伸阅读

• Verification Guide：验证金字塔、DST 两种运行模式（In-Memory 与 gVisor）、Runtime 四维度、Kani 有界模型检查与生产指标命名；
• Verification Stack：从"发现（Discovery）→ 检测（Detection）→ 预防（Prevention）→ 生产可观测性"四个层面解释整套验证栈为何能提升代码正确性；
• TLA+ 规范目录：四份正式规范、配置模板与模型检查器运行方法；
• RUST_STYLE.md 与 CODE_STYLE.md：实现阶段的编码风格依据；
• 仓库实现参考：quickwit-dst（共享不变量与 Stateright 模型）、quickwit-actors（actor 框架）、quickwit-integration-tests（集成测试）。

【免费下载链接】quickwitCloud-native OSS search engine for observability项目地址: https://gitcode.com/GitHub_Trending/qu/quickwit