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, all three being per-placement guarantees rather than global multi-tenant claims, since we prove the global objective NP-hard; (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 × against 8.9 × 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, under a recovery-latency model calibrated to published peer-RAM restore figures, effective training time ratios of 0.980 at 16K GPUs and 0.891 at 131K GPUs where the restart-based baseline measures 0.467, with a sensitivity sweep confirming that fast in-memory recovery dominates restart across the entire plausible range of the assumed parameters. 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.