Validating Memory-Optimal Transformer Kernels on Real Hardware: From Formal Derivation to Measured Performance Across Two HPC Clusters

arXiv:2609.33916v1, titled "Validating Memory-Optimal Transformer Kernels on Real Hardware: From Formal Derivation to Measured Performance Across Two HPC Clusters," is a companion paper by Lenore M. Mullin and Gaetan Hains that empirically validates theoretical derivations from Papers I–IV. Submitted on September 27, 2026, it tests kernels derived via the Mathematics of Arrays (MoA) framework against real hardware performance on the Purdue Anvil and NCSA Delta HPC clusters.

The study confirms that MoA’s Denotational Normal Form (DNF) and Operational Normal Form (ONF) pipeline accurately predicts hardware behavior, with three key findings: GPU Regression Fix: A fused forward+backward kernel initially suffered from atomic contention; a targeted ONF rewrite reversed this, yielding up to 2.5x speedup. Topology Dependency: Identical derivations produced markedly different costs based on machine topology, showing a 535x NUMA-locality penalty on Delta versus less than 3x oversubscription cost on Anvil. * Language Anomaly: Identical computations ran faster in C than Fortran on CPU, but faster in Fortran than C on GPU, linked to specific memory-latency stalls.

The paper advocates treating hardware-specific optimization as a routine ONF rewrite while keeping the underlying DNF fixed and verified, offering a scalable methodology for AI deployment on evolving hardware.

This paper provides the empirical validation layer for a family of memory-optimal transformer kernels derived using the Mathematics of Arrays (MoA). It focuses on kernels for attention forward and backward passes, fused forward+backward, decode, and a complete transformer block including RMSNorm and a gated MLP. The kernels are first specified as a hardware-independent dataflow or DNF representation, then transformed into machine-specific realizations and evaluated on two HPC clusters. The central question is whether the formally derived memory-cost objectives, which are meant to minimize data movement and improve reuse, translate into predictable performance when executed on real accelerator and memory subsystems.

A key contribution is the bridge between formal kernel derivation and measured systems behavior. Rather than treating the MoA-derived cost functions as purely symbolic, the paper tests them against actual execution on representative HPC hardware, comparing predicted memory-optimal behavior with observed performance. The likely insight is that the formal model captures the dominant memory-traffic structure of transformer computation, but real-world performance is also shaped by hardware-specific effects such as cache hierarchy, memory bandwidth, vectorization, synchronization, and layout-dependent access patterns. By validating across two clusters, the work also highlights how portable the derived cost model is and where cluster- or architecture-specific calibration may be needed.

This matters because transformer kernels are a major bottleneck in both training and inference, and current practice often relies on expensive manual tuning or heuristic compiler search. A validated formal framework can make kernel generation more systematic, reproducible, and portable across heterogeneous HPC platforms. If the derived cost functions reliably predict or guide memory behavior, they can be used to design efficient transformer implementations without starting from scratch for each accelerator, improving the connection between array mathematics, compiler theory, and high-performance AI systems.