S-Bus：面向多智能体 LLM 状态协调的自动读集重建 S-Bus: Automatic Read-Set Reconstruction for Multi-Agent LLM State Coordination

完整步骤如下。①读阶段：智能体 $\alpha$ 发 GET /shard/:key?agent_id=X，服务端在持同一 Mutex 的情况下写入 DeliveryLog 条目 $(k, \text{reg}[k].v)$ 再返回响应（A1 完整性）。②提交阶段：智能体发 POST /commit/v2 携带 $(k, v_e, \delta, \alpha)$；ACP 第 1 行调用 DeliveryLog.buildEffRS 构建有效读集 $\hat{R} = R_{explicit} \cup \text{session-deliveries}$（显式条目优先；可选 ARSI 模式声明全集）；第 2 行加 RwLock 写锁；第 3–6 行遍历 $\hat{R}$ 中所有 $k' \neq k$，若 $\text{reg}[k'].v \neq v'$ 返回 CROSSSHARDSTALE；第 7 行校验本键版本 $\text{sk}.v = v_e$，不等返回 VERSIONMISMATCH；第 9 行在 token Mutex 下插入所有权令牌；第 10 行写入内容 $\text{sk}.c \leftarrow \delta$、自增版本、追加 WAL；RAII 释放写锁返回新版本。③冲突恢复：被拒智能体重新 GET、重生成增量、再提交。分布式部署下所有变更经 Raft leader 串行化（满足 A3），follower 按日志顺序 apply，保证跨节点提交顺序一致。

技术新颖性有三层。其一，DeliveryLog 把分布式数据库里的 COPS 因果日志'裁剪'到多智能体 LLM 场景：只跟踪 per-session 的标量 HTTP GET，不做系统级向量时钟，却足以做 OCC 校验。其二，ORI 作为投影一致性性质的精确定位：通过反例历史证明，在 $R_{obs}$ 投影上 ORI 严格介于 Read-Committed 与 Snapshot Isolation 之间——阻止 G2-item（RC 不能阻止）、却允许 $R_{hidden}$ 上的 write-skew（SI 不允许）。其三，三层机械化证据的组合（TLAPS 任意 $N$ 的 687 个义务 + TLC 穷举 $N\le4$ 共 2080 万状态 + Dafny 9 个归纳引理）是短于 IronFleet 全精化但超出工业常规（TiDB/CockroachDB/etcd 仅发 TLA+ 规约不做精化）的验证深度。作者诚实地把实现到 Rust 源码的精化标注为'经验性而非机械化'，并保留一个基础类型公理 FUNTYPINGRECONSTRUCTION 未消解。

独立分析弱点与改进方向：①负载泛化窄——主评测全在 SWE-bench 派生的 Python 协调任务（10 域），WORKLOAD-B 虽补了数据管道规划（8 域）但每域分歧率高度均匀（91%–94%），更像 harness 形状而非领域语义，文档撰写、RAG 编排、智能体规划等类别未覆盖；改进方向是构建 typed-shard 基准（作者已列入 §11.4）。②语义质量评判脆弱——依赖单一 GPT-4o-mini 判官，跨家族 κ=0.46，SJ-v4 语义 rubric 仍未对人类做 IAA，且出现反直觉的 fresh>stale 损坏；改进方向是 100 项人类 IAA 研究并测试位置/长度偏置。③$R_{hidden}$ 闭环不完整——PH-3 的 analyst-LLM 语义抽取（0.59 召回）只在 $p_{hidden}=0.074$ 单智能体负载上验证，未迁移到 $p_{hidden}=0.739$ 多智能体；改进方向是把 analyst-LLM 嵌入 LLM-API 代理（Limitation 16）。④并发故障转移窗口——约 5 ms 的 fire-and-forget 复制窗口未覆盖，虽有量级估计 $\lesssim5\times10^{-3}$ 期望违规/agent-day，但安全攸关场景不应容忍任何窗口；改进方向是同步复制或 Raft-TLAPS 精化。⑤默认 $K=5$ 重试预算在高 $N$ 共享分片下不足（$N=16$ 需 $K\ge19$，$N=32$ 需 $K\ge28$）， practitioner 必须手动调参，缺少自适应。⑥自报告真值污染——所有召回数都是对自报告的上界，真因果读覆盖 $\le70\%$ 的口径需要在摘要里更显眼。

作者明确四向。①A-BUS 自适应路由：针对单分片协作写（ORI 有害拓扑），设计 additive_hint 布尔声明 + 分类器（DEDICATED / CONTENDED_COMMUTATIVE / CONTENDED_NON-COMMUTATIVE）+ 三策略合并引擎（结构按区替换、追加拼接、LLM 语义合并兜底），preliminary 实现已开源（github.com/sajjadanwar0/abus）。②Raft-TLAPS 机械化：把 TLC 抽象（24.7 万状态）升级为 IronFleet 式精化，估计 6–12 人月，是期刊扩展版的主攻方向。③PH-2 语义抽取迁移：把 analyst-LLM 挂到多智能体负载，工程量 + 约 $50 API 花费每格。④typed-shard 基准重建，消除 8.5% 的跨分片交叉标注。基于成果可延伸的方向：把 ORI 投影一致性框架推广到更多隔离级别（用代理语义抽取逐步把 $R_{hidden}$ 纳入投影 $\pi$）；探索与 CRDT（Automerge、Loro、Yjs）的混合部署——加性分片用 CRDT、互斥分片用 OCC；把 DeliveryLog 被动读集重建思路迁移到非 LLM 的微服务协调；与 Temporal/Golem 等持久化执行引擎的 Update API 对比，量化 ORI 跨分片读集推断的额外价值。

复现评估较高。代码已开源（https://github.com/sajjadanhar0/sbus 及 sbus-formals、sbus-experiments 仓库），ACP 核心约 950 行安全 Rust，含 Raft 的完整系统 1,679 行、零 unsafe 块，依赖 openraft 0.8.4 + sled 持久化 + Tokio 1.44 + Axum 0.8.4。形式化工件齐全：SBus_TLAPS_v16.tla、SBus_ori.tla、SBus_Distributed.tla、sbus_lemmas_v4.dfy 均释出。实验脚本（pg_bench_full.py、pg_comparison.py、exp_proxy_ph2*.py、exp_adversarial_rhidden_v2.py、run_llm_judges.py、score_annotations.py）及标注 CSV（first.csv、second_human_annotator.csv）可审计。硬件门槛低：主实验在单台 AWS Lightsail 2 vCPU/8 GB 上即可跑。复现难点：①依赖 OpenAI/Anthropic/Google API 花费与随机性（worker temperature 0.3）；②三后端对比需额外起 PostgreSQL 17、Redis 7；③人类标注（Zahid Hussain）不可完全复制，但 400 对样本 CSV 可审计、κ=0.93 可复核；④TLAPS 证明需特定 tlapm 1.5 环境，保留公理需读者自行判断。总体可复现性在系统论文中属上游，形式化与实验双工件齐备。