windyboy
3085431bea
- G-IGNORE 缺口表述去掉错引 INV-19、补 US-04 - reference 登记 msgx.pipeline.backfill-scan-period - user-stories 的 R_keep 下界/deadline 措辞对齐 - reference 归档参数行从空行后挪回参数表内（修正 acm2-52 提交中的表格位置）
121 lines
12 KiB
Markdown
121 lines
12 KiB
Markdown
# 前提、不变量与声明边界
|
||
|
||
本文件是三件东西的唯一出处：
|
||
|
||
- **前提 PRE-x**：由外部提供、我们无法单方保证的事实。前提失效时不变量必须整体重估。
|
||
- **不变量 INV-x**：本系统自己保证的性质。变更用「追加 + 作废」（`INV-7 → [作废 by INV-7b]`），不静默改写。
|
||
- **声明边界 CLM-x**：每条对外主张依赖哪些 PRE/INV、当前**可否声明**、挂起原因（`[G-x]` 缺口 / `[Q-x]` 待确认）。
|
||
|
||
验证映射在本文件 §4，是验收口径的唯一清单；代码与测试只做证据，不在此重复叙述。
|
||
|
||
## 1. 前提（外部提供）
|
||
|
||
| 编号 | 前提 | 若不成立的影响 | 状态 |
|
||
|---|---|---|---|
|
||
| PRE-1 | 信箱消费权排他：同一时刻只有一个系统有权处理、打标、判定可清除（迁移期由切流规程保证单一权威写者） | 水位、身份去重、清除前提全部失效 | `[待确认]`（切流由运维规程保证，上线前另立） |
|
||
| PRE-2 | ID 单调 + 可见时延上界：见 `C-1`/`C-2` | 水位只能当快路径提示；空洞老化阈值无依据；不能声明发现完整性 | `[待确认 Q2]` |
|
||
| PRE-3 | ID 空间不复位、不复用、不回退：见 `C-3` | 水位（不可逆单游标）之后的行永久不可见 | `[待确认 Q2]` |
|
||
| PRE-4 | 报文的 `DATE_RECEIVED` 时钟基准可解释（偏斜在有界范围内） | 跨系统时间比较（`RECEIVED_AT` 与本地 `NOW`）会提前或推迟判定 | `[待确认 Q7]` |
|
||
| PRE-5 | 单活动实例运行（信箱读取不加锁、水位是单行覆盖写） | 水位互相覆盖、空洞计时失真 | `[我们自证]`（部署约束，见 architecture） |
|
||
| PRE-6 | 信箱与自有 PG 之间没有跨库事务 | 回填、水位推进、清除都不能声称原子 | `[我们自证]`（架构事实） |
|
||
| PRE-7 | 报文不可变：同一业务身份的重发必为同一内容：见 `C-4` | 上游改发会被判为重复并静默跳过 | `[待确认 Q15]` |
|
||
| PRE-8 | `FLID` 在保留期内不复用：见 `C-21` | 「保留最新版本」的合并规则可能压掉新航班事件，旧 tombstone 可能删掉在用航班 | `[待确认 Q16]` |
|
||
|
||
## 2. 不变量
|
||
|
||
### A. 管道
|
||
|
||
- **INV-1** 五个独立事实互不替代：落信 / 入队 / 处理完成 / 已回填 / 投递确认各有独立证据，前一个不蕴含后一个。
|
||
- **INV-2** 水位与入队同事务：不允许出现「水位已推进、消息未入队」的持久化状态；水位只增不减，遇空洞即停，只有判定为永久空洞才放行，且放行只跳过空洞本身、不越过任何已存在的行。
|
||
- **INV-3** 队头唯一：任一时刻只有一个可执行队头（最小未完成 `MSG_ID`，`PENDING` 与 `FAILED` 都占位）；`FAILED` 未退避到期时后续消息不得越过。
|
||
- **INV-4** 只领取已发现的行：主泵只领 `MSG_ID ≤ W`；水位之外的行只可能来自兼容入口，必须等水位追平后按序处理。
|
||
- **INV-5** 发现与处理互不阻塞：收报只看 `ID > W`，不以处理标记为谓词；终态而未回填的行不阻断后续消息的发现。
|
||
- **INV-6** 处理终态不可逆：已提交的 `SUCCEEDED` 不因回填或投递失败回改。
|
||
- **INV-7** 处理标记单调：任何路径只把空标记写成已处理值，不回撤、不覆盖。
|
||
- **INV-8** 回填只针对终态（`PENDING` / `FAILED` 永不写标记）；「还欠一次回填」的事实与终态由**同一条语句**落库，不存在第二处落账。
|
||
- **INV-9** 一信一行、一身份一记录：`PROC_STATE` 按 `MSG_ID` 唯一；同一业务身份至多绑定一条有效处理记录。
|
||
- **INV-10** 对外投递至少一次；端到端恰好一次不在交付范围。
|
||
|
||
### B. 航班域（定义处；flight-state.md 只引编号）
|
||
|
||
- **INV-11** 自有 PG 的航班当前态是唯一权威；信箱、Kafka、展示视图都不是权威。
|
||
- **INV-12** `FLID` 唯一；已写入非空的 `OPERATION_DAY` 不可改变。
|
||
- **INV-13** 每个航班每次成功状态写入单调推进 `STATE_VERSION`；重复消息不重复推进。
|
||
- **INV-14** 报文未携带的字段不被隐式清空；集合按完整合并结果写入，保留输入顺序与源序号。
|
||
- **INV-15** 缺席于某个日计划不构成删除理由；删除只由 FDEL 或受控历史清理触发。
|
||
- **INV-16** 外部副作用（回填、Kafka 投递、出站信箱）失败可重试，但不回滚已提交的本地业务结果。
|
||
- **INV-17** 状态变更、待发事件、处理终态与回填意图在同一 PG 事务内原子提交。
|
||
- **INV-18** 航班表的写者集合是「主泵处理器」与「历史清理」；两者必须互斥（同一 `PIPELINE_LOCK`，或清理在同一事务内复查判据后再删除），不得出现清理删除与处理器更新同一 `FLID` 的竞态。`[实现核对待确认，关联 ACM2-30]`
|
||
- **INV-19** 整包校验失败或运营日冲突时整包不落地，既有状态与版本保持不变。
|
||
- **INV-20** 处理器幂等：同一消息重复执行只产生一次业务效果。身份唯一只防「重复记录」，不防「重新执行」；29 类 FLOP 幂等矩阵补全前，本条**不可声明**。`[G-FLOP-IDEMPOTENT]`
|
||
|
||
## 3. 声明边界
|
||
|
||
| 编号 | 主张 | 依赖 | 当前可否声明 | 挂起原因 |
|
||
|---|---|---|---|---|
|
||
| CLM-1 | 严格 FIFO：迟到的小 ID 不会越序 | PRE-2、PRE-3、`Q2` | **不可** | 发现完整性依赖库方承诺；窗口补偿扫描（G1）未交付 |
|
||
| CLM-2 | 迟到报文不丢（可被发现并处置） | `G1` | **不可** | G1 未交付；现有阶段 0 只读检测仅计数告警，不补入队 |
|
||
| CLM-3 | 重放不产生重复业务副作用 | INV-20、`G-FLOP-IDEMPOTENT` | **不可** | 29 类 FLOP 幂等矩阵未补全；重放不恢复历史顺序 |
|
||
| CLM-4 | 回填不会被短暂故障放弃：最终打标，或进入可对账的放弃清单 | INV-8、`C-5`、`C-8` | **可声明（有条件）** | 条件：`R` 之前不放弃；`MISSING_ROW` 立即放弃并告警；放弃行须经人工对账才可用于清除判定（`C-8`）。原文保留另见 CLM-5 |
|
||
| CLM-5 | 重放窗口内原文仍可读 | `C-6`、`C-7`、`Q7`、`Q9` | **不可** | 清除语义与保留期未确认；「打标即清除」下无补救 |
|
||
| CLM-6 | 单实例内严格 FIFO | PRE-5、INV-3 | **可**（限于单活动实例） | — |
|
||
| CLM-7 | 事件投递在同一 `FLID` 内保序 | INV-10、投递设计 | **可**（跨 `FLID` 不承诺） | 实现当前按目标级全序投递，收敛到按 `FLID` 属投递改造，关联 ACM2-34 |
|
||
| CLM-8 | 出站交付承诺只到「落信」 | `C-24`、`Q10` | **可**（仅落信语义） | 消费方与 ACK 列语义未确认 |
|
||
| CLM-9 | 处理标记延迟由调度周期决定（≤30 秒） | — | **不可** | 30 秒只是扫描调度周期；批次积压、单行超时与历史作业都会延长实际延迟 |
|
||
| CLM-10 | 容量量级假设（单实例、入站日消息量千级到万级、单报文 ≤ 10⁴ 字节） | — | **不可** | 未实测，无生产负载数据；解除条件：取得现役信箱日量、峰值与单报文上限后重估 |
|
||
|
||
## 4. 验证映射
|
||
|
||
每条不变量至少一条证据；「缺口」表示尚无回归。测试名以仓库现状为准，新增测试按此表补位。
|
||
|
||
| 不变量 | 场景 | 证据 / 缺口 |
|
||
|---|---|---|
|
||
| INV-1 | 五事实互不替代：入队不引用标记、回填不引用投递、投递不引用回填 | 缺口（需接口级断言） |
|
||
| INV-2 | 重复扫描、入队中断 | 不重复入队、不丢记录；`InboxPollerTest` |
|
||
| INV-2 | 空洞老化与重置 | 阈值内不推进、不越过入队；超期只放行空洞本身；旧空洞补齐后新空洞获得完整窗口 |
|
||
| INV-2 | 水位写入与入队同事务 | 缺口（需真实 PG 事务用例，关联 ACM2-39） |
|
||
| INV-3 / CLM-1 | 较小 ID 迟到 | **缺口基线已固定**：`InboxPollerTest` 钉住「水位越过后到达的较小 ID 不被发现」；补偿扫描交付前禁止任何「迟到不越序」的验收声明 |
|
||
| INV-4 | 兼容入口与空洞并发 | 兼容入口登记的行超出水位、主泵不领取；`PipelineSmokeTest`「compat injected high id is not claimed until the watermark catches up」 |
|
||
| INV-3 | 队头失败、退避及作业竞争 | 消息不越队；到期后恢复；作业不使消息无限饥饿 |
|
||
| INV-5 | 终态未回填不阻断发现 | 缺口（补齐后应断言发现谓词不引用处理状态） |
|
||
| INV-6 | 投递失败后终态不变 | 缺口 |
|
||
| INV-7 | 回填四种结果 | 写入成功 / 早已标记（不覆盖、记成功）/ 信箱行不存在（立即放弃并告警，不得视为已标记）/ 暂时故障持续到 `R` 仍未打标（停止自动重试，可人工恢复） |
|
||
| INV-7 | `RECEIVED_AT` 为 NULL | 超期分支仍成立且不导致标记提前写入——判据是本地 `ENQUEUED_AT`，与库方时钟及 NULL 无关 |
|
||
| INV-8 | PG 提交失败、信箱回填失败 | 事件、终态与回填意图一起回滚；已提交结果只补写标记，不重放业务；中间态永不补写 |
|
||
| INV-8 | 非业务型终态 | 不触碰航班表 / `MSG_EVENT`，只写 `PROC_STATE`，且终态与回填意图同语句生效 |
|
||
| INV-9 | 同身份多条记录、失败后重试、归档后重复 | 只产生一次有效业务处理，不把自身重试判为重复 |
|
||
| INV-10 | 投递确认丢失、批次失败、次数耗尽 | 允许可识别的重发、保持目标顺序、整批退避并保留死信 |
|
||
| INV-11 | 权威唯一 | 缺口（展示视图与缓存不得成为写入或对账来源） |
|
||
| INV-12 / INV-13 | PG 事务失败、快照重复或迟到 | 整体回滚重试、不重复推进版本、不回退状态、不误删增量航班 |
|
||
| INV-12 | 运营日冲突 | 整包 `DEAD(PROTOCOL)`，既有状态与版本不变 |
|
||
| INV-14 / INV-19 | 整包协议拒绝（声明数不符、缺载荷） | 整包不落地、整体回滚、既有状态不变 |
|
||
| INV-15 | 缺席不删除 | 缺口（F-del 与清理路径分别断言） |
|
||
| INV-16 | 外部副作用失败后本地结果不变 | 待核对 |
|
||
| INV-17 | 业务型终态四件套同事务 | 待核对；真实 PG 用例待补（ACM2-39） |
|
||
| INV-18 | 清理与处理并发 | **缺口**：需断言删除与处理同一 `FLID` 时互斥（关联 ACM2-30） |
|
||
| INV-20 / CLM-3 | 重放同一条消息 | 缺口：29 类 FLOP 幂等矩阵未补全 |
|
||
| CLM-4 | 放弃行与清除前提 | 断言放弃行不写标记、不被当作已打标（关联 ACM2-36） |
|
||
| CLM-9 | 回填/积压完成时限 | 缺口：需要「最老待回填年龄」「扫描积压」「作业心跳」指标（关联 ACM2-38） |
|
||
| — | 请求超时、无匹配 RESP、时间单位不一致 | 不误用迟到应答、不提前完成请求 |
|
||
| — | stub 误配置、重复实例、停机中断 | 生产拒绝不安全启动，工作线程能正确退出 |
|
||
|
||
## 5. 缺口索引与 Plane 的关系
|
||
|
||
本表是**缺口标记的唯一清单**：其他文档只在相应位置写 `[G-x]`，不解释、不记进度；工作进度在 Plane（ACM2）。
|
||
|
||
| 缺口 | 含义 | 影响 |
|
||
|---|---|---|
|
||
| `G1` | 窗口补偿扫描未实现（Plane ACM2-41）：水位越过后的迟到小 ID 没有补入队机制 | CLM-1、CLM-2 |
|
||
| `G-IGNORE` | 忽略规则（`LDM`/`REGN`/`RSTA`/`EROR`）未实现 | US-04；合法忽略报文当前按 `UNSUPPORTED` 处理 |
|
||
| `G-RESP-GUARD` | `RESP` 应答守卫未实现，当前与 `DNLD` 无差别进入快照写入 | 请求匹配闭环；`C-23` |
|
||
| `G-REQ-TRACK` | `REQ_TRACK` 无运行时协调器：出站适配、请求编码、超时与应答匹配未实现 | US-08；`C-24` |
|
||
| `G-PROC-HST` | `PROC_STATE_HST` 未建表，终态归档未落地 | US-11；归档能力 |
|
||
| `G-FLOP-IDEMPOTENT` | 29 类 FLOP 幂等矩阵未补全 | `INV-20`、CLM-3 |
|
||
| `G-EVENT-RETENTION` | `MSG_EVENT` 已发送行的保留期与清理作业未实现 | outbox 有界性 |
|
||
| `G-BACKFILL-BACKOFF` | 回填独立退避键（`backfill-backoff-ms` / `-cap-ms`）未实现，当前为代码内硬编码（取值见 reference） | 回填重试节奏 |
|
||
| `G-KAFKA-D3` | `kafka.producers.default.max-in-flight` 与 D3 要求的 1 不一致（取值见 reference） | 投递幂等前提 |
|
||
| `G-JOB-HEARTBEAT` | 作业心跳、扫描积压、实际回填延迟指标未实现 | CLM-9；回填可观测性 |
|
||
| `G-REPLAY-CHANNEL` | 「打标即清除」语义下的独立原文保留通道未设计 | CLM-5 |
|
||
|
||
`G1` 沿用 Plane 既有编号（ACM2-41）；其余为文档内稳定标记，与 Plane 工作项的对应关系在 Plane 侧维护。
|