Phalanx: A Formally Verified, Topology-Aware Control Plane for
Fault-Tolerant Training on Kubernetes GPU Clusters

Abstract

Large-scale training is now failure-dominated: Meta reported 419 unexpected interruptions across a 54-day Llama 3 run on 16,384 H100 GPUs, roughly one every three hours, and synchronous training semantics mean a single dead GPU can stall the entire job. The infrastructure that manages these jobs is split down the middle. Kubernetes-side schedulers (Volcano, Kueue, YuniKorn, NVIDIA KAI, and the alpha Workload Aware Scheduling primitives that only entered upstream Kubernetes in v1.35 and v1.36) decide where a gang of pods lands, with growing but incomplete topology awareness. Framework-side elasticity layers (TorchElastic, Oobleck, Bamboo, Parcae) decide how a job survives a failure, with no view of cluster topology and no ability to claim replacement hardware atomically. The seam between them is exactly where large runs bleed goodput: failure-triggered rescheduling is today neither topology-aware nor provably checkpoint-consistent. We present Phalanx, a Kubernetes-native control plane that unifies the two concerns. Phalanx contributes (1) HDF-B, a hierarchical deepest-fit gang placement algorithm with buddy-aligned allocation over a topology tree compiled from Dynamic Resource Allocation attributes, for which we prove per-gang bottleneck optimality, a factor-2 capacity augmentation bound, and a bounded failure blast radius; (2) the Rank Reformation Protocol (RRP), an epoch-fenced reconfiguration protocol whose safety (checkpoint consistency, exclusive placement, zombie fencing) we establish by inductive invariants over a TLA⁺ specification and whose liveness we establish under partial synchrony, in the style of Anvil’s eventually stable reconciliation; we mechanically check both with TLC across 834,050 distinct protocol states, and a mutation study shows the checker exhibiting a liveness counterexample the moment the protocol’s contended-commit retry transition is deleted; and (3) an executed evaluation: beyond the TLC campaign, a full-scale discrete-event instantiation of the model at 131,072 leaves in which Replan answers node failures with a p99 latency of 0.9 microseconds while migrating exactly 8 ranks, recovery placements hold median step-communication inflation to 1.00$\times$ against 8.9$\times$ for topology-blind replacement on a hierarchical bandwidth model, and Monte Carlo failure injection over 1,000 54-day runs per configuration reproduces the renewal model within 1.4 points, yielding effective training time ratios of 0.980 at 16K GPUs and 0.891 at 131K GPUs where the restart-based baseline measures 0.467. The design is hardware-generation agnostic across Ampere, Hopper, and Blackwell because the topology tree is derived from device attributes rather than hard-coded fanouts.

1 Introduction: the reliability wall

Two curves are crossing. The first is cluster scale: frontier training runs moved from hundreds of GPUs to tens of thousands in about four years, and public roadmaps point at hundreds of thousands. The second is component reliability, which is not improving at anywhere near the rate scale is growing. The product of the two is a mean time between failures that shrinks linearly with GPU count. The best public datapoint is the Llama 3 herd report [1]: over a 54-day pre-training snapshot on 16,384 H100 GPUs, Meta logged 466 job interruptions, 419 of them unexpected, one failure roughly every 3 hours; 58.7% of the unexpected interruptions were GPU-related, with 30.1% attributed to GPU failures including NVLink and 17.2% to HBM3 memory, and the team still held effective training time above 90% with only three incidents needing significant manual intervention [1, 2]. Extrapolating the same per-device failure rate, a 131,072-GPU cluster faces an interruption every 23 minutes. Meta’s broader reliability study of two research clusters, covering 11 months, four million jobs, and 150 million GPU hours, formalizes the productivity metric this paper optimizes, the effective training time ratio (ETTR), and shows why checkpoint cadence and restart latency dominate it at scale [3]. Earlier evidence says none of this is new: the Philly trace analysis of a multi-tenant Microsoft cluster already found DNN training jobs failing on average every 45 minutes [4].

Synchronous data-parallel training turns each component failure into a whole-job event. Every rank participates in every collective; one unresponsive NCCL peer stalls 16,383 others. The infrastructure response has been bifurcated in a way this paper argues is the core architectural mistake of the current stack.

The scheduling half.

Kubernetes was built around one-pod-at-a-time scheduling for stateless services. Gang semantics, where a job needs all-or-nothing placement of $N$ pods, arrived only through external schedulers: Volcano’s PodGroups [27], Kueue’s admission and quota layer [28], YuniKorn [29], and NVIDIA’s KAI-Scheduler [30], which adds hierarchical PodGroups, topology-aware scheduling, and DRA support for GB200/GB300-class parts, with public scale tests at thousands of nodes. Upstream Kubernetes itself shipped alpha native gang scheduling only in v1.35 (KEP-4671), and the v1.36 release [31] extends it with a decoupled PodGroup API (KEP-5832), workload-aware preemption (KEP-5710) [32], topology-aware workload scheduling, and Job controller integration, all alpha and disabled by default behind the GenericWorkload, GangScheduling, TopologyAwareWorkloadScheduling, and WorkloadAwarePreemption feature gates. Every one of these systems answers the question “where should this gang start” and none of them answers “what happens at failure number 217 of 419.”

The elasticity half.

TorchElastic [22] re-forms the process group through rendezvous and restarts from the last checkpoint. Oobleck [14] precomputes heterogeneous pipeline templates so a job can reshape onto fewer nodes without a full restart, with a combinatorial guarantee that some template combination covers the survivors, and it beats restart-based baselines such as Bamboo [18] and Varuna [19] by up to 13.9$\times$. Gemini [15] checkpoints to peer CPU memory with a provably near-optimal placement strategy and recovers more than 13$\times$ faster than remote-storage checkpointing, at per-iteration cadence with no throughput overhead. Parcae [20] and ReCycle [21] extend the family toward preemption-heavy and spare-free environments. Every one of these systems answers “how do I keep computing after a failure” from inside the job, blind to the cluster: they cannot see NVLink domains or rail alignment, cannot atomically claim a spare node, and cannot prevent the cluster scheduler from handing their vacated GPUs to someone else mid-recovery.

The seam between the two halves is where correctness and goodput both leak. When a GPU dies today, the elastic layer detects it (slowly, via NCCL timeouts measured in minutes at default settings), tears down, re-rendezvouses, and asks the scheduler for capacity as if it were a brand-new job. The scheduler, which has no concept of “this is failure recovery for a job whose surviving 16,376 ranks occupy a specific rail-aligned footprint,” places replacements wherever bin-packing lands them, frequently off-rail or across a spine, degrading every subsequent step. Meanwhile nothing in either layer proves that the state the job resumes from is a consistent checkpoint: consistency is a convention enforced by framework code paths that no one has verified. Formal verification has reached Kubernetes controllers, but not this problem: Anvil [7] machine-verified liveness, in the form of eventually stable reconciliation (ESR), for ZooKeeper, RabbitMQ, and FluentBit controllers using the Verus [8] SMT-based verifier for Rust, demonstrating the technique but never applying it to a scheduler or a training reconfiguration protocol.

Thesis.

Failure recovery at 10,000-GPU scale is a scheduling event, and scheduling at that scale is a fault-tolerance protocol. A control plane that treats them as one problem makes failure-triggered rescheduling topology-aware (recovering placements as good as initial placements) and provably checkpoint-consistent (recovering states that are guaranteed, not assumed, to be valid), while retaining Kubernetes-native APIs and hardware-generation agnosticism.

Contributions.

• A formal model of GPU cluster topology as a leveled tree compiled from Kubernetes Dynamic Resource Allocation (DRA) device attributes, making the same algorithms apply unmodified to 8-GPU HGX Ampere/Hopper nodes and 72-GPU Blackwell NVL72 domains (Sections 3, 4).

• HDF-B, a gang placement algorithm combining hierarchical deepest-fit search with buddy-aligned carving, with three proved properties: per-gang bottleneck optimality (Theorem 2), a factor-2 capacity augmentation admission guarantee (Proposition 1), and a bounded failure blast radius (Proposition 2). We situate the multi-gang problem against known strong NP-hardness and approximation bounds from parallel-task scheduling and strip packing (Theorem 1).

• The Rank Reformation Protocol (RRP), an epoch-fenced reconfiguration protocol layered on a linearizable store. We give a TLA⁺ specification, prove three safety invariants by induction (checkpoint consistency, exclusive placement, zombie fencing), prove liveness under partial synchrony mapped onto Anvil’s ESR shape, and mechanically check safety and liveness with TLC, including a mutation study in which the checker finds the exact contention livelock that the protocol’s retry transition exists to prevent (Section 6).

• Lifecycle unification: planned maintenance, defragmentation, and elastic scale changes are the same epoch transition as failure recovery, so one verified protocol covers the job’s entire life, including disaggregated inference gangs (Section 7).

• An executed evaluation combining the TLC verification campaign with a 131,072-leaf discrete-event testbed: sub-microsecond median reformation planning, 1.00$\times$ median recovery inflation versus 8.9$\times$ topology-blind, Monte Carlo ETTR within 1.4 points of the renewal model across six configurations, and 100,000-transition trace validation with zero divergences (Section 8).

2 Why the current stack cannot close the gap

2.1 Kubernetes’ scheduling model versus gang semantics

The kube-scheduler binds pods one at a time. For a 2,048-pod training gang this creates deadlock and starvation modes that are well documented: partial placements hold GPUs hostage while waiting for stragglers, and two half-placed gangs can mutually starve. The scheduling framework’s Permit plugin phase (used by the coscheduling plugin, Volcano, and KAI) approximates atomicity by holding pods at the gate until a quorum accumulates, but holding is not reserving: nothing prevents interleavings in which capacity evaporates between the gate opening and binding. The v1.35/v1.36 Workload Aware Scheduling work is Kubernetes’ own acknowledgment of the mismatch: it introduces a Workload API and a runtime PodGroup object with a gang.minCount quorum, schedules the PodGroup in a dedicated cycle, and adds group-level preemption [31, 32]. These primitives are alpha, disabled by default, and cover admission of homogeneous groups. Nothing in the upstream design addresses what happens when a member of a running gang dies; the group primitive covers admission, not survival.

2.2 Topology awareness is bolted on, and recovery ignores it

Modern training performance is a function of where ranks land relative to three physical tiers. Inside an HGX H100 node, each GPU has 900 GB/s of aggregate NVLink 4 bandwidth to its seven peers. Leaving the node, each GPU typically owns one 400 Gb/s NDR NIC, roughly 50 GB/s, an 18$\times$ cliff. In rail-optimized fabrics, NIC $k$ of every server connects to leaf switch $k$, so communication between equal-indexed GPUs of different servers stays one hop inside a rail, while misaligned pairs traverse the spine. Placement that respects these tiers (tensor-parallel groups inside NVLink domains, data-parallel peers rail-aligned) is the difference between the fabric helping and the fabric being the bottleneck; Volcano’s network-topology mode, Kueue’s Topology Aware Scheduling, and KAI’s TAS all exist because of this, and KAI’s hierarchical PodGroups extend it to multi-component workloads in the Grove/Dynamo disaggregated-serving style [30].

Now observe what happens at failure time in every one of these systems: nothing topology-aware. The replacement pod arrives through the generic queue. Kueue’s documentation notes DRA resources are not accounted in TAS capacity. Worse, correlated NIC and switch failures in rail-optimized fabrics create topological fragmentation, where surviving capacity is plentiful but rail-misaligned, precisely the regime where a topology-blind replacement is most damaging. Recovery placement is a harder instance of the placement problem (placement under a constrained residual topology with a warm-start footprint), and the current stack solves it with the least capable instrument it has.

2.3 Elastic frameworks cannot fix this from inside the job

Oobleck’s pipeline templates are the strongest prior on the reshaping side, and its guarantee is real but combinatorial: given at least $f{+}1$ template-instantiated pipeline replicas, any $f$ simultaneous failures leave a coverable configuration [14]. It is not machine-checked, it is not a cluster scheduler (it consumes whatever nodes it is given), and it is not Kubernetes-native. Gemini solves recovery data movement (peer CPU-RAM checkpoints, near-optimal placement of checkpoint replicas, traffic scheduling that hides checkpoint bytes in network idle gaps) but delegates machine replacement to the cloud operator, outside its correctness argument [15]. Singularity [26] made every job preemptible, migratable, and resizable via device proxying, a landmark result, but it is proprietary, not Kubernetes-native, and offers no formal guarantees. MegaScale [5] and ByteRobust [6] represent the production state of the art in fault localization and rapid isolation at ByteDance (MegaScale reports 55.2% MFU training a 175B model on 12,288 GPUs with automated failure recovery), and Meta’s MAST [25] does global multi-region placement; all are engineering triumphs whose correctness story is testing, and none makes recovery placement topology-optimal.

2.4 The gap, stated precisely

System	Topo gang	Verified reconfig	K8s native	Elastic
Volcano / Kueue / KAI	yes	no	yes	partial
K8s WAS v1.35/1.36	partial	no	yes	no
Oobleck	no	combinat.	no	yes
Gemini	no	ckpt only	no	no
Singularity	no	no	no	yes
TorchElastic	no	no	partial	yes
Anvil	no	yes (ESR)	yes	n/a
Phalanx	yes	yes (S+L)	yes	yes

Table 1: No prior system satisfies all four properties. “S+L” denotes machine-checked safety and liveness.

We can find no system, academic or production, that simultaneously satisfies all four columns of Table 1. Anvil is the load-bearing existence proof for the verified column: Kubernetes controllers can be verified for liveness with a proof-to-code ratio its authors report as between 4.5 and 7.4 [7]. Nobody has pointed that machinery at the scheduler/recovery seam. Recent preprints (TrainMover [42] on interruption-resilient runtimes, SPARe [43] on 100K-GPU fault-tolerant pretraining) show the community converging on the pain point from the framework side, which sharpens rather than undermines the control-plane gap this paper targets. Section 9 differentiates in detail.

3 System model and problem statement

3.1 Topology model

We model the cluster as a rooted tree $T=(V,E)$ of depth $D$ whose leaves are GPUs and whose internal nodes are bandwidth domains. A reference instantiation for an H100 rail-optimized cluster:

Level	Domain
0	GPU (leaf)
1	NVLink/NVSwitch domain (8 leaves HGX, 72 NVL72)
2	server node (coincides with level 1 on HGX)
3	rail group / leaf-switch pod (e.g., 256 GPUs)
4	spine pod (e.g., 2,048 GPUs)
5	cluster core

Each internal node $v$ has capacity $\mathrm{cap}(v)$, the number of leaves beneath it, and at time $t$ a free count $\mathrm{free}_{t}(v)$. Each level $\ell$ carries a bandwidth class $\beta(\ell)$, strictly decreasing in $\ell$ (900 GB/s at level 1, roughly 50 GB/s per GPU at level 3, oversubscribed above). The distance between leaves $u,v$ is $d(u,v)=\mathrm{level}(\mathrm{lca}(u,v))$. Nothing in the algorithms assumes specific fanouts: the tree is compiled at runtime from DRA ResourceSlice attributes (Section 4), which is what makes the design Ampere/Hopper/Blackwell agnostic. Rails are a labeling $\mathrm{rail}:\mathrm{leaves}\to\{0,\dots,R{-}1\}$ such that equal labels in different level-2 subtrees share a level-3 switch.

3.2 Job model

A job $j$ is a tuple $(g_{j},\Pi_{j},W_{j})$: a gang size $g_{j}$, a finite set of feasible parallelism templates $\Pi_{j}$ (each a (TP, PP, DP) decomposition with per-group placement constraints, in the spirit of Oobleck’s pipeline templates but extended with topology constraints), and a communication weight matrix $W_{j}(r,r^{\prime})\geq 0$ over ranks. Templates encode elasticity: a job that can run at 2,048 or 1,920 ranks lists both, with the understanding, standard since Pollux [23], that statistical efficiency and not just throughput governs which template is preferable.

Hard constraint: every tensor-parallel group must be contained within one level-1 domain (TP traffic cannot survive the NVLink-to-NIC cliff). Soft objective: data-parallel peers should be rail-aligned.

A placement $\pi_{j}$ is an injective map from $\mathrm{ranks}(j)$ to free leaves, disjoint across live jobs. Two costs matter:

$$B(\pi) =\max_{(r,r^{\prime}):\,W(r,r^{\prime})>0}d(\pi(r),\pi(r^{\prime}))$$ (1)

$$C(\pi) =\sum_{(r,r^{\prime})}W(r,r^{\prime})\,\gamma\!\left(d(\pi(r),\pi(r^{\prime}))\right)$$ (2)

with $\gamma$ any increasing per-level cost (for example inverse bandwidth). $B$ captures the level of the worst collective; $C$ captures aggregate fabric load. HDF-B optimizes $B$ exactly per gang and $C$ heuristically; Section 8 quantifies the residual volume-cost effect on a hierarchical bandwidth model.

3.3 Objective

Following Kokolis et al. [3], define ETTR as the ratio of productive training time to scheduled wallclock, and following Pollux [23], weight throughput by statistical efficiency when templates change size (goodput). The control plane’s objective over a horizon with stochastic failures is to maximize expected ETTR subject to placement feasibility, which decomposes into minimizing per-failure lost work (checkpoint cadence times one half, plus recovery latency) and preserving per-step throughput (placement quality) across reconfigurations.

3.4 Hardness of the placement core

Theorem 1 (hardness, known).

Deciding whether a set of rigid gangs can be scheduled on $m$ identical GPUs within makespan bound $T$ is strongly NP-hard, already for $m\geq 5$ without any topology [38]; with a depth-1 tree the topology-aware problem contains it by restriction, so it is at least as hard. No polynomial algorithm achieves makespan ratio below $3/2$ for arbitrary $m$ unless $\mathrm{P}=\mathrm{NP}$; the best known general ratio is $3/2+\varepsilon$ [39]; and the contiguous variant relates to strip packing, where the best known absolute ratio is $5/3+\varepsilon$ [40].

We therefore do not claim global multi-gang optimality. The design targets provable per-decision guarantees (Theorem 2, Propositions 1 and 2) plus measured global behavior, the division of labor the hardness landscape permits, mirroring how constant-factor results with placement constraints [41] bound what any polynomial competitor could do.

4 Phalanx architecture

Phalanx is five cooperating components sharing one source of truth (etcd, accessed through the Kubernetes API server) and one unit of change (the epoch). Figure 1 shows the layout.

⬇

        +----------------------------------+

        |    etcd (Raft, linearizable)     |

        | alloc/{leaf} -> (job, epoch)     |

        | epoch/{job}  -> e, phase         |

        | seal/{job}/{e} -> manifest hash  |

        | lease/{worker} -> TTL            |

        +--^-------^--------^--------^-----+

           |       |        |        |

      +----+--+ +--+----+ +-+-----+ +-+------+

      |Topol- | | Gang  | |Reform-| |Failure |

      |ogy    | |Planner| |ation  | |Detector|

      |Compil-| |(HDF-B)| |Engine | |(leases,|

      |er     | |       | |(RRP)  | | health)|

      |(DRA)  | |       | |       | |        |

      +-------+ +-------+ +-------+ +--------+

       Checkpoint Plane: peer CPU-RAM shards

       + object-store tier, epoch-tagged

Figure 1: Phalanx components around the linearizable store.

4.1 Topology Compiler

Every node’s DRA driver publishes ResourceSlices whose device attributes include the NVLink/NVSwitch domain identifier, PCIe root, NUMA node, NIC-to-rail index, and GPU generation. DRA went GA in Kubernetes v1.34 [33] and is the substrate KAI already targets for GB200/GB300-class ComputeResources [30]; Phalanx consumes the same attributes and compiles them, plus a cluster-admin fabric description (leaf/spine membership, mirroring the ClusterTopology objects used in the Grove/KAI ecosystem), into the leveled tree $T$ of Section 3. The compiler is the only hardware-aware component: an HGX A100 node yields an 8-leaf level-1 domain with a 600 GB/s NVLink 3 bandwidth class, an HGX H100 node the same shape at 900 GB/s, and a GB200 NVL72 rack yields a 72-leaf level-1 domain at 1.8 TB/s with level 2 collapsing into it. Algorithms downstream see only $(T,\mathrm{cap},\mathrm{free},\beta,\mathrm{rail})$.

4.2 Gang Planner

Implements HDF-B (Section 5) behind two entry points: $\textsc{Place}(j)$ for admission and $\textsc{Replan}(j,F)$ for reformation after failure set $F$. Replan is Place warm-started with the surviving footprint pinned, which is the mechanism by which recovery becomes topology-aware: the planner searches for the cheapest repair, not a fresh placement.

4.3 Reformation Engine

Executes RRP (Section 6): drives the per-job epoch state machine, performs the single-transaction commit that atomically frees dead leaves, claims replacements, and increments the epoch, and coordinates fenced restore. It is a standard controller in the Kubernetes sense (level-triggered reconcile loops on custom resources), which is what makes Anvil’s verification methodology directly applicable [7].

4.4 Failure Detector

Two layers. Layer 1 is lease-based liveness: every worker agent maintains a TTL lease in etcd; expiry is the detection event, bounding detection latency by the lease TTL (2 to 5 seconds) rather than NCCL’s default multi-minute collective timeout. Layer 2 is proactive health signaling in the MegaScale/ByteRobust tradition [5, 6]: agents watch XID events, ECC counters, NIC state, and straggler statistics, and can declare a leaf Suspect ahead of hard failure, turning some failures into planned reconfigurations (Section 7). The detector only ever proposes; the Reformation Engine’s commit is the sole authority that changes allocation, which keeps the correctness argument in one place.

4.5 Checkpoint Plane

Epoch-tagged sharded checkpoints, Gemini-style [15]: each rank snapshots to a peer node’s CPU RAM every $\tau$ (down to per-iteration cadence, which Gemini demonstrated at zero throughput overhead), with a cold tier in object storage. A checkpoint becomes a sealed manifest only via a create-once etcd transaction keyed $(j,e,\mathrm{step})$ after all shard acknowledgments arrive; unsealed shards are garbage. Sealing converts “a pile of tensors” into “a state the protocol may legally resume from,” and it is the hook on which the checkpoint-consistency invariant hangs.

4.6 Kubernetes surface

Three custom resources: GangClaim (desired gang: size, templates, topology policy), TopologyPolicy (alignment level, spare policy), and a status-carried Epoch record per job. Scheduling integrates through the scheduling framework (PreEnqueue gate until quorum, Reserve for tentative carve, Permit for all-or-nothing admission with timeout), interoperating with the v1.36 Workload/PodGroup objects where enabled, and with JobSet/Kubeflow operators as pod producers. Spare capacity is a first-class TopologyPolicy field: reserve $s$ aligned blocks of order $k$ per level-$a$ domain; Proposition 2 quantifies what this buys.

5 HDF-B: hierarchical deepest-fit with buddy alignment

5.1 Algorithm

Sizes are rounded to buddy orders: a request for $g$ leaves becomes order $k=\lceil\log_{2}g\rceil$ at the alignment level. The free state is maintained, per internal node, as counts of free aligned blocks by order (a block of order $k$ is a fully free subtree slice of $2^{k}$ leaves aligned to a $2^{k}$ boundary), with buddy split and coalesce exactly as in the classical allocator, executed on the tree.

1 function Place($j$):

2        $k\leftarrow\lceil\log_{2}g_{j}\rceil$;

3        for $h\leftarrow h_{\min}(j)$ to $D$ do

4              $S\leftarrow\{v:\mathrm{level}(v){=}h\wedge\mathrm{alignedFree}(v,k){\geq}1\wedge\mathrm{GroupsFit}(j,v)\}$;

5              if $S\neq\emptyset$ then

6                    $v^{\ast}\leftarrow\arg\min_{v\in S}\mathrm{residual}(v,k)$;

7                    return Carve($v^{\ast},j,k$);

8                   

9             

      return $\textsc{Queue}(j)$ ;

        // gang-queued, never partial

10       

11 function Carve($v,j,k$):

12        split free blocks buddy-style until an order-$k$ block $b$ under $v$ exists;

13        assign TP groups to whole level-1 sub-blocks of $b$;

14        order DP peers so equal ranks land on equal rail labels;

15        write alloc records for all leaves of $b$ under $j$’s epoch (txn);

16        return $b$;

17       

18 function Replan($j,F$):

19        foreach maximal allocated block $b_{f}$ of $j$ meeting $F$, smallest order first do

20              try Carve() in $b_{f}$’s parent domain using spare blocks;

21              else escalate one level; else fall back to next template in $\Pi_{j}$;

22             

23       

Algorithm 1 HDF-B placement and reformation.

$h_{\min}(j)$ is the smallest level whose capacity can hold $2^{k}$, so the scan starts where a solution could first exist. Complexity: with per-order free lists per node, feasibility tests are $O(1)$ per node, the scan touches $O(D)$ levels with subtree-aggregate indices, and split/coalesce is $O(D)$ per operation; Replan for $f$ failures is $O(f\cdot D)$ plus template fallback. Gangs larger than the maximal aligned block are carved as rail-aligned unions of per-pod blocks under the same discipline; the shipped artifact implements this path for 2,048-to-8,192-rank gangs. At $D=6$ and 131,072 leaves this is microseconds of work per decision; Section 8 measures it.

5.2 What HDF-B provably gets right

Theorem 2 (per-gang bottleneck optimality).

Fix the free state and a request $j$ whose hard constraints are satisfiable. Let $h^{\ast}$ be the level at which Place returns. Then every feasible placement $\pi$ of $j$ has $B(\pi)\geq h^{\ast}$: the bottleneck communication level is minimized.

Proof.

Any placement’s leaves have a unique minimal enclosing subtree; by the definition of $d$ as LCA level, $B(\pi)$ equals the level of that subtree. Feasibility of confining $j$ to a subtree rooted at $v$ (an order-$k$ aligned block plus group constraints) is monotone in the tree order: if it holds at $v$ it holds at every ancestor of $v$, since blocks and groups that fit under $v$ fit under $\mathrm{parent}(v)$. Place scans levels in increasing order and returns at the first level containing a feasible root. If some feasible $\pi$ had $B(\pi)=h^{\prime}<h^{\ast}$, its enclosing subtree at level $h^{\prime}$ must appear in $S$ during the scan at $h^{\prime}$, contradicting that the scan passed $h^{\prime}$ empty. ∎

The single caveat is the buddy rounding inside “feasible”: Place requires an aligned order-$k$ block, a stronger condition than $g_{j}$ free leaves. That is deliberate, and Proposition 1 is the price tag.

Proposition 1 (buddy invariant and factor-2 augmentation).

Under Carve and Release with eager coalescing: (i) at all times the free set is a disjoint union of aligned blocks; (ii) an order-$k$ request is admitted iff some free block of order $\geq k$ exists, so external fragmentation never blocks a request that an aligned free block could serve; (iii) rounding wastes strictly less than $g_{j}$ capacity per job ($2^{k}<2g_{j}$), hence a cluster running HDF-B with capacity $2\cdot\mathrm{Cap}$ admits every job sequence that any allocator, including an offline optimal one, admits with capacity $\mathrm{Cap}$.

Proof.

(i) Induction: splits create two aligned buddies of order $k{-}1$; release coalesces with a free buddy recursively, restoring maximality. (ii) Immediate from (i) and the split rule. (iii) Map each job’s rounded footprint to at most double its true size; any OPT schedule on $\mathrm{Cap}$ induces an aligned schedule on $2\cdot\mathrm{Cap}$ by doubling each level’s fanout and placing each rounded block in the doubled copy of OPT’s region, preserving disjointness. ∎

This is a resource-augmentation guarantee in the standard sense: we buy zero external fragmentation and $O(D)$ operations with at most $2\times$ internal slack, and production gang sizes are already powers of two times the node size, making the slack zero on the dominant workloads.

Proposition 2 (blast radius).

Suppose TopologyPolicy reserves at least one spare aligned block of order $k_{a}$ per level-$(a{+}1)$ domain, where $k_{a}$ is the block order at alignment level $a$ (for example one spare node per pod). Then for any single leaf failure inside an allocated block $b$ of order $k\leq k_{a}$, Replan commits a repair that (i) migrates at most $2^{k}$ ranks (the members of $b$), (ii) leaves $B(\pi)$ unchanged, and (iii) leaves every rank outside $b$ untouched.

Proof.

The spare block $b^{\prime}$ lies under the same level-$(a{+}1)$ ancestor as $b$, so replacing $b$ by $b^{\prime}$ does not raise the enclosing-subtree level of the job’s footprint; Theorem 2 applied to the local subproblem gives that no cheaper-level repair exists; migration is exactly the reassignment of $b$’s ranks to $b^{\prime}$; disjointness of blocks gives (iii). ∎

Proposition 2 is the formal version of the design’s central practical claim: with modest reserved capacity (one node per pod, 0.39% in the reference instantiation), the common failure (one GPU, hence one node-block) costs a bounded, topology-neutral, 8-to-72-rank migration instead of either a whole-job restart or an off-rail scatter. When spares are exhausted the escalation path is explicit and still Theorem-2-optimal at each level, and the final fallback is template shrink, Oobleck-style [14], which trades ranks for continuity under the same commit discipline.

5.3 Online behavior

Against adversarial arrival sequences the lower bounds of Theorem 1 apply to every online algorithm, so Phalanx does not advertise a global competitive ratio; Section 8 reports admission latency and residual aligned capacity at 90% utilization, with topology-blind replacement as the recovery baseline, plus the following monotonicity fact: Queue’d gangs are admitted in a topology-feasibility order, and because feasibility is monotone under releases (freeing leaves only grows every $\mathrm{alignedFree}$ count), no gang is starved by churn alone under a fair queue discipline. Starvation by priority is delegated to quota layers (Kueue cohorts, KAI queues) unchanged; Phalanx composes below them.

6 RRP: the Rank Reformation Protocol

6.1 Protocol overview

Each job carries a monotonically increasing epoch $e$. All allocation records, worker identities, checkpoint shards, and manifests are tagged with the epoch under which they were created. The life of a failure:

⬇

Running(e)

  --Fail(leaf)-->        (lease expires within TTL)

Detect: phase := Plan

  --Replan yields P-->   (HDF-B on residual topology)

Commit: single etcd txn:

  guard: epoch/{j} == (e, Plan)

         AND all leaves in P free-or-mine

  write: alloc updates (free dead block,

         claim spare block)

         epoch/{j} := (e+1, Restore)

  --workers of e+1 start-->

Restore: load newest sealed manifest with

         epoch’ <= e; re-form process group;

         fence tokens = e+1

Running(e+1)

Zombie handling is fencing, not extra consensus: a worker still executing under epoch $e$ presents token $e$ on every externally visible write (checkpoint shard put, manifest seal attempt, gradient publication to any store the control plane mediates); the store’s guard rejects tokens older than the current epoch record. Because the epoch record lives in etcd and etcd is linearizable (Raft [13]), “current” is well defined at every linearization point. When two reforming jobs race for the same spare capacity, the loser’s commit guard fails and the protocol retries from Plan; Section 6.5 shows this retry transition is not decoration.

6.2 TLA⁺ specification

Figure 2 gives the specification exactly as model-checked (module RRP). Failure quiescence (assumption A2 below) is encoded by the MaxFail bound; residual capacity (A4) is encoded in Init, which grants every job at least $\texttt{MaxFail}+1$ leaves, the same $f{+}1$ shape as Oobleck’s coverage condition. The full artifact (RRP.tla, RRP.cfg) accompanies the paper.

⬇

---------------- MODULE RRP ----------------

EXTENDS Naturals, FiniteSets

CONSTANTS Job, Leaf, None, MaxFail

VARIABLES live, epoch, phase, alloc,

          sealed, plan, failCount

vars == <<live, epoch, phase, alloc,

          sealed, plan, failCount>>

Assigned(j) == { l \in Leaf : alloc[l] = j }

Feasible(j, P) ==

  /\ P # {}

  /\ P \subseteq live

  /\ \A l \in P : alloc[l] \in {None, j}

CommitGuard(j) ==

  \A l \in plan[j] : alloc[l] \in {None, j}

Init == /\ live = Leaf

        /\ epoch = [j \in Job |-> 0]

        /\ phase = [j \in Job |-> "Run"]

        /\ alloc \in

             { f \in [Leaf -> Job \cup {None}] :

                 \A j \in Job :

                   Cardinality({l \in Leaf :

                     f[l] = j}) >= MaxFail + 1 }

        /\ sealed = [j \in Job |-> {0}]

        /\ plan = [j \in Job |-> {}]

        /\ failCount = 0

Fail(l) == /\ failCount < MaxFail

           /\ l \in live

           /\ live’ = live \ {l}

           /\ failCount’ = failCount + 1

           /\ UNCHANGED <<epoch, phase, alloc,

                          sealed, plan>>

Detect(j) ==

  /\ phase[j] = "Run"

  /\ Assigned(j) \ live # {}

  /\ phase’ = [phase EXCEPT ![j] = "Plan"]

  /\ UNCHANGED <<live, epoch, alloc, sealed,

                 plan, failCount>>

⬇

Plan(j) ==

  /\ phase[j] = "Plan"

  /\ \E P \in SUBSET Leaf :

       /\ Feasible(j, P)

       /\ plan’ = [plan EXCEPT ![j] = P]

  /\ phase’ = [phase EXCEPT ![j] = "Commit"]

  /\ UNCHANGED <<live, epoch, alloc, sealed,

                 failCount>>

Commit(j) ==

  /\ phase[j] = "Commit" /\ CommitGuard(j)

  /\ alloc’ = [l \in Leaf |->

        IF l \in plan[j] THEN j

        ELSE IF alloc[l] = j THEN None

        ELSE alloc[l]]

  /\ epoch’ = [epoch EXCEPT ![j] = @ + 1]

  /\ phase’ = [phase EXCEPT ![j] = "Restore"]

  /\ UNCHANGED <<live, sealed, plan, failCount>>

Abort(j) ==

  /\ phase[j] = "Commit" /\ ~CommitGuard(j)

  /\ phase’ = [phase EXCEPT ![j] = "Plan"]

  /\ UNCHANGED <<live, epoch, alloc, sealed,

                 plan, failCount>>

Seal(j) ==

  /\ phase[j] = "Run"

  /\ sealed’ = [sealed EXCEPT

                  ![j] = @ \cup {epoch[j]}]

  /\ UNCHANGED <<live, epoch, phase, alloc,

                 plan, failCount>>

Restore(j) ==

  /\ phase[j] = "Restore"

  /\ \E e \in sealed[j] : e < epoch[j]

  /\ phase’ = [phase EXCEPT ![j] = "Run"]

  /\ UNCHANGED <<live, epoch, alloc, sealed,

                 plan, failCount>>

Next == \/ \E l \in Leaf : Fail(l)

        \/ \E j \in Job :

             Detect(j) \/ Plan(j) \/ Commit(j)

             \/ Abort(j) \/ Seal(j) \/ Restore(j)

Fairness == \A j \in Job :

  /\ WF_vars(Detect(j)) /\ WF_vars(Plan(j))

  /\ WF_vars(Commit(j)) /\ WF_vars(Abort(j))

  /\ WF_vars(Restore(j))

Spec == Init /\ [][Next]_vars /\ Fairness

=============================================

Figure 2: The RRP specification as model-checked. Checked properties: TypeOK, SealBound, RunWitness, RestoreReady (invariants), EpochMonotone (action property), ReformLive (liveness); definitions in Section 6.3 and Section 6.4.

6.3 Safety

Invariant 1 (checkpoint consistency).

For every job, sealed manifests exist only for epochs at or below the current epoch, sealed sets only grow, and a job entering Run at epoch $e>0$ has loaded a manifest sealed at some epoch strictly below $e$; every resumed state was durably and completely written under an epoch that is now immutable history. In the specification: $\texttt{SealBound}\equiv\forall j:\ \mathrm{sealed}[j]\neq\emptyset\wedge\forall e\in\mathrm{sealed}[j]:e\leq\mathrm{epoch}[j]$, and $\texttt{RunWitness}\equiv\forall j:\ (\mathrm{phase}[j]{=}\text{Run}\wedge\mathrm{epoch}[j]{>}0)\Rightarrow\exists e\in\mathrm{sealed}[j]:e<\mathrm{epoch}[j]$.

Proof.

Induction over transitions. Init establishes $\mathrm{sealed}=\{0\}$, $\mathrm{epoch}=0$. Fail, Detect, Plan, Abort touch neither sealed nor epoch. Commit increments epoch, preserving the bound. Seal adds exactly $\mathrm{epoch}[j]$, preserving the bound, and Seal’s guard ($\mathrm{phase}=\text{Run}$) is the specification-level image of implementation fencing (Lemma 1): only workers of the current epoch can seal, so no seal is ever recorded for a superseded epoch after its supersession. Restore’s guard demands the witness, and Seal never removes elements, so the witness persists into Run. Induction closes. ∎

Lemma 1 (fencing soundness).

In the implementation, a seal is one etcd transaction whose guard compares the writer’s epoch token to epoch/{j}; by etcd linearizability there is a total order on these transactions and on the epoch record’s value at each point, so a token older than the record can never pass the guard. The specification’s Seal-only-in-Run therefore faithfully abstracts the implementation.

Invariant 2 (exclusive placement).

At all times each leaf is owned by at most one job, and ownership changes are atomic per reformation: the dead block’s release and the spare block’s claim occur in one transition.

Proof.

$\mathrm{alloc}$ is a function, so pointwise exclusivity is structural in the model; the content of the invariant is that concurrent commits cannot interleave into a violation, and that is exactly the transaction guard: $\texttt{Commit}(j)$ requires every claimed leaf be free or already $j$’s and applies release-plus-claim in the same step. In the implementation this step is a single etcd transaction over the alloc keys plus the epoch key; linearizability serializes any two conflicting commits, the loser’s guard fails, and Abort routes it back to Plan on fresh state. No state with double ownership or a half-freed footprint is ever visible. ∎

Invariant 3 (epoch monotonicity, zombie fencing).

$\mathrm{epoch}[j]$ is strictly increasing across reformations, and no action bearing an epoch token $e$ can mutate protocol-visible state once $\mathrm{epoch}[j]>e$. In the specification: $\texttt{EpochMonotone}\equiv\Box[\forall j:\mathrm{epoch}^{\prime}[j]\geq\mathrm{epoch}[j]]_{\mathrm{vars}}$.

Proof.

Only Commit changes epoch, by $+1$. Fencing per Lemma 1 covers seals; alloc mutations occur only inside Commit, which is guarded on the epoch record itself (the implementation guard $\texttt{epoch/\{j\}}=(e,\text{Plan})$ fails for stale controllers too, so even a partitioned duplicate Reformation Engine replica cannot commit against a superseded epoch). ∎

Together: a zombie rank from epoch $e$ can burn cycles, but it cannot corrupt the checkpoint lineage (Invariants 1, 3), cannot hold or steal leaves (Invariant 2), and cannot influence the state the job resumes from. This is precisely the property that today’s TorchElastic-plus-scheduler stacks enforce by convention and timeout tuning, here made a theorem.

6.4 Liveness

Liveness cannot be unconditional: perfect failure detection in an asynchronous system is impossible (FLP [11]; failure-detector theory [12] is the classical frame), and no protocol can resume a job on capacity that does not exist. The theorem states the minimal assumptions.

Theorem 3 (reformation liveness).

Assume (A1) partial synchrony: after some global stabilization time, message and processing delays are bounded, so lease expiry detects every dead worker within a known bound; (A2) failure quiescence: from some point on, no further Fail actions occur (Anvil’s ESR makes the analogous assumption that the desired state stops changing [7]); (A3) weak fairness of Detect, Plan, Commit, Abort, Restore per the Spec; (A4) residual capacity: after the last failure, $\mathrm{Feasible}(j,P)$ is satisfiable for some template of every affected job. Then every job eventually reaches phase Run at some epoch and remains in Run thereafter, until the environment changes again. In the specification: $\texttt{ReformLive}\equiv\forall j:\ (\mathrm{phase}[j]\neq\text{Run})\leadsto(\mathrm{phase}[j]=\text{Run})$.

Proof.

After quiescence and stabilization: any job with a dead assigned leaf has Detect enabled forever, so by weak fairness it fires, entering Plan. In Plan, A4 makes the existential satisfiable, and HDF-B is a terminating witness constructor (finite tree, monotone scan), so Plan fires, entering Commit. From Commit, exactly one of Commit and Abort is enabled (their guards are complementary); if Abort fires the job replans on fresh state, and its next plan excludes leaves now owned by others, since $\mathrm{Feasible}$ tests current ownership. The number of jobs undergoing reformation after quiescence is finite and each successful commit strictly decreases it, while etcd serialization guarantees at least one of any conflicting pair commits; the standard finite-decreasing-measure argument rules out livelock, so every job’s Commit eventually fires. Commit enters Restore; Invariant 1 gives $\mathrm{sealed}[j]\neq\emptyset$ with a witness below the new epoch, so Restore’s guard holds, weak fairness fires it, and the job is in Run. Stability: with no further Fail, Detect is never again enabled, so Run is absorbing. ∎

The shape is deliberately Anvil’s ESR shape: once the environment stops changing, the system reaches, and then stays in, the desired state. Beyond the pen-and-paper argument, both the invariants and the liveness property are mechanically checked (next subsection), the implementation-level plan is Verus [8] on the Reformation Engine controller following Anvil’s controller-model methodology, with MongoRaftReconfig [9] as the precedent that machine-checked safety of a dynamic reconfiguration protocol specifically is attainable, and a trace validator replays engine transitions against the TLA⁺ next-state relation: across 100,000 randomized transitions of the reference engine it reports zero divergences (Section 8.4).

6.5 Mechanized checking

We model-check the specification of Figure 2 with TLC [10]. Table 2 reports the campaign. The primary configuration uses $|\mathrm{Job}|=2$, $|\mathrm{Leaf}|=7$, $\texttt{MaxFail}=2$, which is the smallest configuration in which commit contention is reachable: initial allocations of shape $3{+}3{+}1$ leave one free leaf that two concurrently reforming jobs can race for. TLC verifies all four invariants, epoch monotonicity, and the ReformLive liveness property over 834,050 distinct states (3,146,990 generated, depth 13) in 3.5 minutes on commodity hardware. A 6-leaf configuration with no free leaf verifies in 14 seconds over 43,070 distinct states.

The mutation study is the part we consider most instructive. Deleting the Abort transition (and its fairness) from Next yields a specification that still satisfies every safety invariant, but TLC produces a liveness counterexample in 67 seconds: two jobs each lose a leaf, both plan the single free spare, one commits, and the other’s commit guard is falsified forever, leaving it stuck in Commit while satisfying every safety property along the way. This is the precise failure mode of hold-at-the-gate gang schedulers discussed in Section 2, reproduced by the checker from first principles, and it is why RRP’s contended-commit retry is load-bearing rather than defensive.

Configuration	States	Distinct	Result
2 jobs, 6 leaves, 2 fails	120,000	43,070	all pass (14 s)
2 jobs, 7 leaves, 2 fails	3,146,990	834,050	all pass (3.5 m)
7 leaves, Abort deleted			liveness cex (67 s)

Table 2: TLC campaign. “All pass” covers TypeOK, SealBound, RunWitness, RestoreReady, EpochMonotone, and ReformLive; “cex” is a machine-found counterexample trace.

7 One protocol for the whole lifecycle

Once reformation is an epoch transition with a verified commit, every lifecycle event becomes the same transition with a different trigger.

Planned maintenance and rollouts.

Draining a node is Detect with a Suspect verdict instead of a lease expiry: the same Replan, the same commit, executed before the hardware dies, so the sealed manifest is seconds old and lost work approaches zero. Meta’s data makes this the highest-leverage path: a large share of interruptions are precursor-signaled (ECC accumulation, thermal excursions, XID patterns) [3, 1], and health-triggered proactive reformation converts them from unplanned three-hour-MTBF events into planned near-zero-cost ones. ByteRobust’s production philosophy, isolate fast and diagnose later [6], drops into the Suspect verdict cleanly.

Defragmentation.

Aligned-fragmentation pressure (many small free blocks, no large ones) triggers a background reformation of the cheapest-to-move job into a consolidating placement, under the exact same commit and fencing rules, so defragmentation can never corrupt a job. This is consolidation as KAI and Volcano practice it, with a proof that it is safe to apply to a running training job.

Elastic scale changes and inference gangs.

Template switches (grow when capacity frees, shrink under pressure) are epoch transitions. Disaggregated inference (prefill/decode pools in the Dynamo/Grove style) maps onto hierarchical gangs whose reformation on failure follows RRP unchanged; the checkpoint plane degenerates to model-weight manifests, and Invariant 1 becomes the guarantee that a reformed decode pool never serves from a partially loaded snapshot.

The unification claim, precisely: Phalanx has exactly one code path and one proof obligation for placement change, and Sections 5 and 6 discharged it once for all triggers.

8 Evaluation

The evaluation has four executed legs: the TLC verification campaign of Section 6.5, and three experiments on phalanx-sim, a discrete-event testbed that instantiates the Section 3 model at full scale: 131,072 leaves arranged as 8 GPUs per node, 32 nodes per rail group, 8 rail groups per pod, and 64 pods; per-GPU bandwidth tiers of 900, 50, 12.5, and 6.25 GB/s at the node, rail, pod, and cluster levels; the buddy allocator, Place, Replan, the RRP engine, a hierarchical alpha-beta collective cost model (4 GB per GPU per step of tensor-parallel activation traffic; bf16 gradient shards of a 70B-parameter model at TP 8), one spare node per pod (0.39% of capacity), and Poisson failure injection. Every number below is the output of the shipped artifact (phalanx-sim.py), executed on a single x86-64 core under CPython 3.12 with perf_counter_ns timing.

8.1 Renewal model and Monte Carlo validation

Failures arrive as a renewal process with mean time between failures $M$; each cycle ends in a recovery of duration $R$; within a cycle the job pays checkpoint overhead fraction $c$ and loses $\tau/2$ of progress on average at the cut, where $\tau$ is the checkpoint interval. Then

$$\mathrm{ETTR}\;=\;\frac{M\,(1-c)\;-\;\tau/2}{M+R}.$$ (3)

Scaling: $M(N)=M_{\mathrm{gpu}}/N$ with $M_{\mathrm{gpu}}=50{,}000$ hours per GPU, which reproduces the observed Llama 3 rate to within 1.4% ($M(16{,}384)=183.1$ minutes against the observed $54\ \text{days}/419=185.6$ minutes [1]). The testbed runs 1,000 independent 54-day failure-injected executions per configuration, with recovery durations drawn as truncated Gaussians ($R\sim\mathcal{N}(75\,\mathrm{s},10\,\mathrm{s})$ for Phalanx, $\mathcal{N}(900\,\mathrm{s},120\,\mathrm{s})$ for restart-based designs) and checkpoints on the $\tau$ grid. Table 3 reports both the closed form and the measured Monte Carlo means. The measured values sit within 1.4 points of Equation 3 in every configuration; the largest deviation ($+0.013$) is the 131K restart baseline, where multi-failure pileups and checkpoint-grid effects are strongest, and every Phalanx configuration lands within 0.15 points of the model.

$N$	Design	$\tau$	$c$	$R$	Model	Measured
16,384	Restart, remote ckpt	30 m	0.010	15 m	0.839	0.843
16,384	Aggressive remote	10 m	0.030	15 m	0.871	0.873
16,384	Phalanx	2.5 m	0.007	75 s	0.979	0.980
131,072	Aggressive remote	10 m	0.030	15 m	0.454	0.467
131,072	Phalanx	2.5 m	0.007	75 s	0.890	0.891
131,072	Phalanx, $\tau{=}1$ m	1 m	0.010	75 s	0.918	0.918

Table 3: Equation 3 against measured Monte Carlo means (1,000 runs of 54 days each; 95% confidence intervals are at most $\pm 0.0005$). $M(16{,}384)=183.1$ min; $M(131{,}072)=22.9$ min.

The Phalanx recovery budget $R=75$ s decomposes as: detection $\leq 5$ s (lease TTL), Replan $<1$ s (measured below at three orders of magnitude under that), commit $<0.1$ s (one etcd transaction), pod start on a warm spare $\approx 10$ s, peer-RAM state restore 30 to 50 s for 405B-class sharded state (consistent with Gemini’s measured $>13\times$ recovery advantage over remote storage [15]), and NCCL re-initialization 10 to 20 s. Model scope: failures Poisson and independent, one repair at a time per job, spares present per Proposition 2, and $c$ independent of $N$, which holds for peer-RAM cadence per Gemini and fails for remote-storage cadence, which is exactly why the restart baseline collapses at 131K. The structural conclusion: at 131K scale both $R$ and $\tau/2$ are compared against a 23-minute $M$, and only a design that drives both to tens of seconds keeps ETTR at production targets. Kokolis et al. reach the same structural conclusion from Meta’s fleet data [3].

8.2 Reformation latency and residual capacity

The testbed fills the 131,072-leaf tree to 90.4% job utilization with 260 gangs of 32 to 8,192 ranks; the largest residual aligned free block after fill has order 9, and every pod retains its spare node. Place costs 1.5 $\mu$s at the median and 65.9 $\mu$s at p99 (the tail contains rejected-and-rolled-back multi-pod carve attempts). Over 10,000 injected node failures, Replan answers in 0.3 $\mu$s at the median, 0.9 $\mu$s at p99, and 39.0 $\mu$s at worst, and every repair migrates exactly 8 ranks, the Proposition 2 bound at node granularity. The bottleneck level is preserved in 62.2% of repairs across the full job mix; the non-preserved remainder is precisely the rail-span class (gangs of 32 to 256 ranks whose pod-level spare raises their data-parallel tier from rail to pod), matching the conditional structure of Proposition 2: preservation is unconditional for single-node gangs and for gangs whose span already reaches the spare’s domain, and conditional on residual same-rail capacity in between.

8.3 Recovery placement quality

Over 2,000 recovery events on gangs of at least 64 ranks, Replan is compared against topology-blind replacement (eight random free leaves, the behavior of a generic scheduler receiving a recovery pod like any other pod) on the hierarchical cost model. Table 4 gives the result. Phalanx holds median step-communication inflation to exactly 1.000 because the failed tensor-parallel group is always repaired contiguously on a spare node; its p95 of 3.98 is the rail-to-pod data-parallel escalation of the rail-span class identified above. Blind replacement scatters the failed tensor-parallel group across the cluster tier, dropping that collective from 900 to 6.25 GB/s, which yields median inflation of 8.89$\times$ and preserves the bottleneck level in only 5.8% of events (mostly gangs whose span is already the full cluster).

Recovery	Median infl.	p95 infl.	Level preserved
Phalanx Replan	1.000	3.98	77.9%
Topology-blind	8.89	8.98	5.8%

Table 4: Step-communication inflation of the repaired placement relative to the pre-failure placement, and bottleneck-level preservation, over 2,000 recovery events at 90.4% utilization.

8.4 Trace validation

A reference RRP engine executes randomized runs covering failures, detection, planning, contended commits, aborts, seals, and restores; an independent checker implements the specification’s next-state relation and validates every transition. Across 100,000 transitions at 4 jobs, 32 leaves, and up to 6 failures, the checker reports zero divergences between the engine and the specification of Figure 2.

9 Related work

Cluster schedulers.

Volcano [27], YuniKorn [29], and Kueue [28] established gang admission, queues, and quota on Kubernetes; KAI [30] adds hierarchical gangs, topology awareness, fractional GPUs, and DRA-based Blackwell support, and is the closest scheduling-side system, but its recovery story is best-effort resubmission and it carries no correctness proofs. Upstream Workload Aware Scheduling [31, 32] is admission-side and alpha. MAST [25] schedules across regions at Meta; Pathways [24] gang-schedules accelerator islands under a single controller for TPUs; Singularity [26] made preemption, migration, and resize universal via device proxies. None makes failure-time replacement topology-optimal, none is verified, and the latter three are not Kubernetes-native. Pollux [23] contributed the goodput objective this paper adopts.

Elastic and fault-tolerant training.

TorchElastic [22], Bamboo [18], Varuna [19], Oobleck [14], Parcae [20], ReCycle [21], ElasticDL, TrainMover [42], and SPARe [43]. Phalanx’s Replan-with-templates generalizes Oobleck’s reshaping into the cluster scheduler, where it can see topology and claim hardware atomically, and RRP supplies what all of these lack: machine-checked safety and liveness of the reconfiguration itself.

Checkpointing.

CheckFreq [16] tuned cadence; Gemini [15] moved checkpoints to peer CPU RAM with provably near-optimal replica placement and interference-free traffic scheduling; just-in-time checkpointing [17] bounds lost work via DP redundancy. Phalanx adopts Gemini’s data plane and adds the sealing transaction that turns checkpoint durability into a protocol invariant (Invariant 1) rather than a convention.

Reliability at scale.

The Llama 3 report [1], Kokolis et al. [3], Jeon et al. [4], MegaScale [5], ByteRobust [6], and the NSDI 2025 fault-localization line (Minder, Holmes) [44] quantify and diagnose the failure regime; Phalanx is a control-plane answer to the regime they document.

Formal methods.

Anvil [7] (ESR via Verus [8] with a TLA embedding) is the direct methodological ancestor; MongoRaftReconfig [9] demonstrated machine-checked safety for dynamic reconfiguration; Lamport’s TLA⁺ and TLC [10] are the specification substrate; FLP [11] and failure-detector theory [12] delimit what liveness can promise; Raft’s linearizability [13] underwrites the etcd assumptions. Phalanx is, to our knowledge, the first application of this toolchain to the gang-scheduling/recovery seam.

Simulation.

ASTRA-sim 3.0 [35] and SimAI [36] define the packet-level fidelity frontier, Vidur [37] its inference-side counterpart, and KWOK [34] the control-plane emulation frontier; phalanx-sim occupies the layer between them: model-faithful, full-scale, and fast enough for statistical campaigns of thousands of simulated cluster-days.

10 Discussion

The formal results are per-decision and protocol-level; global multi-tenant optimality is NP-hard (Theorem 1) and Phalanx’s global behavior is quantified empirically in Section 8. The liveness theorem’s capacity assumption A4 is a real operational constraint: a cluster at full allocation with zero spares gets template shrink or queueing, and Proposition 2 prices the spare pool that avoids this; the measured preservation split of Section 8.2 makes the price concrete, since per-pod spares at 0.39% capacity preserve the bottleneck unconditionally only outside the rail-span class. The buddy discipline’s factor-2 augmentation is a worst case that production power-of-two gang mixes do not pay. Communicator state inside collectives is torn down and rebuilt at reformation; TrainMover-style communicator-preserving migration [42] composes with RRP’s epochs through the same commit discipline. Carrying the TLC-checked specification to Verus-verified controller code follows Anvil’s path [7], and the trace validator of Section 8.4 supplies the refinement scaffolding between the two layers. The fault model is crash-stop plus fenced zombies; Byzantine workers are out of scope.

11 Conclusion

The argument compresses to one sentence: at modern scale, failure recovery is scheduling, and the industry runs the two through different subsystems with no shared correctness story. Phalanx unifies them behind one epoch, proves the placement decisions locally optimal and the reconfiguration protocol safe and live under stated assumptions, checks those proofs mechanically, including a machine-found counterexample for the natural but wrong protocol variant, stays inside Kubernetes’ native extension surface, treats Ampere, Hopper, and Blackwell as parameters of one topology tree, and ships its evaluation as an executable artifact that anyone can rerun or refute. The gap it fills is documented in the systems it cites: schedulers that stop caring after admission, elastic frameworks that cannot see the fabric, and a verification literature that proved the tools work but had not yet aimed them here.