S-Bus: Automatische Lese-Set-Rekonstruktion für die Zustandskoordination von Multi-Agenten-LLMs

Zusammenfassung

Gleichzeitige LLM-Agenten, die einen veränderlichen natürlichsprachlichen Zustand teilen, erzeugen strukturelle Wettlaufsituationen (Structural Race Conditions, SRCs): Schreib-Schreib- und shardübergreifende veraltete Lese-Konflikte, die die Agentenausgabe stillschweigend korrumpieren. Bestehende Multi-Agenten-Frameworks (LangGraph, CrewAI, AutoGen) bieten keine Schreib-Eigentumssemantik für gemeinsamen Zustand. Wir präsentieren S-Bus, eine HTTP-Middleware, deren zentraler Mechanismus ein server-seitiges DeliveryLog ist: ein agentenspezifisches Log von HTTP-GET-Operationen, das automatisch den Lese-Satz jedes Agenten zum Commit-Zeitpunkt rekonstruiert, ohne Änderungen am Agenten-SDK unter HTTP/1.1. Die Konsistenzeigenschaft, die das DeliveryLog bereitstellt – Observable-Read Isolation (ORI), eine partielle kausale Konsistenz über die HTTP-beobachtbare Projektion des Lese-Satzes – verhindert strukturelle Wettlaufsituationen, wenn Agenten über gemeinsame Shards zusammenarbeiten. Drei Beiträge: (C1) Der DeliveryLog-Mechanismus zur automatischen, auf HTTP-Datenverkehr basierenden Rekonstruktion des Lese-Satzes, mit maschineller Evidenz auf drei Ebenen: ReadSetSoundness und ORICommitSafety maschinengeprüft in TLAPS (bis auf ein beibehaltenes Typisierungsaxiom); erschöpfendes TLC bei N=3 (20.763.484 verschiedene Zustände, null Verstöße); Dafny erledigt 9 induktive Korrektheitslemmata. (C2) Empirische strukturelle Konfliktvermeidungsgleichheit gegenüber PostgreSQL 17 SERIALIZABLE und Redis 7 WATCH/MULTI bei Gemeinschafts-Shard-Konkurrenzdurchläufen mit 427.308 aktiven HTTP-409-Konflikten: Null Typ-I-Korrumpierungen über alle drei Backends hinweg. (C3) Der Betriebsbereich von ORI ist topologieabhängig: semantisch neutral bei dedizierten Shard-Workloads; schädlich bei gemeinschaftlichem Schreiben auf einem einzelnen Shard, da die Erhaltung gleichzeitige Widersprüche propagiert. Quellcode: 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