https://arxiv.org/api/AOdWLs0mlNk8FDpdVb0UG+V/gbQ 2026-07-18T22:05:00Z 29328 15 15 http://arxiv.org/abs/2604.20032v2 LEO: Tracing GPU Stall Root Causes via Cross-Vendor Backward Slicing 2026-07-15T22:02:45Z More than half of the Top 500 supercomputers employ GPUs as accelerators. On GPU-accelerated platforms, developers face a key diagnostic gap: profilers show source lines where stalls occur, but not why they occur. Furthermore, the same kernel may have different stalls and underlying causes on different GPUs. This paper presents LEO, a root-cause analyzer for NVIDIA, AMD, and Intel GPUs that performs backward slicing from stalled instructions, considering dependencies arising from registers as well as vendor-specific synchronization mechanisms. LEO attributes GPU stalls to source instructions with the goal of explaining root causes of these inefficiencies. Across 21 workloads on three GPU platforms, LEO-guided optimizations deliver geometric-mean speedups of 1.73$\times$--1.82$\times$. Our case studies show that (1) the same kernel may require different optimizations for different GPU architectures, and (2) LEO's structured diagnostics improve code optimization with large language models relative to code-only and raw-stall-count baselines. 2026-04-21T22:23:55Z Manuscript accepted at SC'26 Yuning Xia John Mellor-Crummey http://arxiv.org/abs/2607.12121v2 FlashDiff: Efficient Regional Execution and Scheduling for Diffusion Model Serving 2026-07-15T22:00:17Z Diffusion models have become the central backbone for modern image, video, and audio generation, but their efficient service remains a challenge. Unlike autoregressive decoding, diffusion inference repeatedly updates high-dimensional spatial or temporal latents over many denoising steps. This all-region execution pattern makes generation latency high and limits serving throughput. Existing multi-GPU parallelization methods can reduce per-step computation, but often introduce substantial activation exchange overhead, causing communication to offset or even outweigh the benefits of parallel execution. This paper presents FlashDiff, a diffusion serving system that improves inference efficiency through adaptive regional execution and scheduling. FlashDiff is based on the observation that diffusion refinement is not uniform across latent regions or denoising steps: different regions often stabilize at different rates, while neighboring steps exhibit strong temporal correlation. FlashDiff leverages these properties to selectively execute only regions that require further refinement and to reallocate the resulting compute slack across concurrent serving requests. FlashDiff consists of three mechanisms. First, it decomposes the latent representation into coherent execution regions using early-stage attention signals, preserving semantic structure while exposing fine-grained parallelism. Second, it uses a lightweight runtime controller to estimate region activity and bypass low-impact updates when further refinement is unlikely to affect output quality. Third, it applies an affinity-aware online scheduler that co-locates dependent regions, balances residual load across GPUs, and reuses reclaimed compute capacity to improve serving efficiency. Across real-world image, video, and audio workloads, FlashDiff reduces end-to-end serving latency by 30-97% and improves throughput by 1.2-2.2x. 2026-07-13T20:00:39Z Yaqi Qiao Ping He Songrun Xie Ayush Barik Chensong Zhang Zhengzhong Tu Fan Lai http://arxiv.org/abs/2606.17288v2 Local Fault Repair of Perfect Resource Placements in Eisenstein--Jacobi Networks 2026-07-15T21:37:36Z Perfect resource placements in dense Eisenstein--Jacobi (EJ) networks partition the network into hexagonal radius-$t$ service cells. This paper studies local repair of such placements after resource failures. For one failed resource, we prove that one replacement cannot cover the failed hexagon and two always suffice, giving $ρ_{\mathrm{EJ}}(t)=2$ for all $t\ge1$. Among minimum-size repairs, the sharp minimum-overlap formula $Ω_{\mathrm{EJ}}(t)=t^2$ follows from the three-strip geometry of EJ balls. For two failed resources, independent repair gives a four-replacement upper bound, but unlike the Gaussian case EJ repair is not always additive: two infinite neighboring displacement families admit three-replacement repairs, proved optimal by a two-ball impossibility argument. Additive behavior is established algebraically via endpoint-rigidity and diagonal-corridor theorems. For $q$ failed resources, independent canonical repair gives a universal $2q$ upper bound, exact when failed cells are pairwise more than $4t$ apart. Dense cluster subadditivity is proved for infinite four-fault and six-fault families with exact repair numbers four and five, giving savings of four and seven over independent repair. An exact inclusion--exclusion identity governs repeated coverage for arbitrary multi-fault repairs. An audit over 19,400 instances confirms widespread subadditivity. EJ local repair is structurally distinct from the Gaussian case: the one-fault overlap is quadratic, two-fault repair can be non-additive, and clustered repairs reuse replacement balls across multiple failed cells. 2026-06-15T20:52:58Z Preprint also available on Zenodo:https://doi.org/10.5281/zenodo.20690942 Bader Albader http://arxiv.org/abs/2606.01183v6 The World's Fastest Matching Engine Algorithm 2026-07-15T14:55:28Z We drove 247 matching engines through one C-ABI harness on one identical workload: every open-source FIFO implementation we could find, deduplicated, and our own, on the same gate. The workload doubles as a byte-identical correctness oracle - 1,000,000,000+ order messages per engine, replayed against an independent-engine consensus. Only 47 are correct as shipped; we filed 181 GitHub issues upstream, 18 already fixed by their maintainers, none declined. Our engine leads the 160 that reproduce the consensus by ~25 M/s - 4x the second best - on worst-case throughput. One core sustains 33.2 million order messages per second at sub-microsecond median latency; a 96-core server (~$1,630/month) sustains ~640 million/s across 10,000 symbols, over 20x the CTA quote feed's capacity. The lead is structural: the 52 engines written inside the trading industry sit under the same 8.19 M/s ceiling as the rest of the field. Every classical book - linked lists in a balanced tree - pays a pointer chase and a root-to-leaf search per operation. We eliminate both: the Priority-Indicated Node (PIN) resolves insertion in O(1) from priority indicators, not O(log n) comparisons; a neighbor-aware balanced tree splices or removes a price level in O(1) writes from the in-order neighbors electronic trading already supplies. 2026-05-31T11:51:22Z 19 pages, 3 figures, 6 tables Jake Yoon http://arxiv.org/abs/2509.11076v2 SmartSwap: Swap-Based Memory Optimization for LLM Training under Varying Operator Sequences 2026-07-15T13:51:17Z The increasing size of large language models (LLMs) has led to a surge in memory requirements during training, often exceeding the capacity of high-bandwidth memory (HBM). Swap-based memory optimization incurs neither accuracy loss nor additional end-to-end overhead when effectively overlapped, thus being an attractive solution. However, existing swap methods assume consistent operator sequences, which is impractical in Eager Mode, where operator sequences can vary during change. We propose Chameleon, which redesigns the end-to-end process of swap-based memory optimization and is the first work to consider varying operator sequences in Eager Mode. Chameleon (i) introduces a lightweight online profiler to enable continuous profiling for monitoring operator sequences, (ii) generates effective swap policies with limited operator information, and (iii) optimizes the policy execution module for accurate policy application and better performance. Experimental results demonstrate that Chameleon reduces profiling overhead by 84.25%, enables training models up to 4x larger than hardware memory while adapting to changes in operator sequences, improves performance by up to 38.94% compared to recomputation or high-degree parallelism. 2025-09-14T03:55:03Z Accepted to DAC 2026. Previously titled "Chameleon: Taming Dynamic Operator Sequences for Memory-Intensive LLM Training." Zibo Wang Yuhang Zhou Zhibin Wang Shipeng Li Xinjing Huang Chendong Cai Bingxu Mu Yuqing Sun Zhiheng Hu Bin She Shu You Guanghuan Fang Rong Gu Wanchun Dou Guihai Chen Chen Tian http://arxiv.org/abs/2605.28333v2 High-Quality Multi-Constraint Hypergraph Partitioning via Greedy Rebalancing 2026-07-15T12:51:42Z Multi-constraint hypergraph partitioning is a generalization of balanced partitioning, where the vertex set of a hypergraph is partitioned such that the inter-block connectivity of hyperedges is minimized while balancing the vertices with regard to $d$ distinct constraints. A prominent class of applications is data distribution tasks, where this allows to achieve good load balance for $d$ different kinds of resources and simultaneously minimize the communication volume. Although the best approaches for single-constraint partitioning are usually complex (multilevel) algorithms with many components, we show that replacing only one component already leads to high-quality multi-constraint partitions: the rebalancing step, which restores balance for a partition that has (hopefully) small connectivity but violates the constraints. We design a multi-constraint rebalancing algorithm based on greedy local search, proving that balance is always restored for $d=2$ and bounded maximum weight. The key is to ensure monotonically decreasing global imbalance by choosing an imbalance metric where there is always a balance-improving move available. Integrating our algorithm into the state-of-the-art partitioner Mt-KaHyPar, we demonstrate an 11.5% geometric mean connectivity reduction compared to the next best competitor (Metis) and better reliability regarding partition balance, even though the majority of inputs is outside of the theoretical guarantee. 2026-05-27T11:36:57Z ESA 2026 Nikolai Maas http://arxiv.org/abs/2607.02529v2 RepliCore: Reproducible Parallel Simulation under Asynchronous Browser Runtimes 2026-07-15T12:40:26Z Browser-based simulations execute over asynchronous runtime mechanisms including event loops, rendering callbacks, and independently scheduled Web Workers, causing simulation progression to depend on runtime timing and callback scheduling behavior. RepliCore addresses this problem by separating asynchronous runtime progression from externally observable logical-state visibility. Runtime-visible simulation states are exposed only after logical-state progression becomes externally stable, preventing asynchronous runtime activities from observing partially updated simulation progression. The framework prevents rendering callbacks and asynchronous runtime tasks from observing transient intermediate logical states during parallel progression. This organization maintains consistency between parallel and sequential execution. Based on this model, we implement RepliCore, a browser-oriented deterministic parallel simulation framework for reproducible large-scale simulation under asynchronous browser runtimes. Experiments in real browser environments produce bitwise-identical outputs across varying worker configurations, scheduling conditions, and rendering frequencies while remaining practical for large-scale browser-oriented workloads. Additional ablation experiments show systematic state divergence after relaxing key execution constraints. These results indicate that reproducible asynchronous parallel simulation can be achieved through controlled logical-state visibility stabilization without relying on execution replay or explicit schedule control. 2026-05-28T09:22:46Z 14 pages, 2 figures, 5 tables Anqing Chen http://arxiv.org/abs/2607.13677v1 Local Certification of Vertex and Edge Connectivity 2026-07-15T10:18:36Z Local certification is a framework for verifying global graph properties using only local information. In this model, a prover assigns short labels, called certificates, to the vertices of a graph. Each vertex then exchanges certificates with its neighbors and performs a purely local check to determine whether the graph satisfies the desired property. This line of research has led to efficient certification schemes for a broad range of graph classes, including minor-closed families, topological graph classes, and graphs defined by forbidden subgraphs. In this paper, we study the local certification of graph connectivity. Prior work by Bousquet, Feuilloley, and Pierron (JPDC 2024) showed that $2$-vertex-connectivity, $2$-edge-connectivity, and $3$-vertex-connectivity admit $O(\log n)$-bit certificates, leveraging structural characterizations such as ear decompositions. We go substantially beyond these cases and investigate general $k$-vertex-connectivity and $k$-edge-connectivity. We develop new approaches that exploit connections between connectivity and combinatorial structures, including branchings, Eulerian subgraphs, and independent spanning trees. For $k$-edge-connectivity, we obtain an $O_k(\log n)$-bit certification scheme and prove a matching $Ω_k(\log n)$ lower bound for every $k\ge 3$. The lower bound also applies to $k$-vertex-connectivity. For $k$-vertex-connectivity, we obtain $\tilde{O}_k(\sqrt{n})$-bit certificates for every $k$ under a conjecture of Itai and Zehavi. We further show that, for $k=2$, the logarithmic barrier can be broken on sparse graph classes: $2$-edge-connectivity admits constant-size certificates in bounded-expansion graphs, and $2$-vertex-connectivity admits constant-size certificates in bounded-degree graphs. In contrast, for $2$-vertex-connectivity in general graphs, we prove an $Ω(\log(\log^\ast n))$-bit lower bound. 2026-07-15T10:18:36Z Abstract shortened to meet arXiv requirements Yi-Jun Chang Yi-Xuan Lee Meng-Tsung Tsai http://arxiv.org/abs/2607.14172v1 The Cost and Network Limits of Space-Based AI Compute 2026-07-15T09:42:59Z This paper evaluates whether large-scale AI data centers deployed in low-Earth orbit (LEO) could become a cost-effective alternative to terrestrial facilities. The analysis compares orbital and ground-based systems across launch cost, power generation, cooling, radiation exposure, and atmospheric reentry, as well as compute-network performance. A key distinction is the shift from terrestrial Clos networks to space-based mesh networks using laser inter-satellite links. Using bisection bandwidth, bisection intensity, and roofline-style models, we show that while LEO-based inference may be feasible, training frontier-scale LLMs in orbit is unlikely to be competitive with terrestrial data centers. 2026-07-15T09:42:59Z Kees van Berkel http://arxiv.org/abs/2607.13642v1 A Distributed Framework for Compiling and Reasoning with d-DNNF 2026-07-15T09:34:26Z Knowledge Compilation (KC) is a powerful paradigm that enables efficient reasoning by transforming propositional formulas into tractable target languages, such as Deterministic, Decomposable Negation Normal Form (d-DNNF). However, as real-world problem instances grow in complexity, the offline compilation phase becomes a significant computational bottleneck, often exceeding the memory and temporal limits of single-node systems. While distributed computing has been successfully applied to model counting ($\#\mathsf{SAT}$), extending these techniques to knowledge compilation remains a challenge due to the difficulty of sharing partial circuit fragments across distributed nodes. In this paper, we propose dkc, the first distributed knowledge compiler designed for large-scale Decision-DNNF generation. Leveraging a Cube-and-Conquer strategy, dkc effectively partitions the search space into independent subproblems, mitigating the communication overhead typically associated with work-stealing architectures in circuit-based tasks. Recognizing that the utility of compilation lies in subsequent querying, we further introduce dreasoner, a distributed reasoning engine. dreasoner is capable of performing core inference tasks (including model counting, direct access, and uniform sampling) across a distributed d-DNNF structure, even under variable conditioning. Our experimental evaluation on benchmarks demonstrates that our distributed architecture scales effectively, enabling the compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers. 2026-07-15T09:34:26Z Zhenghang Xu Minghao Yin jianan Wang Jean-Marie Lagniez http://arxiv.org/abs/2607.13634v1 gDMC: A Generic Distributed Model Counting Framework via Work-Stealing 2026-07-15T09:28:58Z Propositional Model Counting ($\#\mathsf{SAT}$) is essential for probabilistic reasoning but faces scalability limits on single cores. Existing distributed approaches struggle with high initialization overheads (static decomposition) or rigid architecture. We propose a novel, generic framework for distributed \emph{exact} model counting. Leveraging C++ templates, our architecture decouples parallel orchestration from solving logic, enabling state-of-the-art solvers to be parallelized with minimal modification. We implement an adaptive work-stealing strategy that ensures effective load balancing. Experiments on competition benchmarks show that our approach achieves near-linear scalability and significantly outperforms existing distributed solvers. 2026-07-15T09:28:58Z Zhenghang Xu Minghao Yin Jumping Zhou Jean-Marie Lagniez http://arxiv.org/abs/2607.13617v1 A Telemetry-Driven Model for Quantifying Upgrade Risk in Durable Workflow Execution 2026-07-15T09:07:34Z Durable workflow engines reconstruct execution state by deterministically replaying an immutable event log, coupling every in-flight run to the code version that produced its history: a new deployment can invalidate the replay of runs started under the old version, silently corrupting state or halting progress. Existing mitigations -- pinning, patch gates, side-by-side deployment -- treat every change as maximally dangerous and drain old versions, untenable for workflows that sleep for weeks. We present a closed-form probabilistic model that quantifies the risk of upgrading in-flight runs from workflow version $V_1$ to $V_2$ using only a static structural diff and telemetry the protocol already persists -- event logs, step payloads, historical paths -- with no dry-run, sandbox, or shadow execution. Risk decomposes along three axes (protocol, interface, state migration) and combines an exact backward (rehydration) term, computed on recorded prefixes modulo trace equivalence of concurrent completions, with a probabilistic forward term from hitting probabilities in an empirically estimated Markov model of control flow. Estimation is Bayesian throughout, so the Workflow Upgrade Risk (WUR) score carries a credible interval and thin telemetry surfaces as uncertainty. We prove that a zero backward-risk verdict certifies safe rehydration under the new version, and derive a policy partitioning runs into migrate, review, and pin classes. Finally we drop the inter-run independence assumption: coupling through hooks, hierarchy, and shared resources is captured by an empirical coupling graph, fleet risk becomes the least fixpoint of a failure-contagion operator, and the coupling-aware migrate/pin partition is computed exactly as a minimum s-t cut. 2026-07-15T09:07:34Z 29 pages, 3 figures Luca Maraschi Matteo Collina http://arxiv.org/abs/2607.10443v2 CloudMicroHaskell: Direct-Style Distributed Haskell via Runtime Graph Serialisation 2026-07-15T08:58:24Z Cloud Haskell brings Erlang-style distributed programming to Haskell, but its treatment of mobile code exposes a difficult boundary in the source-level API. Remote processes must be expressed as static closures, messages must satisfy serialisation constraints, and participating nodes are assumed to share the relevant code. This paper explores a different design point. We present CloudMicroHaskell, a Cloud Haskell-style library built on MicroHaskell, whose runtime represents both code and data as a combinator graph. When a process or message crosses a node boundary, CloudMicroHaskell serialises the reachable graph directly. As a result, remote spawning can be written in direct style: process bodies may capture variables from their surrounding scope, and messages may contain ordinary values, including functions, without programmer-written closure conversion. We describe the implementation of the CloudMicroHaskell node runtime, including remote spawn, message delivery, monitors, exit propagation, and library implementations of generic servers and supervisors. We evaluate the system with process/message benchmarks, a distributed work-pool benchmark, a file-synchronisation case study, and a heterogeneous deployment on microcontrollers. The results show that runtime graph serialisation makes the \ch{} programming model substantially more direct, while also making the tradeoff explicit: some guarantees enforced by \ch{}'s source-level types become dynamic checks, and programmers must be aware of laziness and runtime-owned resources when moving graphs between nodes. 2026-07-11T19:02:53Z Robert Krook Lennart Augustsson http://arxiv.org/abs/2607.13531v1 Ripple: An Open, AI-Formalized Lean 4 Framework for Computing with CRNs 2026-07-15T07:32:07Z We present Ripple, an open, AI-formalized Lean 4 framework for the mathematics of computing real numbers with chemical reaction networks (CRNs). Ripple formalizes the full ladder of models -- the GPAC / CRN continuum and the CRN-computable reals, the large-population-protocol (LPP) compilation pipeline, and a continuous-time Markov chain (CTMC) layer bridged to the deterministic mean-field limit by three machine-checked versions of Kurtz's theorem, and two Turing-completeness results -- the Bournez-Graça-Pouly GPAC Turing-completeness construction and the Soloveichik-Cook-Winfree-Bruck stochastic-CRN universality theorem. The development is reliable (its core constructions are verified to depend on exactly the three Mathlib foundational axioms, with no sorry); it exposed genuine, fixable gaps in published proofs (the approximate-majority convergence argument and the LPP main theorem); and it proves new results -- a fully machine-checked construction of Apéry's constant ζ(3) as a CRN-computable number via its holonomic generating function, the same recipe turning the modular 1/π series of Ramanujan into a sharp open problem. The formalization was carried out predominantly by AI agents using only publicly available models, so the workflow is reproducible. 2026-07-15T07:32:07Z Comments: 27 pages, 1 figure, 1 table. Poster paper for DNA32 (32nd International Conference on DNA Computing and Molecular Programming) Ho-Lin Chen Xiang Huang http://arxiv.org/abs/2607.14166v1 Stop Means Stop: Measuring and Repairing the Enforcement Gap in Agent-Framework Control Primitives 2026-07-15T05:55:38Z Production LLM-agent frameworks expose control primitives -- human-in-the-loop approval gates, run cancellation, and execution timeouts -- whose names and documentation imply barrier semantics: while a run is paused, cancelled, or timed out, no gated side effect executes. We show this implied contract holds on none of the six widely used open-source frameworks we test. Model-free differential probes isolate a recurring sibling leak -- an approval gate suspends its own branch while a sibling branch's effect executes during the pause, so a later rejection cannot prevent it -- in every framework shipping a pre-execution gate (five of six), plus three further gaps: replay double-execution, cancellation orphans, and timeout zombies. The hazard is reachable, not merely constructible: under an a-priori-fixed protocol, frontier models emit the leak-triggering plan shape at pooled rates up to 14%, and when live models drive the unmodified frameworks under an approval pause, 215 of 1,200 runs execute their effect during the pause, across three schedulers and two language runtimes. To repair the measured gaps we present SOUNDGATE, an environment-external effect gate in Rust through which every side effect must be admitted, enforcing hold-until-decided, reject-cancels, dedup-on-replay, and fence-on-cancel -- one property per violation class -- under a stated complete-mediation contract discharged for network egress by kernel-enforced routes. We verify the properties over a model of the admission core (Verus; TLA+/TLC, exhaustive to 7.5e7 states; TLAPS), model-check the deployed Rust with Loom, and bridge model to code by differential conformance over 1.2e7 operations -- refinement evidence, not a mechanized proof. SOUNDGATE blocks every measured violation end-to-end on all six frameworks while releasing legitimate effects, at about 1 ms admission per write and 12k-26k durable admissions per second. 2026-07-15T05:55:38Z 31 pages, 3 figures, 11 tables Sajjad Khan