S-Bus: Reconstrução Automática de Conjunto de Leitura para Coordenação de Estado de LLM Multiagente

Resumo

Agentes LLM concorrentes que compartilham estado mutável em linguagem natural produzem Condições de Corrida Estruturais (Structural Race Conditions – SRCs): conflitos de escrita-escrita e de leitura desatualizada entre shards que corrompem silenciosamente a saída dos agentes. Os frameworks multiagentes existentes (LangGraph, CrewAI, AutoGen) não fornecem semânticas de propriedade de escrita sobre o estado compartilhado. Apresentamos o S-Bus, um middleware HTTP cujo mecanismo central é um DeliveryLog no servidor: um log por agente de operações HTTP GET que reconstrói automaticamente o conjunto de leitura de cada agente no momento do commit, sem alterações no SDK dos agentes, sob HTTP/1.1. A propriedade de consistência que o DeliveryLog fornece — Isolamento de Leitura Observável (Observable-Read Isolation – ORI), uma consistência causal parcial sobre a projeção observável por HTTP do conjunto de leitura — previne condições de corrida estruturais quando agentes colaboram por meio de shards compartilhados. Três contribuições: (C1) O mecanismo DeliveryLog para reconstrução automática do conjunto de leitura baseada em tráfego HTTP, com evidência mecanizada em três níveis: ReadSetSoundness e ORICommitSafety verificadas por máquina em TLAPS (módulo um axioma de tipagem retido); TLC exaustivo em N=3 (20.763.484 estados distintos, zero violações); Dafny descarrega 9 lemas indutivos de solidez. (C2) Paridade empírica de prevenção de conflitos estruturais em relação ao PostgreSQL 17 SERIALIZABLE e ao Redis 7 WATCH/MULTI em varreduras de contenção de shards compartilhados com 427.308 conflitos HTTP-409 ativos: zero corrupções do Tipo I em todos os três backends. (C3) O envelope operacional da ORI é condicionado à topologia: semanticamente neutro em cargas de trabalho com shards dedicados; prejudicial em escrita colaborativa de shard único porque a preservação propaga contradições concorrentes. Código-fonte: 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