DST Bug #NNN: Description【免费下载链接】quickwitCloud-native OSS search engine for observability项目地址: https://gitcode.com/GitHub_Trending/qu/quickwitStatus: Fixed/OpenDiscovered: YYYY-MM-DDSeeds: comma-separated failing seedsComponent: crate::moduleSummaryReproductionRoot CauseFixVerificationLessons Learned种子Seeds字段是该文档的灵魂——正是它让 bug 可以被任何人确定性复现。 ## 4. TLA 形式化规范 ### 4.1 规范的内容与目标 人类可读的形式化规范位于 [docs/internals/specs/tla/](https://link.gitcode.com/i/35bf435b04d5ad48505107e60d5e0ea2)。仓库当前包含四份规范及配套 .cfg 配置 | TLA 规范 | 对应 ADR / 不变量前缀 | 配套 cfg | |-----------|----------------------|----------| | ParquetDataModel.tla | ADR-001DM-1..DM-5 | ParquetDataModel.cfg、ParquetDataModel_small.cfg | | SortSchema.tla | ADR-002SS-1..SS-5 | SortSchema.cfg、SortSchema_small.cfg | | TimeWindowedCompaction.tla | ADR-003TW/CS/MC 系列 | TimeWindowedCompaction.cfg、TimeWindowedCompaction_small.cfg | | MergePipelineShutdown.tla | MP-1..MP-11 | MergePipelineShutdown.cfg、MergePipelineShutdown_chains.cfg | 每份规范定义四类元素 - **State variables**系统追踪什么状态 - **Actions**状态转移 - **Invariants**必须始终成立的属性 - **Temporal properties**活性liveness保证。 ### 4.2 何时编写规范 **需要写规范** - 并发协议事务、锁 - 状态机生命周期、恢复 - 一致性保证exactly-once、顺序 - 资源管理GC、缓存 **跳过规范** - 简单 CRUD - 无状态转换 - 已被充分理解的算法 ### 4.3 需要规范的关键领域 | Area | Component | Key Invariants | |------|-----------|----------------| | Split lifecycle | quickwit-metastore | No lost splits, no premature visibility | | Compaction | quickwit-indexing | Atomic split swap, no data loss | | Ingest pipeline | quickwit-ingest | Backpressure, bounded buffers | | Shard management | quickwit-control-plane | No split-brain, consistent assignment | | Tantivy Parquet | quickwit-indexing | Dual-write consistency | 这些领域恰好对应 Quickwit 分布式架构中最容易出现竞态和故障的部分元数据丢失、压缩非原子、背压失控、分片脑裂、双写不一致。 ## 5. 共享不变量单一事实来源 ### 5.1 核心思想与 API **单一事实来源**不变量定义只存在于一处被所有验证层使用。 rust // Both DST and production code use the same invariant definitions use quickwit_invariants::{SplitPropertyChecker, PropertyChecker}; let checker SplitPropertyChecker::new(state); let result checker.no_lost_splits(); if !result.holds { println!({}, result); // no_lost_splits: Split abc123 not visible in metastore }在仓库中这一思想的落地位于 quickwit-dst/src/invariants/mod.rs 明确写道该模块是 single source of truth包含纯 Rust 函数与类型表达整个验证金字塔TLA、Stateright、DST、生产代码要验证的不变量零外部依赖、仅用stdregistry.rs 定义了InvariantId枚举按SPEC_PREFIXNUMBER命名覆盖 SS-1..SS-5、TW-1..TW-3、CS-1..CS-3、MC-1..MC-4、DM-1..DM-5、MP-1..MP-11 共 30 个不变量 ID并附带as_str()热路径上返回static str避免分配与description()。以InvariantId中定义的部分不变量为例ID含义descriptionSS-1每个 split 内的行按该 split 的 schema 排序SS-2null 永远排在非 null 之后与排序方向无关TW-2window_duration必须整除 3600 秒1 小时TW-3数据绝不跨时间窗口合并MC-1压缩保持行多重集合不变不增、不减、不重复MP-4已发布 split 的总行数 累计摄入行数跨崩溃/重启仍成立MP-7没有任何 split 同时出现在两个并发进行中的合并里MP-10孤儿输出已上传未发布与已发布 split 不相交5.2 不变量模块规划ModulePropertiessplits.rsno_lost_splits,no_premature_visibility,no_zombie_splitscompaction.rscompaction_atomicity,no_data_loss_during_compactioningest.rsno_buffer_overflow,backpressure_correctnessshard.rsno_split_brain,shard_assignment_consistencytantivy_parquet.rstantivy_subset_of_parquet,idle_consistency5.3 共享不变量在源码中的实际形态原文档中的不变量模块规划是to build清单仓库当前已落地的是sort、window、merge_pipeline、merge_policy、recorder、registry、check等模块。这里以两个典型例子说明单一事实来源如何同时被模型与生产代码使用例一null 排序不变量SS-2——sort.rspub fn compare_with_null_orderingT: Ord( a: OptionT, b: OptionT, ascending: bool, ) - Ordering { match (a, b) { (None, None) Ordering::Equal, (None, Some(_)) Ordering::Greater, // null always after non-null (Some(_), None) Ordering::Less, // non-null always before null (Some(va), Some(vb)) { if ascending { va.cmp(vb) } else { vb.cmp(va) } } } }该函数是 SS-2 的单一事实来源注释明确指出它同时被 Stateright 的sort_schema模型与生产代码使用与写入端nulls_first: false保持一致——正因为缺失的排序列被隐式处理为 nullabsent 列才可以简单地从 sorted_series 键中省略。例二时间窗口数学TW-1/TW-2——window.rspub fn window_start_secs(timestamp_secs: i64, duration_secs: i64) - i64 { timestamp_secs - timestamp_secs.rem_euclid(duration_secs) } pub fn is_valid_window_duration(duration_secs: u32) - bool { duration_secs 0 3600 % duration_secs 0 }注意window_start_secs使用rem_euclid而非%标准取模向零截断-1 % 900 -1错误rem_euclid恒返回非负值(-1i64).rem_euclid(900) 899从而正确处理 Unix 纪元之前的负时间戳。其注释明确说明这镜像了 TLA 中的WindowStart(t) t - (t % WindowDuration)。而is_valid_window_duration正是 TW-2 的实现——合法值必须是 3600 的正约数1、2、3、4、5、6、8、9、10、12、15、16、18、20、24、25、30、36、40、45、48、50、60、72、75、80、90、100、120、144、150、180、200、225、240、300、360、400、450、600、720、900、1200、1800、36007、11、7200 等均非法。该模块的单元测试window.rs覆盖了负时间戳、窗口边界、合法/非法时长四类情况。5.4 check_invariant 宏把不变量接到运行时与指标check.rs 定义了一个贯穿预防层与生产可观测层的宏check_invariant!(InvariantId::TW2, 3600 % duration_secs 0, : duration{}, duration_secs);其语义是条件在所有构建配置debug 与 release下都会求值——debug 构建下违规会通过debug_assert!直接 panic对应验证金字塔的 Prevention 层所有构建下结果都会转发给注册的InvariantRecorder用于指标发射对应 Production 层未注册 recorder 时是 no-op单次原子加载。6. Stateright 模型检查6.1 运行方式与优势Stateright 是 Rust 原生的穷举式状态空间探索工具# Run Stateright model checking cargo test -p quickwit-dst stateright -- --ignored相对于 TLA 的优势在 CI 中用cargo test直接运行使用 Rust 类型系统与 DST 共用同一套共享不变量无需独立的 TLC 工具链。6.2 编写 Stateright 模型impl Model for SplitLifecycleModel { type State SplitState; type Action SplitAction; fn init_states(self) - VecSelf::State { ... } fn actions(self, state: Self::State, actions: mut VecSelf::Action) { ... } fn next_state(self, state: Self::State, action: Self::Action) - OptionSelf::State { ... } fn properties(self) - VecPropertySelf { vec![ Property::always(no_lost_splits, |_, state| { let checker SplitPropertyChecker::new(state); checker.no_lost_splits().holds }), ] } }注意properties()中复用的正是SplitPropertyChecker——同一个不变量检查器同时服务 DST 与 Stateright 模型模型层与运行时检查共享同一份 Rust 函数与同一份状态结构从结构上杜绝了模型与实现漂移。6.3 仓库中的模型实现仓库在 quickwit-dst/src/models/ 下提供了四个镜像 TLA 规范的模型需model-checkingfeature 编译sort_schema.rs— SS-1..SS-5ADR-002SortSchema.tlatime_windowed_compaction.rs— TW-1..TW-3、CS-1..CS-3、MC-1..MC-4ADR-003TimeWindowedCompaction.tlaparquet_data_model.rs— DM-1..DM-5ADR-001ParquetDataModel.tlamerge_pipeline.rs— MP-1、MP-4..MP-11MergePipelineShutdown.tla与invariants::merge_pipeline字面共享状态类型与谓词函数以 merge_pipeline.rs 的文档注释为例该模型是MergePipelineShutdown.tla的 Rust 对应物动作集合一一镜像 TLA 的 Next 关系——IngestSplit、PlanMerge、UploadMergeOutput合并完成阶段一此处崩溃会孤儿化上传、PublishMergeAndFeedback阶段二原子替换元数据 可选 planner 反馈、DisconnectMergePlanner、RunFinalizeAndQuit、DrainComplete、Crash以max_crashes为界、Restart以max_restarts为界从持久化的published_splits重新播种 planner模拟全新进程启动。该模型从 invariants::merge_pipeline 导入no_split_loss、rows_conserved、bounded_write_amp、no_duplicate_merge、restart_re_seeds_all_immature等谓词——模型与运行时检查求值的是同一批 Rust 函数因此模型漂移在结构上不可能发生。6.4 集成测试穷举 BFS 验证stateright_models.rs 提供了穷举模型检查的集成测试需要--features model-checking编译运行#[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() ); }三个测试分别对应 small 配置exhaustive_sort_schema— 镜像SortSchema_small.cfgColumns{c1}, RowsPerSplitMax2, SplitsMax2, SchemaChangesMax1验证 SS-1..SS-5exhaustive_compaction— 镜像TimeWindowedCompaction_small.cfg验证 TW/CS/MC 共 10 条不变量exhaustive_data_model— 镜像ParquetDataModel_small.cfgNodes{n1}, MetricNames{m1}, TagSets{tags1}, Timestamps{1}, RequestCountMax3验证 DM-1..DM-5。spawn_bfs()以广度优先搜索穷举状态空间result.assert_properties()在任一不变量被违反时让测试失败并输出状态数与唯一状态数供分析。6.5 生产侧事件流让模型吃真实轨迹events/mod.rs 展示了另一个值得关注的模式生产侧事件流用于轨迹一致性测试trace-conformance testing。它镜像invariants::recorder的模式——全局可插拔观察者生产代码在每次状态转移时调用record_*_event测试安装观察者把事件捕获进 collector再回放给 Stateright 模型。这意味着模型不仅能从随机/穷举生成的轨迹中验证还能回放生产系统的真实行为轨迹来确认模型与生产实现一致。7. Kani 有界模型检查7.1 运行方式Kani 验证debug_assert!不变量对所有输入都成立有界模型检查# All proofs cargo kani # Specific crate cargo kani --package quickwit-metastore # Specific proof cargo kani --package quickwit-metastore --harness verify_no_lost_splits平台注意Kani 在 x86_64 Linux 上表现最佳应在 CI 中运行以获得可靠结果原文档明确提示。7.2 编写 Kani Proofs#[cfg(kani)] mod kani_proofs { use super::*; #[kani::proof] #[kani::unwind(10)] // Bound loops fn verify_my_invariant() { let input: u64 kani::any(); kani::assume(input 0); let result my_function(input); kani::assert(result input, Result must exceed input); } }要点kani::any()生成任意输入kani::assume()约束前提kani::unwind(10)为循环提供有界展开kani::assert()声明必须对所有可达输入成立的结论。8. 生产可观测性闭合验证闭环8.1 在生产中记录不变量形式化验证证明属性理论上成立生产可观测性证明属性实践中成立// Record invariant check in production quickwit_observability::record_invariant(no_lost_splits, passed);仓库中的实际实现是 recorder.rs全局OnceLockInvariantRecorderset_invariant_recorder在进程启动时注册一次first-writer-wins线程安全record_invariant_check每次check_invariant!调用都会执行未注册 recorder 时为 no-op单次原子加载实现必须廉价因为可能落在热路径上。其单元测试验证了无 recorder 时不 panic与recorder 收到调用并统计违规次数两条路径。可插拔 recorder 支持多种后端OSS Quickwit 二进制在quickwit_cli::logger中接入了 Prometheus 后端文档注释给出了最小 recorder 形状fn my_recorder(id: InvariantId, passed: bool) { if !passed { eprintln!({} violated in production, id); } } set_invariant_recorder(my_recorder);8.2 不变量指标MetricPurposequickwit_invariant_checks.countTotal checksquickwit_invariant_checks_passed.countPassed checksquickwit_invariant_checks_failed.countFailed checks (0 healthy)quickwit_invariant_healthHealth gauge (1.0 all passing)quickwit_invariant_health是一个聚合健康度1.0 表示全部通过适合直接接入告警。8.3 添加生产不变量// 1. Add verification method impl SplitMetastore { async fn verify_no_lost_splits(self, ...) - bool { // Check condition } } // 2. Call record_invariant after operation let passed self.verify_no_lost_splits(...).await; quickwit_observability::record_invariant(no_lost_splits, passed);8.4 形式化验证与生产观测的互补Formal Verification SaysProduction ShowsNo lost splits is provableNo lost splits held for 30M real operationsBackpressure triggers at 80%Backpressure triggered 47 times, all at 81-83%Recovery completes in finite timeRecovery P99 is 2.3 seconds, P99.9 is 8.1 secondsConcurrent operations are safe12 optimistic retry conflicts per hour at peak形式化验证的局限在于TLA 模型是抽象不捕获实现 bug、Stateright 探索有限状态空间生产有无限多样性、Kani 对输入有界生产输入无界。生产观测恰好补上这些盲区并形成完整反馈回路生产指标反馈 → 修复证明缺口 / 优化真实热路径 / 把错误模式编码进 DST / 回滚回归提交 → 改进规范、模型与代码【免费下载链接】quickwitCloud-native OSS search engine for observability项目地址: https://gitcode.com/GitHub_Trending/qu/quickwit创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考