S-Bus: Automatische Read-Set Reconstructie voor Multi-Agent LLM Toestandcoördinatie

Samenvatting

Gelijktijdige LLM-agenten die veranderlijke natuurlijke-taaltoestand delen, veroorzaken Structurele Racecondities (SRC's): schrijf-schrijf- en cross-shard verouderde-leesconflicten die de uitvoer van agenten stilzwijgend beschadigen. Bestaande multi-agent frameworks (LangGraph, CrewAI, AutoGen) bieden geen schrijfeigendomssemantiek voor gedeelde toestand. We presenteren S-Bus, een HTTP-middleware waarvan het centrale mechanisme een server-side DeliveryLog is: een per-agent log van HTTP GET-operaties die automatisch de leesset van elke agent op commit-tijd reconstrueert, zonder aanpassingen aan de agent-SDK, onder HTTP/1.1. De consistentie-eigenschap die de DeliveryLog biedt – Observable-Read Isolatie (ORI), een partiële causale consistentie over de HTTP-waarneembare projectie van de leesset – voorkomt structurele racecondities wanneer agenten samenwerken via gedeelde shards. Drie bijdragen: (C1) Het DeliveryLog-mechanisme voor automatische, op HTTP-verkeer gebaseerde leessetreconstructie, met drielaags mechanisch bewijs: ReadSetSoundness en ORICommitSafety machine-geverifieerd in TLAPS (op één behouden typeringsaxioma na); uitgebreide TLC op N=3 (20.763.484 verschillende toestanden, nul overtredingen); Dafny bewijst 9 inductieve correctheidslemma's. (C2) Empirische pariteit in preventie van structurele conflicten ten opzichte van PostgreSQL 17 SERIALIZABLE en Redis 7 WATCH/MULTI bij gedeelde-shard-contentiesweeps met 427.308 actieve HTTP-409 conflicten: nul Type-I-corrupties voor alle drie de backends. (C3) ORI's operationele bereik is topologie-afhankelijk: semantisch neutraal in workloads met speciale shards; schadelijk bij gezamenlijk schrijven op een enkele shard omdat het behoud gelijktijdige tegenstrijdigheden propageert. Broncode: 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