How Ashiba attributes silent-correctness failures across silicon.
Two ML kernels can disagree numerically, both pass functional tests, and both be — depending on the contract — correct. There is no formal artifact today against which "correct" can be graded. That is the specification gap. Kernel Contracts is the language that closes it.
A kernel contract is an eight-part formal object:
All twelve contract classes group under three physically-grounded failure primitives:
Path dependence. The result depends on an evaluation order the contract allows to vary. Root cause: IEEE 754 non-associativity combined with non-deterministic parallel scheduling.
Domain violation. The operator encounters inputs outside its valid domain — subnormals, NaN, overflow, out-of-range indices. Root cause: finite precision combined with unconstrained input distributions.
Resource contention. The result depends on concurrent access to shared silicon resources — atomics, memory-model reorderings, collective-operation arbitrations. Root cause: shared-memory concurrency combined with silicon-specific arbitration policies.
Three primitives, twelve manifestations, one framework.
Our methodology adapts forty years of silicon-test engineering — Shewhart statistical process control, ATPG coverage mathematics, Huang-Abraham algorithm-based fault tolerance, Freivalds probabilistic verification — to the ML kernel domain. For a given workload we deliver:
Shewchuk 1997 on adaptive-precision geometric predicates. Demmel and Nguyen on ReproBLAS. Wilkinson's backward error analysis. Bates on approximate-computing error debt. The silicon-test lineage: Shewhart SPC, ATPG, Huang-Abraham ABFT, Freivalds. Each contributes one component of the framework. The port from silicon test to ML kernel is the work.