S-Bus: 面向多智能体大语言模型状态协调的自动读集合重构

摘要

并发LLM代理共享可变自然语言状态会导致结构竞争条件(SRCs)：写-写冲突和跨分片过时读冲突，这些冲突会悄然破坏代理输出。现有的大多数多代理框架(LangGraph、CrewAI、AutoGen)在共享状态上不提供写所有权语义。我们提出S-Bus，这是一个HTTP中间件，其核心机制是服务器端的DeliveryLog：每个代理维护一个HTTP GET操作日志，在提交时自动重建每个代理的读集，无需在HTTP/1.1下修改代理SDK。DeliveryLog提供的一致性属性——可观测读隔离(ORI)，一种对读集的HTTP可观测投影的部分因果一致性——在代理通过共享分片协作时防止了结构竞争条件。三项贡献：(C1) DeliveryLog机制，用于基于HTTP流量自动重建读集，并附带三层机制化证据：在TLAPS中经机器检查的读集可靠性和ORI提交安全性（除一个保留的类型公理外）；在N=3时经TLC穷举验证(20,763,484个不同状态，零违规)；Dafny验证了9个归纳可靠性引理。(C2) 在427,308个活跃HTTP-409冲突的共享分片竞争扫描中，与PostgreSQL 17 SERIALIZABLE和Redis 7 WATCH/MULTI相比，实现了实证的结构冲突预防对等性：三个后端均无第一类破坏。(C3) ORI的运行范围是拓扑条件相关的：在专用分片工作负载中语义中性；在单分片协作写入时有害，因为保留机制会传播并发矛盾。源代码：https://github.com/sajjadanwar0/sbus

English

Concurrent LLM agents sharing mutable natural-language state produce Structural Race Conditions (SRCs): write-write and cross-shard stale-read conflicts that silently corrupt agent output. Existing multi-agent frameworks (LangGraph, CrewAI, AutoGen) provide no write-ownership semantics over shared state. We present S-Bus, an HTTP middleware whose central mechanism is a server-side DeliveryLog: a per-agent log of HTTP GET operations that automatically reconstructs each agent's read set at commit time without agent SDK changes under HTTP/1.1. The consistency property the DeliveryLog provides -- Observable-Read Isolation (ORI), a partial causal consistency over the HTTP-observable projection of the read set -- prevents structural race conditions when agents collaborate via shared shards. Three contributions: (C1) The DeliveryLog mechanism for automatic HTTP-traffic-based read-set reconstruction, with three-tier mechanised evidence: ReadSetSoundness and ORICommitSafety machine-checked in TLAPS (modulo one retained typing axiom); exhaustive TLC at N=3 (20,763,484 distinct states, zero violations); Dafny discharges 9 inductive soundness lemmas. (C2) Empirical structural-conflict prevention parity against PostgreSQL 17 SERIALIZABLE and Redis 7 WATCH/MULTI on shared-shard contention sweeps with 427,308 active HTTP-409 conflicts: zero Type-I corruptions across all three backends. (C3) ORI's operating envelope is topology-conditional: semantically neutral in dedicated-shard workloads; harmful in single-shard collaborative writing because preservation propagates concurrent contradictions. Source code: https://github.com/sajjadanwar0/sbus