Bitwise Reproducibility as an Incomplete Correctness Signal: A Structural Audit for Parallel Spectral GCMs

Dmitrii Vokhmintsev 

Bitwise reproducibility of an OpenMP-parallelized scientific code is usually verified by checksum comparison on a short run—an inductive leap that carries no guarantee at longer integration lengths. We study it instead as a deductive and diagnostic property of the source text, taking a legacy spectral atmospheric general circulation model, whose time step is a reduction over a partitioned latitude dimension, as the concrete instance. We isolate four source-level conditions, (C0)–(C3): determinism of the inner transform reductions, a fixed-order outer reduction, per-iteration state isolation, and disjoint per-thread writes—two ordering conditions (C0, C1) and two independence conditions (C2, C3). Under them and an IEEE-754 determinism assumption, the output is bit-identical across all thread counts on a fixed binary for arbitrary integration length—a property we call thread-count-invariant bitwise reproducibility, strictly stronger than the fixed-thread-count rerun determinism a single-configuration checksum verifies; we establish it as a lemma. The lemma's per-iteration factorization frames the paper's diagnostic point: an across-thread reproducibility check detects an inter-iteration state-leakage fault only when the fault's effect on the checksummed output varies with the thread count. Driving the model to bit-identity, we exposed a real, long-undetected leak in its vertical-exchange cache for exactly that reason; but the check is, by construction, blind to a leak whose effect is thread-count-invariant—one that stays bit-identical across threads while corrupting the physics—a blind spot independent of which reproducible-summation algorithm produces the checksum. A structural audit of the state-isolation condition detects such leaks directly, independent of thread count, so bitwise reproducibility, however obtained, is a sound but incomplete correctness signal that the audit complements rather than replaces. We give (C0)–(C3) as a reusable audit checklist for any partitioned-reduction OpenMP loop, sketch how they transfer to other spectral cores, and point to a companion empirical study that confirms bit-identity across thread counts on two hardware platforms. The structural conditions are exercised on a single legacy model, but the diagnostic itself is additionally demonstrated on a small open synthetic kernel that anyone can run.