distributed systems engineers

Abstract: How does the number of sampled opinions affect the time required to reach consensus in distributed consensus dynamics? We study the synchronous $h$-\textsf{Majority}, in which every node independently samples $h$ nodes uniformly at random with replacement in each round and adopts a most frequent sampled opinion, breaking ties uniformly at random. We show that $h$-\textsf{Majority} achieves the nearly-optimal trade-off between the sample size and the consensus time, among a broad class of consensus dynamics. In particular, we prove the following results. For every sample size $h \ge 3$ and for every initial configuration, we prove that the process reaches consensus with high probability within $\widetilde{O}\left(1+\min\left\{\frac{1}{\min\{h^2p_{\max},1\}},\frac{\sqrt{n}}{h}\right\}\right)$ rounds, where $n$ is the number of nodes and $p_{\max}$ is the largest initial fraction of nodes supporting any single opinion. This is the first bound on the consensus time for $h$-\textsf{Majority} that holds for every $h\ge3$ and every initial configuration. When the initially most popular opinion has a sufficiently large lead over every other opinion, we show that all nodes adopt this opinion with high probability within $O(\log n/\min\{h^2p_{\max},1\})$ rounds. We establish a matching lower bound up to polylogarithmic factors for any fixed update rule that treats all opinions symmetrically and that selects either a sampled opinion or the node's current opinion.

Abstract: We study the scaling of the expected total queue length in an $n\times n$ input-queued switch. It has been conjectured that the optimal scaling is $O(n/(1-ρ))$, up to logarithmic factors, where $ρ$ is the system load. This conjecture has been established in the traditional heavy-traffic regime and in certain sub-regimes of the large-system regime. But it remains unresolved over a wide range of load scalings in the large-system regime. In this paper, we develop a family of scheduling policies parameterized by a positive integer $k\ge 2$. We show that under uniform traffic, our policy achieves an expected total queue length of $O\bigl({n\log\max\{n,1/(1-ρ)\}}\big/{(1-ρ)^{2^k/(2^k-1)}}\bigr)$, as long as $ρ\to 1$ in the large-system regime. As $k$ increases, the exponent $2^k/(2^k-1)$ approaches $1$, bringing our bound arbitrarily close to the conjectured scaling. The expected amortized scheduling cost of the policy is $O(n^3 k)$ per time slot. Our policy is of a batching type, with a novel recursive design that allows an arbitrary number of batching levels. This design principle may also be useful for other scheduling problems in which combinatorial constraints restrict which jobs can be served simultaneously.

Abstract: Determining the communication complexity of graph connectivity has been one of the longest standing open problems in communication complexity since the seminal work of Babai, Frankl, and Simon [FOCS'86]. A simple protocol transmits a spanning forest using $O(N\log N)$ communication on $N$-vertex graphs. While this was shown optimal for deterministic protocols by Hajnal, Maass, and Turán [STOC'88], the optimal nondeterministic and randomized complexities have remained unresolved for decades. We settle the nondeterministic communication complexity of graph connectivity by proving an optimal $Ω(N\log N)$ lower bound. The best prior bound was $Ω(N\log\log N)$ due to Raz and Spieker [Combinatorica'95]. Our bound is shown by upper bounding the maximum size of $1$-monochromatic rectangles. Generalizing our techniques to weighted, almost $1$-monochromatic rectangles yields an $Ω(N \cdot \log(\min(1/\varepsilon,N)))$ lower bound for randomized protocols with error probability $\varepsilon$. In particular, this bound is optimal for any polynomially small $\varepsilon$. For constant error probability, we also prove that any $r$-round protocol requires $Ω(N/r \cdot \log N)$ communication, which is optimal for every constant $r$. Previously, optimal $Ω(N\log N)$ lower bounds for graph connectivity were known only for $1$-round [Sun, Woodruff; APPROX/RANDOM'15] and $2$-round protocols [Radhakrishnan, Reddy, Venkat; ITCS'26]. Our proof introduces a new communication problem which can be viewed as a composition of inner product and pointer chasing problems. Our lower bounds can be extended to other fundamental graph properties, and also imply optimality of known query and streaming algorithms for related problems.

Abstract: We study alternation hierarchies for distributed decision in anonymous networks with constant-size certificates. A prover and a disprover alternately assign certificates to nodes over a constant number of rounds, after which each node decides whether to accept based on its own input and the certificates observed in its neighborhood. An instance is accepted if all nodes accept. Unlike previous work on distributed alternation hierarchies, which considered restricted local computation (Reiter, PODC 2024) or logarithmic-size certificates (Feuilloley et al., ICALP 2016), we focus on constant-size certificates and the role of neighborhood information in determining expressive power. We consider three models: SET, where nodes observe only the set of certificate sequences of their neighbors; MULTISET, where multiplicities are also visible; and PORTS, where neighbors can additionally be distinguished by local port numbers. We establish that SET is strictly weaker than MULTISET, which is in turn strictly weaker than PORTS, and that all three alternation hierarchies are strict at every level. Despite their severe restrictions, these models are remarkably expressive: LEADER belongs to the third level of SET. Our main characterization shows that, over finite input alphabets, SET coincides exactly with monadic second-order logic (MSO$_1$). Moreover, every language definable in counting monadic second-order logic (CMSO$_1$) belongs to PORTS, while MULTISET already contains languages that are not CMSO$_1$-definable. Nevertheless, this expressive power has fundamental limitations. PORTS does not capture MSO$_2$: neither Hamiltonicity nor the existence of a perfect matching belongs to PORTS. Furthermore, over unbounded input alphabets, PORTS cannot verify that every node has been given the correct network size.

Abstract: Causal Graph Rewriting was recently introduced as an evolution of Causal Graph Dynamics to allow for a controlled form of asynchronism in these dynamical systems with dynamical graphs. In this context, the notion of borders---akin to dangling edges---has gained increasing importance. In this paper, we re-examine these borders, interpreting them as missing information. This perspective adds structural rigor to the framework, allowing border-agnostic causal graph rewriting to be reformulated as a rewriting system rather than a dynamical system. This shift represents a crucial step toward facilitating the treatment of reversibility.

Abstract: We present FRACTAL, a self-similar multi-agent architecture for recursive goal decomposition, in which the same five-component organizational pattern -- Orchestrator, Ensemble, Knowledge Ledger, Decision Maker, Meta-Observer -- recurs at every level of a decomposition tree. We make four formal contributions: (1) a communication bound showing intra-node cost is linear in ensemble size and round count (O(kr)) under a two-phase blind-proposal/stress-test protocol, versus quadratic cost for free-form debate, with an explicit, stated assumption on fixed evaluator count; (2) a two-mode orchestration criterion separating generative and evaluative phases via a measurable diversity-saturation threshold; (3) a supermajority convergence guarantee with explicit probability bounds at stated agreement levels, and a formal depth bound under an operationalized goal-complexity measure; (4) a Bayesian inter-layer escalation mechanism unifying hysteresis and contract-breach signaling under one posterior update. We illustrate the architecture's execution qualitatively on a worked example and a multi-layer case study; we do not report quantitative performance claims in this paper, and we explicitly discuss the formal and inductive-bias limitations of the model, including an unimplemented but architecture-compatible direction toward bounded self-improvement. We use "fractal" as an architectural metaphor for self-similarity, not a measured mathematical property. Empirical validation of the architecture's comparative performance is left to future work.

Abstract: We study the $(K,N,S,M,K_c)$ distributed linearly separable computation (DLSC) setting, where a master employs $N$ workers with a per-worker computation load of $M$ to recover $K_c$ deterministic linear combinations of $K$ messages in the presence of up to $S$ stragglers. We propose a DLSC framework based on nested cyclic codes that achieves $M=\frac{K}{N}(S+K_c)$. For sufficiently large $K$, we establish the matching converse $M\geq\frac{K}{N}(S+K_c)$, proving the asymptotic computation load optimality of the proposed framework. By instantiating cyclic locally recoverable codes (LRCs) as base codes in the framework, the master can recover the desired $K_c$ linear combinations by contacting fewer than $N-S$ workers under many straggler scenarios. This essentially softens the straggler threshold without increasing the computation load or communication cost. Finally, we extend the construction to reduce the per-worker communication load by a factor of $m$, while achieving an asymptotically optimal computation load of $M=\frac{K}{N}(S+mK_c)$.

Abstract: Collective communication is a critical performance bottleneck in large-scale distributed training. Existing libraries and synthesis frameworks compute open-loop schedules once, assuming a static topology and peak link capacities. In production, however, persistent gray failures can silently degrade link throughput and latency for hours, causing pre-computed schedules to lose much of their efficiency during execution. In this paper, we present Measurement-based Collective Communication Library (MCCL), a collective communication library that closes the loop between runtime network measurement and dynamic schedule synthesis. MCCL passively measures GPU-to-GPU throughput, detects persistent degradation, re-synthesizes the affected communication-intensive schedules with warm-started synthesizers, and hot-swaps them without interrupting training. We validate the complete loop on a multi-node hardware prototype and use simulations to evaluate cluster-scale scenarios. In our experiments, MCCL incurs negligible overhead (<2%) while maintaining high measurement accuracy (<1.2% error) and low schedule hot-swap time (about 12 ms). Notably, under gray failures, MCCL reduces training time by up to 4.99x over static schedules on simulated training workloads for state-of-the-art LLMs such as Llama and DeepSeek.

Abstract: We introduce FORGE (Fast On-chip Rotor Generation for Experts), a procedural weight generation system for Sparse Mixture-of-Experts (MoE) inference. Rather than storing and loading every expert weight tensor from HBM, we show how a compact accelerator inside each Streaming Multiprocessor can regenerate them on-the-fly from $O(\log^2 d)$ rotor parameters per projection. Per replaced layer, gigabytes of stored expert weights are approximated with under a megabyte of seeds. This addresses the dual memory bottleneck of autoregressive Sparse MoE decode, where per-expert FFN operations are HBM-bandwidth-bound at small routed-token counts and the aggregate expert footprint forces multi-node Expert Parallelism (EP) with all-to-all traffic. We realize the approach as the Rotor Generation Unit (RGU), a fixed-function datapath that generates FFN weight tiles without competing with Tensor Core execution. With 30% of the MoE FFN layers replaced across five Sparse MoE models, we estimate 1.3-2.8x higher system throughput at matched GPU count and 1.10-1.15x lower per-user decode latency at short context. In exchange, downstream accuracy on three model families falls below that of the same model fine-tuned without rotor replacement, and the replacement ratio controls this tradeoff. FORGE also expands KV cache capacity by 1.2-2.6x. It is agnostic to the bit width at which weights are stored, so it can compose with quantization. The RGU is fully implemented/verified in SystemVerilog at ~0.9% SM area overhead (0.032 mm^2/SM, 7nm).

Abstract: We give a deterministic distributed algorithm for $(Δ+1)$-coloring an $n$-node graph of maximum degree $Δ$ in $O(\sqrtΔ+\log^* n)$ rounds in both the LOCAL and CONGEST models. More generally, $(°+1)$-list coloring with lists from a color space of size $C\geqΔ+1$ can be solved in $O(\sqrtΔ\log(1+C/Δ)+\log^* n)$ rounds; in CONGEST, we assume $C\leq n^{O(1)}$. The algorithm combines Barenboim's polynomial coloring procedure with arbdefective decompositions, degree reduction, and a short family of hash functions. Using the polynomial procedure in the degree-reduction framework already gives an $O(\sqrtΔ\logΔ+\log^* n)$-round algorithm when $C=O(Δ)$. Hashing adapts the color space to the current degree and removes the logarithmic factor. We prove the existence of the hash family by the probabilistic method and compute it by deterministic exhaustive search, using unrestricted local computation. We also give an explicit variant based on lossless expanders that avoids this search and achieves $O(\sqrtΔ+\log^* n)$ rounds for $C=O(Δ)$.

Abstract: We study constant-round LOCAL approximation for additive local vertex-subset minimization problems. Given a $k$-uniform $α$-approximation on a hereditary source class closed under disjoint union, Bonamy, Das, Gavoille, Picavet, Suomela, and Wesolek obtained ratio $α(d+1)+1$ on locally nice target classes of asymptotic dimension $d$. We prove two transfers with ratios $α+1+η$ and $α+η$ for every $η>0$. These bounds require the stronger local niceness assumption at a larger scale that depends on $η$. The first algorithm keeps their repair construction and increases the radius used to detect errors. We average over partitions of the graph to bound the retained cost without the factor $d+1$. These partitions are used only in the analysis. The second algorithm tests several deletion widths around the errors. In each component of the repair zone, it chooses a smallest union of retained choices and an exact repair. Averaging over the widths bounds the cost counted twice and yields ratio $α+η$. Both transfers are deterministic and computable, use arbitrary distinct numerical identifiers, and need no knowledge of the graph size. Their outputs also satisfy local uniformity guarantees. For 2-domination on graphs of bounded Euler genus, the same planar source gives ratio $19$ through the earlier transfer and $6+η$ through ours. For minimum dominating set, our transfer gives ratio $7+\varepsilon$ on graphs formed by attaching a clique of arbitrary size at one vertex of a planar graph, using the source algorithm of Amiri and Siebertz. This class satisfies our target assumptions and allows nonempty error sets. Its Euler genus is unbounded, so their guarantee for graphs of bounded Euler genus does not cover the whole class.

Abstract: Formal verification of distributed protocols is still dominated by inductive-invariant proofs, whose central challenge is discovering strengthening assertions that rule out unreachable states. This burden is often misaligned with how protocol designers reason: they explain correctness by following representative executions, causal histories, and phase-structured interactions among nodes. This paper introduces scenario proofs, a verification methodology that makes such execution-oriented reasoning formal. A scenario is a structured expression describing representative protocol executions, enriched with ghost variables. Rather than enumerate all possible interleavings, a scenario describes canonical executions and uses a sound semi-commutation relation to account for reorderings that preserve feasibility and final states. Verification then factors into two main obligations. Coverage shows that every feasible protocol execution is equivalent, up to semi-commutation, to one described by the scenario; this obligation is independent of the safety property and serves as a reusable behavioral characterization of the protocol. Correctness proves the desired safety property only over the representative executions, using Hoare-style weakest-precondition reasoning along the scenario structure. We formalize the scenario language, its layered semantics, and proof rules for coverage and correctness. Through case studies of ring leader election, two-phase commit, a decentralized lock, two variants of multi-signature payment, and single-decree Paxos, we show how scenario proofs capture the causal and phase-based arguments used informally by protocol designers. These examples illustrate that scenario proofs can replace monolithic invariant discovery with structured reasoning over representative executions, while retaining a rigorous connection to all feasible protocol behaviors.

Abstract: Modern large-scale systems rely on distributed protocols to maximize efficiency while preserving the correctness guarantees of single-process execution. However, designing such protocols is non-trivial: adding resources to a system inherently increases its complexity, which in turn introduces faults that must be addressed during design. One such fault class, arising in systems that use distributed shared memory (e.g., replicated databases), is consistency violating fault (cvf), a fault in which a process accessing shared memory reads stale data previously written by another process. Cvfs are inherent to systems that prioritize availability over strict consistency. Prior work has shown that self-stabilizing programs remain correct under high availability, provided such faults stay within a tolerable bound. Characterizing the behavior of self-stabilizing programs in the presence of cvfs can therefore help system designers build systems that are both correct and efficient. In this paper, we study self-stabilizing programs under cvfs to understand when and where such faults occur, enabling runtime measures that improve computational efficiency. Since exhaustive state-space exploration does not scale, it suffers from state-space explosion; our study investigates two complementary approaches: a conflict-based state-space exploration technique for monotonically stabilizing $(Δ + 1)$-Graph Coloring programs, and a machine-learning-based approach for a Maximal Independent Set program. We propose a conflicting-edges-based state-space exploration algorithm alongside a rigorously validated ML model, evaluated on an out-of-distribution dataset through structural consistency checks against known graph invariants.

Abstract: For every fixed proper minor-closed class $\mathscr C$ and every $ε>0$, we give a deterministic LOCAL algorithm that returns a dominating set of size at most $(2a(\mathscr C)+1+ε)γ_f(G)$ on every $G\in\mathscr C$. Here $a(\mathscr C)$ is the supremum edge-to-vertex ratio in~$\mathscr C$, and $γ_f(G)$ is the fractional domination number. The class also admits a deterministic $(1+ε)$-approximation for fractional dominating set and a randomized algorithm that always returns a dominating set and has expected size at most $(1+ε)γ(G)$. In each case, the number of rounds depends only on $\mathscr C$ and~$ε$. None of these algorithms requires the number of vertices or the maximum degree as part of the input. For planar graphs, this gives the deterministic guarantee $(7+ε)γ_f(G)$. Together with the lower bound of Hilke, Lenzen and Suomela, it determines the infimum of the deterministic constant-round approximation ratios for planar minimum dominating set as~$7$, settling a question that had remained open since their work. The corresponding infima, measured against the integral optimum, are $7$ for graphs of Euler genus at most any fixed $g\ge0$, $2t-3$ for $K_t$-minor-free graphs with $3\le t\le9$, and $2r+1$ for graphs of treewidth or pathwidth at most any fixed $r\ge1$. We also prove that, for every integer~\mbox{$r\ge1$}, no deterministic constant-round LOCAL algorithm achieves an approximation ratio below~\mbox{$2r+1$} on the $r$-th powers of paths, even when every vertex knows the number of vertices. This gives a new proof that the limiting constants are optimal for planar graphs, graphs of bounded treewidth or pathwidth, and $K_t$-minor-free graphs with $3\le t\le9$. For triangle-free planar graphs, the corresponding infimum is $5$.

Abstract: Huffman coding is one of the oldest and most fundamental problems in computer science. Given a string of length $\TextLength$ over a general alphabet, the goal is to assign a binary codeword to each character so that no codeword is a prefix of another and the total encoded length of the string is minimized. Huffman coding is widely used in practical compression systems, including file compression. As modern datasets continue to grow, it is natural to study whether a Huffman code can be constructed efficiently in the massively parallel computation (\MPC) model. The celebrated Huffman coding algorithm admits two straightforward \MPC implementations: for any constant $ε\in(0,1)$, one uses $O(\TextLength^ε)$ memory per machine but requires $Θ(\log \TextLength)$ rounds, while the other runs in $O(1)$ rounds but requires $Θ(\sqrt{\TextLength})$ memory per machine. We give the first nontrivial \MPC algorithm for Huffman coding that bypasses both limitations. For every constant $ε>0$, our algorithm uses $O_ε(\log\log \TextLength)$ rounds and $\softO(\TextLength^ε)$ memory per machine, while its total memory and total computation are $\softO(\TextLength)$. This provides a rare example in which an exact solution to a problem whose classical algorithm is sequential in nature can be obtained in a sublogarithmic number of \MPC rounds.

Abstract: Linearizability gives developers the illusion that operations on a distributed datastore execute sequentially on a single machine. Providing it is expensive, so numerous specialized reads algo- rithms have been proposed to make reads significantly faster without sacrificing linearizability, which matters because most workloads are read-dominant by orders of magnitude. Yet, none of these algorithms is the best choice for every deployment. We show why with a framework that classifies these algorithms into a generalized space together with a mathematical analysis of their latencies as a function of this generalization. The analysis exposes two fundamental tradeoffs, one between read and write latency and one between read and write tolerance to network variance, which together leave the best algorithm dependent on network and workload conditions that vary over time. It also exposes a gap: there is a way to minimize the delay a read incurs when it overlaps a concurrent write, at no cost to writes, yet exist- ing algorithms can apply it only for a subset of the tradeoff space, forcing any deployment that needs the full space to settle for a strictly worse solution. We close this gap with a new algorithm, Pairwise Quorums, and build a second, Ditto, that reconfigures across the space at runtime as conditions change. Together they subsume every existing algorithm under our model: against each, the combination is either strictly better, or reconfigures to match it where a genuine tradeoff applies.

Abstract: In graphical two-choice allocation, each arriving ball is assigned to one endpoint of a random edge. We study rules whose decision is a monotone function of the two endpoint loads, allowing edge-dependent thresholds and fresh randomization. Such a rule has an exact unit-discrepancy coupling: adding one ball to the initial state produces one tagged discrepancy at every later time. We represent the tag by conditional-expectation projections on the marked edge space and obtain diffusive displacement bounds. A transport-volume inequality then converts slow propagation of influence into lower bounds for the load gap. On the cycle with $n$ vertices, from every initial distribution and at every physical time $t\ge 1/n$, the expected gap is at least a constant times $\min\{\sqrt n,t^{1/4}\}$, and the gap exceeds this scale with probability at least $1/8$. After exactly $k\ge1$ allocations, the corresponding scale is $\min\{\sqrt n,(k/n)^{1/4}\}$. No stationarity, symmetry, recurrence, or moment assumption is used. The general inequality also yields a lower bound of order $\sqrt{L/K+\log K}$ on the $L\times K$ discrete torus $C_L\square C_K$. These results separate endpoint-local rules from global-information strategies that achieve polylogarithmic gaps on cycles.

Abstract: Federated clustering methods that do not require the global number of clusters $K$ still assume that each client knows its local number $K_g$. This assumption is hard to justify when clients know no more about their data than the server does, as in fault diagnosis across independently operated industrial sites. We propose a two-phase framework in which neither count is known: each client first estimates $K_g$ from its own data, and an aggregator that requires local counts, such as FedGEM, then uses these estimates in place of the true values. For the first phase we introduce Adaptive Split--Merge (ASM), which grows a spherical Gaussian mixture by BIC-driven splitting and then merges excess components. ASM uses no labels, selects its hyperparameters on held-out client data only, and makes no assumption about how clusters are shared across clients. We derive a closed-form split criterion whose critical cluster size falls with anisotropy and rises with dimension, and show empirically that over-fragmentation grows with the number of points per cluster, which federation divides among clients. Across eight datasets, ASM with FedGEM attains a mean ARI of 0.333, against 0.256 for the next best label-free estimator and 0.361 when the true local counts are supplied. It also gives the most reliable global estimates of $K$ and is robust when client size is decoupled from local cardinality.

Abstract: We prove that the state space of every well-formed session type, quotiented by strongly connected components, forms a bounded lattice; n-ary parallel composition yields product lattices. Two consequences follow: duality preserves the lattice up to isomorphism, and Gay-Hole width subtyping corresponds to lattice embedding for non-recursive types. We validate this on 108 benchmark protocols across networking, databases, distributed systems, AI, and fault tolerance: all form lattices, 93 distributive, 15 non-distributive. Mechanised in Lean 4 with two independently developed tool implementations.

Abstract: The development of round elimination into a general-purpose technique [PODC 2019] marked a turning point in our understanding of the hardness of many graph problems in the distributed setting and led to several breakthrough results. However, the round elimination technique seems unable to yield randomized lower bounds of $ω(\log \log n)$ rounds as a function of the number $n$ of nodes. Very recently, Khoury and Schild [FOCS 2025] introduced a new technique called round elimination via self-reduction, which bypasses the limitations of classical round elimination. Using this approach, the authors show that any randomized algorithm for maximal matching requires $Ω(\sqrt{\log n})$ rounds in the LOCAL model. Their elegant technique is, in some respects, similar to classical round elimination while being fundamentally different in others. However, it is tailored specifically to maximal matching rather than being applicable to a broad class of problems. In this paper, we show that self-reduction is, in fact, a special case of classical round elimination, thereby turning it into a general-purpose approach. In particular, we introduce a new way to measure the error of an algorithm and show that, under this new measure, classical round elimination can indeed yield $ω(\log \log n)$ randomized lower bounds. More specifically, we identify a large class of problems for which this improvement is entirely black-box: once a problem is shown to belong to the class, stronger randomized lower bounds follow automatically from the classical round-elimination framework. As an application, we prove $Ω(\sqrt{\log n})$ randomized lower bounds for a range of graph problems, namely, maximal matching on regular $2$-colored graphs, $\frac{1}{k}$-integral matching, and maximal $H$-packing.

Abstract: Adversarial consensus simulators require not only a model of message delivery but also a model of time. For timeout-sensitive protocols, coupling protocol-time progression to scheduler activity can allow communication scheduling to influence when failure detectors expire. We study this interaction in VeriProtocol using controlled Multi-Paxos and Raft experiments. In the primary Multi-Paxos study, we compare EventCoupled timing, where every scheduler opportunity advances protocol time, with RoundTick timing, which decouples individual scheduler events from timeout progression. At N=5, increasing the bounded message-delay budget from K=6 to K=14 increased the observed EventCoupled leadership-instability rate from 5\% to 100\% across the tested grid, while no additional valid leader elections occurred in any of the corresponding 140 RoundTick executions. At K=0, neither model produced additional elections. Matched-trace analysis identifies the mechanism: under EventCoupled timing, scheduler activity used to perturb communication also directly advances failure-detector state. Under RoundTick, comparable scheduler activity does not imply equivalent protocol-time progression. A targeted heartbeat-delay control confirms that RoundTick does not suppress timeout-driven elections; an additional election remains reachable when leader contact is unavailable across sufficient logical time.

Abstract: We introduce a novel functional-style concurrent programming language called Categorical Message Passing Language (CaMPL) which is designed using the mathematics of linear actegories. This mathematical underpinning gives CaMPL programs useful properties such as deadlock freedom, and additionally, livelock freedom for programs without general recursive processes. We explore CaMPL's type system through a series of code examples. The current proto-alpha version of the compiler and the abstract machine is implemented in Haskell. A reader is encouraged to experiment with writing CaMPL programs either using the online compiler https://campl-app.vercel.app/ or by installing CaMPL from https://campl-ucalgary.github.io -- our website has detailed instructions on how to run CaMPL code.

Abstract: For integers $1\le k\le n/2$, let $f(k,n)$ be the least integer $s$ such that every $s$-connected graph on $n$ vertices contains a spanning bipartite $k$-connected subgraph. Thomassen conjectured that $f(k,n)$ is bounded by a function of $k$ alone. Delcourt and Ferber proved $f(k,n)=O(k^3\log n)$, and Yuster subsequently obtained $f(k,n)\le22k^2\log_2 n$. We prove that, for $2\le k\le n/2$, \[ f(k,n)\le\min\left\{n-1,\, \left\lfloor6(k-1)\log_2\frac{n}{k-1}\right\rfloor\right\}. \] In particular, $f(k,n)=O(k\log(n/k))$.

Abstract: Tiny twins are compact behavioral models derived from timed actor models for selected observable messages. When a source model evolves, regenerating its tiny twin requires state-space exploration and reduction even if the relevant behavior is unchanged. We present a static analysis for Timed Rebeca that compares backward slices of Rebeca dependence graphs for a given set of observable message names. For the Zeno-free fragment with after annotations and no delay statements, we prove that slice equivalence implies weak timed bisimulation under the selected observations. This preserves observable actions and total elapsed time across internal transitions, allowing the existing tiny twin to be reused. We evaluate the implementation on ten benchmark models paired with revisions that preserve their observable slices. The cost of static comparison depends on the size of the graphs representing source statements and their dependencies, while tiny-twin generation depends on the number of reachable states and transitions. This difference is reflected in the measurements: static comparison takes less than one second using tens of megabytes of memory, while tiny-twin generation can take over an hour and use hundreds of gigabytes.

Abstract: Set reconciliation, where two parties each holding a large set of elements aim to identify their set difference, is a fundamental task in many areas. There are two important metrics in this problem: time (computation cost) and space (communication cost). Most previous work focuses on optimizing one metric at the expense of the other. We present XYZ-Sketch, proving that it is possible to achieve near-minimal space and $O(1)$ time updates simultaneously. Specifically, for sufficiently large $d$, XYZ-Sketch reconciles sets with only $(1+\varepsilon)d$ elements for communication, while achieving $O(1)$ insertion time and $O(d\log V)$ decoding time. Here, $d$ and $V$ denote the size of the difference between two sets and the universe size, respectively. We further establish a broad fixed-support canonical model for the problem, showing that, under an open extremality conjecture, XYZ-Sketch is asymptotically optimal within this model. Experiments validate the predicted near-optimal performance of XYZ-Sketch. The source code is available at https://github.com/djwj233/XYZ-Sketch.

Abstract: Temporal Path Cover (TPC) and Temporally Disjoint Path Cover (TDPC) ask for minimum-cardinality covers of a temporal digraph by temporal paths, with TDPC additionally requiring pairwise temporal disjointness. Cioni et al. proved both problems NP-hard on temporal DAGs whose underlying undirected graph has vertex-cover number three and left the vertex-cover-two case open. We resolve this question affirmatively for both problems. Using polynomial-time reductions from Distinct Numerical Matching with Target Sums, we show that TPC and TDPC are NP-complete already when the underlying undirected graph has vertex-cover number exactly two. For TPC, this yields an exact vertex-cover threshold: polynomial-time solvability at vertex-cover number at most one and NP-completeness at two. For TDPC, we further study the boundary case of temporal oriented stars. A reuse-normalization argument reduces optimum solutions to leaf-unique two-edge merges. If either the incoming or outgoing side is single-label, the optimum remains polynomial-time computable even when the opposite side is multi-label. We also introduce a span parameter for feasible merge realizations and prove that any feasible family of k merges forces a realization of span at least 2k-2. Hence TDPC on temporal oriented stars is in XP parameterized by maximum span, and is polynomial-time solvable for every fixed span bound. The unrestricted multi-label star case remains open.

Abstract: Large Language Models (LLMs) with function-calling capabilities are becoming critical for modern agentic AI systems. Nevertheless, current deployments typically route inferences to powerful cloud-based models, incurring significant energy use and carbon emissions. We address this sustainability challenge with a carbon-aware routing framework that distributes function-calling queries across a three-tier edge-cloud architecture, combining edge and cloud LLMs on heterogeneous hardware. At its core, a lightweight k-NN predictor operating in a unified semantic-lexical embedding space estimates query-specific accuracy, delay, and power consumption on each edge tier. These predictions are then combined with real-time grid carbon intensity to route every query to the lowest-emission tier capable of executing it successfully. Evaluated on state-of-the-art function-calling benchmarks and LLM families, our framework matches cloud-level accuracy while reducing operational carbon emissions by $4\times$ on average.

Abstract: Can a finite verifier obtain public, model-relative evidence about response latency for sequential computation? Verifiable delay functions (VDFs) make this possible in principle: evaluation requires T sequential steps, whereas verification is efficient in the security parameter and polylogarithmic in the numerical value of T for standard constructions. Thus a delay can be astronomically large to evaluate yet succinctly represented and feasibly checked. A VDF proof for a chosen message alone is insufficient because it may be precomputed. We specify and analyze Fresh-Challenge VDF Attestations (FCLA), a protocol composition that binds a VDF to an unpredictable public challenge, a message, and independently auditable release and receipt records. Under explicit assumptions about VDF sequentiality, the challenge source, witness logs, and a calibrated upper bound on an adversary's sequential evaluation rate, an accepted FCLA transcript is inconsistent with post-challenge generation by an adversary in that bounded model. The result neither identifies a named claimant nor excludes relaying, outsourcing, or a faster unmodeled machine. A benchmark of the public reference implementation confirms the expected empirical separation between evaluation and verification on one documented machine. Our contribution is a protocol/design analysis and benchmarked reference implementation layer, not a new VDF construction or cryptographic primitive.

Abstract: How does cooperation evolve in complex agentic systems? Prior work in evolutionary game theory studies why individuals are incentivized to cooperate by isolating social interactions from the physical costs of behavior, while artificial life models traditionally study emergent self-replication without formalizing the dilemma between acquiring resources and preserving the shared energy needed to reproduce. In contrast, we introduce Autopoietic Game Theory, a computational model where social interactions, replication mechanisms, and their associated computational costs are endogenous and simultaneously co-evolving. We study these dynamics using a computational substrate of randomly initialized programs in Z80 machine code, showing empirically, and motivating with a simplified theoretical model, that embedding a social dilemma directly into the physics of computation can favor the emergence of self-replicating, cooperative strategies. When resources are scarce, our analysis shows that defection can become self-limiting even in well-mixed populations: parasitic stealing destroys shared energy, slows execution, and can prevent reliable replication. Empirically, evolved programs suppress stealing across several Z80 environments, while spatial assortment further supports structural complexity and task performance. We further show that the framework can incorporate exogenous pressures, such as math tasks structured as sequential social dilemmas, when rewards are tied to computation budgets. These results suggest that coupling an agent's capacity for computation to its available energy transforms cooperation into a dominant scaffolding for building sustainable, self-organizing systems.

Abstract: We introduce a graph decomposition primitive called introvert clustering, which strengthens standard low-diameter clustering by guaranteeing that every clustered vertex keeps at least a $\left(\frac12-\varepsilon\right)$-fraction of its relevant neighbors in its own cluster. Repeatedly applying this primitive yields a layered introvert network decomposition with $O(\log n)$ layers and weak diameter $O(\log n)$. We give two applications in the $\mathsf{LOCAL}$ model. For every constant $\varepsilon>0$, we obtain a $\widetilde O(\log^2 n)$-round deterministic algorithm for list $\left(\frac32+\varepsilon\right)Δ$-edge coloring on graphs of maximum degree $Δ\geqΔ_0(\varepsilon)$; for bipartite graphs, the result holds for all $Δ$. For every constant $0<\varepsilon<1/4$, we also obtain a $\widetilde O(\log^2 n)$-round deterministic algorithm for a $\left(\frac14-\varepsilon\right)$-locally balanced cut, where every vertex has at least a $\left(\frac14-\varepsilon\right)$-fraction of its neighbors on the opposite side. The resulting algorithms are remarkably simple: edge coloring processes the layers in reverse order and colors each cluster, while locally balanced cut processes them forward and computes a locally maximum cut within each cluster. The introvert guarantee enables these procedures beyond the usual greedy regime of network decomposition. We construct the decomposition in $O(\log^2 n)$ randomized rounds using Miller--Peng--Xu low-diameter clustering and a simple trimming procedure, and deterministically in $\widetilde O(\log^2 n)$ rounds via a white-box adaptation of the recursive network decomposition algorithm of Ghaffari and Grunau [FOCS 2024].

Abstract: Distributed-tensor systems specify where values reside, while collective systems optimize how requested operations execute. At a boundary between vendor runtimes that cannot share a native communicator, neither abstraction states what a remote consumer must observe. SemBridge fills this gap by compiling graph and runtime facts into a typed contract for the consumer-visible result and its delivery obligations. The contract captures provenance, substitutability, completion, authority, demand, and native-domain locality. A deterministic lowerer constructs backend-neutral communication plans, and a symbolic checker validates each plan before execution across CUDA/NCCL and CANN/HCCL. An independent layout-only planner handles all 72 structural transitions but establishes only 54 complete obligations; a byte-only minimizer proposes 40 semantically invalid candidates, all rejected by SemBridge. On nine real edges, SemBridge produces distinct observation-aware plans that reduce startups on all nine and payload bytes on the three result edges. A live CUDA/CANN run derives and executes full-logit reconstruction, source projection, and owner-token delivery from log-probability, token-only, and owner-scoped requests. On a measured two-host 1-GbE capacity-spillover deployment, source projection cuts result traffic by more than 99.97% and increases throughput by 8.92-80.20% across Dense, MoE, and MiniMax workloads. All 18 MiniMax restart pairs at concurrency 1, 8, and 16 favor source projection. A Qwen3-14B MLP slice additionally verifies bitwise activation-shard delivery and HCCL completion of row-parallel partials. These results establish consumer observation as a semantic layer between placement and collective execution.

Abstract: Byzantine Reliable Broadcast (BRB) and Message-Adversary-Tolerant Byzantine Reliable Broadcast (MBRB) are reliable-dissemination abstractions for fault-tolerant distributed systems. Yet their operational behavior is shaped not only by specifications and asymptotic communication bounds, but also by serialization, cryptography, buffering, orchestration, deployment environment, and fault-injection semantics. This paper implements and evaluates Bracha [Information and Computation, 1987], AFRT by Albouy et al. [TCS, 2023], and Coded MBRB by Albouy et al. [OPODIS, 2024]. We implement the algorithms in a shared Go codebase with common orchestration, instrumentation, parser-based specification checks, fault injection, and an open-source reproducibility artifact. The evaluation uses single-shot broadcasts in the Shadow network simulator, native profiling, a Google Cloud Platform deployment, and a distributed FABRIC testbed, covering controlled experiments up to 30 nodes, payloads up to 40 MB, 92,190 runs, and 2,361,600 parser-checked entries. The results show that Coded MBRB reduces transmitted data and improves latency in the evaluated cloud setting for larger payloads, but shifts cost to cryptographic and coding computation. Bracha and AFRT incur lower CPU costs at smaller payloads, but their full-payload dissemination increases processing, allocation, and network costs as payloads grow. Across the tested configurations, the parser found no duplicate deliveries, conflicting deliveries, or deliveries of values different from the sender's payload. The paper contributes implementation-level evidence and an extensible artifact for benchmarking BRB and MBRB as executable distributed-system components, exposing bottlenecks and operational trade-offs that are hidden by algorithmic descriptions alone.