跳到主要内容
AURA 论文精讲

第7章：迁移协议与 I1–I4 一致性证明

按论文 §4 逐段重读：AcquireAuthority / ValidateAuthority 双接口、本地快路径 vs 远程慢路径 vs fallback 三分叉、freeze-drain-handoff-publish 四阶段时序、I1–I4 不变量的违反 corner case + 防御 + 一致性论证草图（四个 paragraph proof）

AURA Migration Protocol Freeze-Drain-Handoff I1-I4 Consistency Proof AcquireAuthority ValidateAuthority Linearization Point 论文精讲

第 6 章把 cohort → owner 的规划和事务 → home CN 的路由讲完了，本章正式进入协议层——论文 §4。这是整个 AURA 论文的”安全性核心”：怎么在 cohort 漂移时不丢一致性。论文按”事务执行（§4.1–4.3）→ fallback 与权威唯一（§4.4）→ 迁移协议（§4.5）→ 一致性论证（§4.6）“四个层次展开。本章按一一对应顺序，把双接口 AcquireAuthority/ValidateAuthority、三种事务执行路径（local fast / remote slow / fallback）、4 阶段迁移时序、4 段一致性证明 paragraph 一次性讲透。读完你能：(1) 徒手画 4 阶段时序图；(2) 给出 I1–I4 每条的违反 corner case + 防御代码；(3) 用 4 段证明草图回答 reviewer “你怎么证明没双授权”的问题。

📑 目录

1. §4.1 协议接口：AcquireAuthority + ValidateAuthority

1.1 两个接口的职责分离

AURA 把事务的”加锁”动作拆成两个显式接口：

   AcquireAuthority(cohort_list)     // 事务执行开始前
   ────────────────────────────────────
   for each c in cohort_list (按全局 cohort_id 排序):
     根据 mode 进入：本地快路径 / 远程慢路径 / fallback / 等待重试
     拿到 token 或 fallback 锁
   返回 token_list

   ValidateAuthority(token_list)     // 事务 commit 前
   ────────────────────────────────────
   for each token in token_list:
     if token.epoch < owner_map[token.cohort].epoch:
       return ABORT     // I2 违反：epoch 过期
     if token.mode != owner_map[token.cohort].mode:
       return ABORT     // 迁移在事务中途发生了
   return COMMIT_OK

🌟 关键设计：

  • AcquireAuthority = 取锁
  • ValidateAuthority = commit 前再验一次锁还有效

🧠 关键洞察：这两个接口是 AURA 不变量 I2 的”机制”——AcquireAuthority 给 token 打 epoch 戳，ValidateAuthority 在 commit 前验戳。中间任何迁移都会让 epoch 不对，事务被迫 abort。这就是论文里 “epoch 单调” 落地的工程手段。

1.2 事务伪代码（论文 Table 5）

1. M ← owner map 只读快照
2. home ← route(T, M)
3. for c in C(T) sorted by global cohort_id:
4.   if mode(c) = owned and owner(c) = home:
        本地 OwnerLockTable.TryAcquire → token
5.   elif mode(c) = owned and owner(c) != home:
        OwnerRpc.RequestToken(owner, c) → token
6.   elif mode(c) = fallback:
        MN masked-CAS → fallback_lock
7.   elif mode(c) = transferring:
        等待 / 重新路由 / abort 重试
8. 通过 RDMA READ/WRITE 访问 MN 数据
9. ValidateAuthority(token_list) → COMMIT or ABORT
10. 释放所有 token / fallback lock

🌟 结论：事务执行的 4 条分支（owned-local / owned-remote / fallback / transferring）由 mode 决定——这是 AURA 三态状态机在事务路径上的体现。

1.3 按 cohort_id 排序：避免跨 owner 死锁

   反例：
   T1 持有 cohort_A 的 token，等 cohort_B
   T2 持有 cohort_B 的 token，等 cohort_A
   → 死锁

🌟 防御：所有事务按全局 cohort_id 升序加锁 → 不会出现环 → 不会死锁。

🍎 直觉比喻：和银行家算法一样的思路——“所有线程按同一顺序申请资源就不死锁”。

2. §4.2 本地所有者快路径

2.1 7 步流程

   1. 解析读写集合：通过 Begin → SelectRecord/InsertRecord 构造 read_set / write_set
   2. 检查 epoch：读 owner_map[c].epoch，记下 token.epoch
   3. 本地加锁：OwnerLockTable 上 lock_cmpxchg（CPU 指令，不发 RDMA）
   4. RDMA READ 拉数据：从 MN 读 record content + version
   5. 执行 + 版本验证：按 CREST/Motor OCC 风格做 validation
   6. 提交写回：RDMA WRITE + 原 commit 协议
   7. 本地解锁：OwnerLockTable.Release

2.2 关键收益

🌟 结论：步骤 3 的加锁从”RDMA atomic CAS”换成”本地 lock_cmpxchg” —— 这是 AURA 唯一改变的地方，其他全部不动。

操作原 CRESTAURA local数量级
加锁RDMA atomic CAS (~2 μs)lock_cmpxchg (~10 ns)200× 加速
数据读RDMA READ (~2 μs)RDMA READ (~2 μs)不变
commit 写RDMA WRITE (~2 μs)RDMA WRITE (~2 μs)不变

🧠 关键洞察：单一事务的延迟不一定大幅降低（仍要 RDMA READ/WRITE），但集群吞吐上限提升（lock_cmpxchg 不受 AU 物理墙限制）。

📎 工程踩坑视角：模块十五第 7 章讲过这一点——AURA 的 headline 是 atomic_per_txn 而不是单事务延迟，原因就在这里。

3. §4.3 远程所有者慢路径

3.1 两种慢路径选择

方案触发条件代价
OwnerRpc（CN_i → CN_j 一次 RPC）home CN 持多数写锁，少数 cohort 在别处一次 RPC ~5 μs + 批量摊薄
重新路由（重发到更优 home CN）home CN 完全错位、事务未开始执行一次 dispatch ~3 μs

🌟 结论：慢路径不是为了”消灭远程通信”，是为了”把 atomic 从 MN AU 路径换到 CN-CN RPC 路径”——CN-CN RPC 受 CN 数水平扩展，AU 不能。

3.2 OwnerRpc 协议

   CN_i (home) ──RPC RequestToken(c, key_list, txn_id, epoch=e)──► CN_j (owner of c)
       │                                                              │
       │                                                              │ TryAcquire on OwnerLockTable
       │                                                              │
   CN_i ◄──Reply(token_list, granted_epoch=e)──────────────────── CN_j
       │
       │ ... 事务执行 ...
       │
   CN_i ──RPC ReleaseToken(token_list, txn_id)─────────────────────► CN_j

🧠 关键洞察：OwnerRpc 是 batch 友好——一个事务的所有 cohort_j 的请求可以打包成一个 RPC，分摊 RPC overhead。

📎 工程踩坑视角：模块十五第 12 章讲过为什么 OwnerRpc 走 TCP 而不是 RDMA——slot 256B 装不下 NewOrder ~450B 的 token 请求。

4. §4.4 Fallback 与权威唯一性规则

4.1 论文核心规则

🌟 权威唯一性规则：对任一锁簇 cc，任一 epoch 内只能存在一个锁权威：要么由 owner CN 的本地锁表裁决，要么由 MN 上的远端锁字通过 RDMA CAS 裁决，不能二者并存。

这就是 I1 的工程化语句。

4.2 违反 corner case（必须挡）

   1. cohort c 当前 mode = owned, owner = CN_1
   2. T1 在 CN_1 OwnerLockTable.TryAcquire(c) → 成功
   3. 同时 T2 在 CN_3 看到一份**陈旧** owner_map（mode=fallback）
   4. T2 跳过 owner，直接 MN masked-CAS(c.slot) → 成功
   5. 两个 token 都被授予 → 双写

🌟 防御：

  • 任何 cohort 处于 owned 模式时，所有 CN 必须走 owner 路径，禁止直接 MN CAS
  • ValidateAuthority 在 commit 前再验一次 mode 和 epoch
  • 切到 fallback 必须等所有 owner 本地 token drain 完

🧠 关键洞察：权威唯一性是 I1 + I3 的综合——I1 保证模式互斥、I3 保证迁移期间不并发授权。两者一起防 corner case。

4.3 mode 的”准入许可证”角色

// 在 AcquireAuthority 内部
switch (owner_map[c].mode) {
    case OWNED:
        if (owner_map[c].owner == self_cn) goto local_fast_path;
        else goto remote_slow_path;
    case FALLBACK:
        goto mn_cas_path;
    case TRANSFERRING:
        goto wait_or_retry;
}

🌟 结论：mode 是事务路径选择的唯一依据。任何”绕过 mode 判断”的代码都会破坏 I1。

5. §4.5 4 阶段迁移协议：freeze-drain-handoff-publish

5.1 4 阶段时序

   ──────────────── Time ─────────────────►
   
   [1.Planner]   [2.Freeze]    [3.Drain]    [4.Handoff]    [5.Publish]
       │             │            │             │              │
       │             │            │             │              │
   决策 c: O→N    O停接新token   等旧token     O发cohort       发布
   分配 epoch e+1 路由器停发c    释放/超时     状态给N        ⟨N, e+1, owned⟩
                                              N安装锁表       到 owner_map
                  ┌─────────────┴───────────────┴──────────────┐
                  │      transferring 状态                       │
                  │      (no new token granted on c)             │
                  └─────────────────────────────────────────────┘
                  
                                           ╳ 线性化点在这里

5.2 每阶段的关键动作

阶段在哪干啥耗时
1 PlannerRouter决定 c: O→N，分配 e+11 ms
2 FreezeRouter → memcached把 owner_map[c] 改成 ⟨O, e+1, transferring⟩，路由器停发1 ms
3 DrainO 本地等 outstanding token 释放或超时 abort5–50 ms ← 最慢
4 HandoffO → NRDMA 发 cohort 状态（成员 + 统计 + 空锁表）~10 μs
5 PublishRouter → memcached发布 ⟨N, e+1, owned⟩1 ms

🌟 结论：Drain 是 4 阶段里最慢的一步——取决于事务最长执行时间。这是 C_move（第 6 章）的主要来源。

🧠 关键洞察：Drain 不能跳过——否则旧 token 仍在 O 上活，新事务在 N 上拿到 token，两个事务可能 commit 同一 cohort 的写。这就是 I3 的工程对应。

5.3 失败处理：宁可保 transferring 也不能激活双权威

   if any step fails AND can't confirm old token drained:
       → leave cohort in TRANSFERRING state OR downgrade to FALLBACK
       → 禁止: 直接激活新 owner

🌟 结论：失败的优先级是”安全 > 进展”——TRANSFERRING 状态可以一直停留（事务全部 abort 重试或走 fallback），但绝不能违反 I1。

6. 线性化点：第 7 行 owner map 发布

6.1 什么是线性化点

线性化点 = 协议从外部观察”迁移生效”的瞬间。

🌟 AURA 的线性化点：第 5 步 Publish 时把 owner_map[c] 改成 ⟨N, e+1, owned⟩ 这一瞬间。

6.2 线性化点的意义

                       线性化点
                          │
   ──────时间──────►──────╳──────►
   
   线性化点之前：           线性化点之后：
   - N 没有 token            - 任何 epoch=e 的 token 在 ValidateAuthority 失败
   - O 上的 epoch=e token   - 新事务从 N 拿到 epoch=e+1 的 token
     仍能 commit (drained)  - O 的 OwnerLockTable[c] 已清空
   - 新事务等待 transferring
     或 fallback

6.3 为什么不是更早的步骤

  • Step 1 决策时：还没有 epoch 升级，没生效
  • Step 2 Freeze：epoch 升了但 N 还没就位，新事务被 stall 但不能进展
  • Step 4 Handoff：N 装好锁表了但 owner_map 还没改，事务读 owner_map 仍看到 O
  • Step 5 Publish：外部第一次看到 N 是 owner ← 这是线性化点

🧠 关键洞察：线性化点选在”全局可见的 owner_map 切换” —— 因为 owner_map 是所有事务的 ground truth。

📎 工程踩坑视角：模块十五第 14 章 §6 InstallCohort 幂等性陷阱本质就是”线性化点之前/之后状态混了”。

7. §4.6 一致性论证草图（4 段 paragraph proof）

论文 §4.6 给的”一致性论证草图”是 4 个 paragraph，每段证一个性质。reviewer 必看，自己也得能复述。

7.1 P1：单 cohort 内不会双授权

论据：

  • 若 mode = OWNED → 事务伪代码第 4–5 行强制走 owner，第 6 行 MN CAS 被禁
  • 若 mode = FALLBACK → owner 本地锁表不授予 token，权威退回 MN CAS
  • 若 mode = TRANSFERRING → 第 7 行拒绝新 token，旧 owner 只 drain

🌟 结论：同一 epoch 内不存在 “owner lock 与 MN CAS 同时成功裁决同一 cohort” 的执行。这证明 I1。

7.2 P2：迁移不会产生新旧 owner 并发授权

论据：

  • Transfer 伪代码第 2 行先升级到 transferring + 递增 epoch
  • 第 4 行要求 O 冻结并 drain
  • 第 7 行才发布 N 为 owner（线性化点）
  • 任何在旧 epoch 拿到的 token，commit 前 ValidateAuthority 会被 epoch 检查拒绝

🌟 结论：线性化点之前 N 不授权，之后旧 epoch token 不能 commit。这证明 I2 + I3。

7.3 P3：跨 cohort 事务不会死锁

论据：

  • 事务按全局 cohort_id 升序加锁（伪代码第 3 行）
  • OwnerRpc 也按相同顺序 batch 处理
  • 不存在 T1 持 c_a 等 c_b、T2 持 c_b 等 c_a 的环
  • 若发现新写 key，不强行插入更小 id 的 cohort，而是 abort 重试

🌟 结论：全局序排除环 → 不会死锁。

7.4 P4：隔离级别继承

论据：

  • 上述 P1–P3 保证每个写数据项有唯一 owner 锁服务
  • 数据读写、日志、版本验证、commit 可见性 100% 复用底层 DM 系统
  • 因此底层在远端锁路径上提供的隔离级别（CREST 是 SR），AURA 不降低

🌟 结论：AURA 在无故障 + 读写集合可知或可安全重试的前提下，不降低底层隔离级别。这就是 I4 在隔离级别上的体现。

7.5 4 段证明的关系

   P1 单 cohort 不双授权 ─┐
                          │
   P2 迁移不双授权 ───────┤── 推出 → 每个写记录的"加锁权威唯一"
                          │
   P3 不死锁 ─────────────┤
                          │
                          ▼
                  P4 隔离级别继承
                  （不退化底层 SR/SI）

🌟 结论：P1+P2+P3 共同保证”加锁权威唯一”，P4 把”加锁权威唯一”翻译成”隔离级别不退化”。

🧠 关键洞察：AURA 不证明 SR/SI 本身——它把 SR/SI 的证明留给底层 CREST/Motor。它只证明”AURA 的修改没破坏 SR/SI 的前提”。这是工程上的”最小承诺”，但 reviewer 接受。

8. Corner case：owner CN 在 drain 中途 crash

最常被 reviewer 问的 corner case：如果 owner CN 在 drain 阶段（步骤 3）挂掉怎么办？

8.1 故障状态分析

   时间线：
   t0: Planner 决策 O→N, epoch e+1
   t1: owner_map[c] = ⟨O, e+1, transferring⟩
   t2: O 开始 drain，等 outstanding token 释放
   t3: O 突然 crash！（在 drain 中）
       此时状态：
       - epoch=e 的 outstanding token 仍可能在事务中（绕不掉）
       - N 还没就位
       - owner_map 是 transferring
       - 没人确认 token 是否 drain 完

8.2 防御策略：保 transferring 或 downgrade fallback

on_cn_crash(O):
    for each cohort c owned by O:
        if owner_map[c].mode == OWNED:
            owner_map[c].mode = FALLBACK   // 退回 MN CAS
            owner_map[c].epoch += 1        // 强制旧 token invalidate
        elif owner_map[c].mode == TRANSFERRING:
            // 还在迁移中：留 transferring 或 fallback
            // 关键：不能直接激活新 owner，因为不能确认旧 token drain 完
            if can_confirm_old_tokens_completed():
                proceed_to_publish_new_owner()
            else:
                owner_map[c].mode = FALLBACK
                owner_map[c].epoch += 2    // 跨过 transferring epoch

🌟 结论：遇到 owner crash 的安全路径是退回 fallback——MN CAS 是 always-correct 的”地板”。第一版 AURA 假设无故障，但容错版本会按这个规则做。

8.3 为什么 epoch 加 2 跨过 transferring

   原 epoch: e (owned)
   crash 时 transferring 用了 e+1
   退回 fallback 时 epoch = e+2
   
   原因：epoch=e+1 的 token 可能在事务中
        epoch=e+2 让旧 epoch 的 token 全部失效

📎 工程踩坑视角：模块十五第 7 章讨论过 AdaptX 折叠 AURA 的故障路径——本节 §8.2 是它的迁移版。

✅ 自我检验清单

  • AcquireAuthority + ValidateAuthority：能解释这两个接口怎么分工 + 怎么实现 I2
  • 事务伪代码 4 分支：能徒手写 owned-local / owned-remote / fallback / transferring 的代码分支
  • 按 cohort_id 排序：能解释为什么按全局 id 加锁能防死锁
  • 本地快路径 7 步：能徒手写 + 解释每步唯一改变了什么（步骤 3）
  • OwnerRpc 协议：能画 RequestToken / ReleaseToken 时序 + 解释为什么走 TCP
  • 权威唯一性规则：能讲 violation corner case + 防御
  • 4 阶段时序：能画 freeze-drain-handoff-publish 时序图 + 每阶段耗时
  • 线性化点：能解释为什么选 Publish 那一步 + 为什么不是更早
  • 4 段证明 P1–P4：能复述每段的论据 + 它证明 I1/I2/I3/I4 哪一条
  • owner crash corner case：能讲清 transferring 中途 crash 的 epoch+2 退 fallback 策略

第 8 章预告

第 8 章按论文 §5 + v25 工程实现展开 Router-Centric 实现细节：

  • Manifest v1 vs v2 wire format
  • 9216 cohort 全表展开
  • v25 access-graph cohort planner 实测结果
  • Lever B 的反直觉负结果 + record_key reshape 方法论
  • “Lever ordering matters” 的可推广教训

读完第 8 章你能讲清楚 “为什么 v25 cohort planner 实测半步走到位 + Lever B 为什么 collapse”。

📚 参考资料

论文原文

分布式系统经典

  • Linearizability (Herlihy & Wing, 1990) —— 线性化点概念奠基
  • Two-Phase Commit / Three-Phase Commit —— freeze-drain-handoff 协议的远房表亲
  • Raft Joint Consensus —— epoch + handoff 范式的另一案例

模块内交叉引用