S-Bus : Reconstruction automatique d'ensembles de lecture pour la coordination d'état de LLM multi-agents

Résumé

Des agents LLM concurrents partageant un état mutable en langage naturel produisent des conditions de concurrence structurelles (SRC) : des conflits d'écriture-écriture et de lecture obsolète inter-shard qui corrompent silencieusement la sortie des agents. Les cadres multi-agents existants (LangGraph, CrewAI, AutoGen) ne fournissent pas de sémantique de propriété d'écriture sur l'état partagé. Nous présentons S-Bus, un middleware HTTP dont le mécanisme central est un DeliveryLog côté serveur : un journal par agent des opérations HTTP GET qui reconstruit automatiquement l'ensemble de lectures de chaque agent au moment de la validation sans modification du SDK de l'agent sous HTTP/1.1. La propriété de cohérence que fournit le DeliveryLog — l'isolement de lecture observable (ORI), une cohérence causale partielle sur la projection observable via HTTP de l'ensemble de lectures — empêche les conditions de concurrence structurelles lorsque les agents collaborent via des shards partagés. Trois contributions : (C1) Le mécanisme DeliveryLog pour la reconstruction automatique de l'ensemble de lectures basée sur le trafic HTTP, avec une preuve mécanisée à trois niveaux : ReadSetSoundness et ORICommitSafety vérifiées par machine dans TLAPS (modulo un axiome de typage retenu) ; TLC exhaustif à N=3 (20 763 484 états distincts, zéro violation) ; Dafny décharge 9 lemmes de solidité inductive. (C2) Parité empirique de prévention des conflits structurels par rapport à PostgreSQL 17 SERIALIZABLE et Redis 7 WATCH/MULTI sur des balayages de contention de shard partagé avec 427 308 conflits HTTP-409 actifs : zéro corruption de type I sur les trois backends. (C3) Le domaine d'opération d'ORI est conditionné par la topologie : sémantiquement neutre dans les charges de travail avec shards dédiés ; nuisible dans l'écriture collaborative sur un seul shard car la préservation propage les contradictions concurrentes. Code source : 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