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

摘要

並行的LLM代理共享可變的自然語言狀態會產生結構競爭條件：寫-寫衝突和跨分片過時讀取衝突會悄悄破壞代理輸出。現有的多代理框架（LangGraph、CrewAI、AutoGen）對共享狀態缺乏寫所有權語義。我們提出S-Bus，這是一個HTTP中介軟體，其核心機制是伺服器端的DeliveryLog：每個代理的HTTP GET操作日誌，能在提交時自動重建每個代理的讀取集，無需在HTTP/1.1下修改代理SDK。DeliveryLog提供的一致性屬性——可觀察讀取隔離（ORI），一種對HTTP可觀察投影讀取集的部分因果一致性——能防止代理通過共享分片協作時的結構競爭條件。我們有三項貢獻：(C1) DeliveryLog機制實現了基於HTTP流量的自動讀取集重建，並提供三層機械化證據：在TLAPS中（除一個保留的類型公理外）經機器驗證的ReadSetSoundness和ORICommitSafety；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