S-Bus: Автоматическая реконструкция множества чтения для координации состояний многоагентных LLM

Аннотация

Параллельные LLM-агенты, совместно использующие изменяемое естественно-языковое состояние, порождают структурные состояния гонки (Structural Race Conditions, SRC): конфликты записи-записи и устаревшего чтения между шардами (cross-shard stale-read conflicts), которые незаметно искажают вывод агентов. Существующие мультиагентные фреймворки (LangGraph, CrewAI, AutoGen) не предоставляют семантики владения записью над разделяемым состоянием. Мы представляем S-Bus — HTTP-промежуточное ПО, центральным механизмом которого является серверный DeliveryLog: поагентый журнал HTTP-операций GET, который автоматически восстанавливает набор чтения каждого агента на момент фиксации без изменений в SDK агентов под HTTP/1.1. Свойство согласованности, обеспечиваемое DeliveryLog — Изоляция наблюдаемого чтения (Observable-Read Isolation, ORI), частичная причинно-следственная согласованность над проекцией набора чтения, наблюдаемой через HTTP, — предотвращает структурные состояния гонки при сотрудничестве агентов через общие шарды. Три вклада: (C1) Механизм DeliveryLog для автоматического восстановления набора чтения на основе HTTP-трафика с трехуровневым механизированным доказательством: корректность набора чтения (ReadSetSoundness) и безопасность фиксации на основе ORI (ORICommitSafety), проверенные на машине в TLAPS (с сохранением одной аксиомы типизации); исчерпывающий TLC при N=3 (20 763 484 различных состояний, ноль нарушений); Dafny разряжает 9 индуктивных лемм о корректности. (C2) Эмпирическая паритетность предотвращения структурных конфликтов по сравнению с PostgreSQL 17 SERIALIZABLE и Redis 7 WATCH/MULTI при прогонах конкуренции за общие шарды с 427 308 активными конфликтами HTTP-409: ноль повреждений типа I на всех трёх бэкендах. (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