Module Ir.Numerics

Numerics policy (gh-ocannl-478's "option 3" knob): compute-precision decisions that change results, so they are chosen by the user — via the global config or set_policy — never by the optimizer. Storage precisions live on tensor nodes (Tnode.t.storage_prec); this record governs how computations over those storages are carried out. It must be identical across sibling autotune candidates: candidate schedules compete on speed, never on numerics (the bitwise-parity discipline of the tensorized twins depends on it).

The record is deliberately open-ended — later compute-precision questions (fast-math transcendentals, accumulation widths, fp8 format selection per tensor class, gh-ocannl-492) land here rather than growing ad-hoc booleans elsewhere.

type fp16_mode =
  1. | Fp16_auto
  2. | Fp16_narrow
  3. | Fp16_wide

The fp16 compute/accumulator mode (gh-ocannl-680, refining gh-ocannl-516's boolean).

  • Fp16_auto (the default): each backend's structural residency. On the CPU backends f16 computes in f32 (under narrow_compute_f32); on the GPU backends f16 arithmetic is native and reduction accumulators keep storage residency, mirroring the tensor-unit triples every backend seeds at f16 accumulate. The auto resolution is per BACKEND and deliberately retains latitude: on hardware where a wide f16 accumulate costs nothing (datacenter-class NVIDIA runs f32-accumulate f16 mma at full rate) a later refinement may resolve it wide, so do not write code that assumes Fp16_auto equals Fp16_narrow — ask the backend's accum_prec/seeding instead.
  • Fp16_wide (config false): f16 reduction accumulators reside in f32 on every backend, narrowing once per nest — the strict cross-backend-uniform semantics. Backends whose tensor-unit f16 legs cannot accumulate f32 (Backend_intf.mma_capability.mma_f16_wide_acc is false: Metal's simdgroup_matrix is uniform-precision only) have their uniform-f16 mma seeds withheld, per the gh-ocannl-545 seeding-vs-emission discipline — widening only the serial legs would restore the schedule-dependent width gh-ocannl-663 removed.
  • Fp16_narrow (config true): compute fp16 in fp16 on CPU targets that have native 16-bit arithmetic (ARMv8.2-FP16, AVX512-FP16) — gh-ocannl-516's opt-in, trading fp16's 10-bit mantissa and 65504 range for a doubled lane count. On targets that merely promote to float it is ignored (costs accuracy for no speed), and the GPU backends behave as under Fp16_auto (their f16 arithmetic is native narrow already).
val fp16_mode_of_sexp : Sexplib0.Sexp.t -> fp16_mode
val sexp_of_fp16_mode : fp16_mode -> Sexplib0.Sexp.t
val compare_fp16_mode : fp16_mode -> fp16_mode -> Base.int
val equal_fp16_mode : fp16_mode -> fp16_mode -> Base.bool
type t = {
  1. tf32_matmuls : Base.bool;
    (*

    Allow tensor-core matmuls over uniform-f32 operands to compute in tf32 on backends with a tf32 tile shape (CUDA sm_80+): f32's exponent range with a 10-bit mantissa, accumulation in f32. Off by default — opt-in like PyTorch's allow_tf32, because enabling it silently changes numerics. Metal (simdgroup_float8x8 is genuine f32) and HIP (RDNA WMMA has no tf32-like shape) are unaffected.

    *)
  2. narrow_compute_f32 : Base.bool;
    (*

    Run the arithmetic over narrow-float storage (bf16, fp16, fp8) in f32 on backends that have no native narrow arithmetic — the CPU backends, where every narrow operator is an explicit widen/op/narrow round-trip anyway (gh-ocannl-517). Storage stays narrow: reads widen once at the load, the result narrows once at the store, and the intermediates of an assignment keep f32 mantissa instead of being rounded per operator. That is both the faithful reading of "16-bit storage with f32 compute" and what makes the vectorized renderings — which are f32/f64 shaped — reachable for narrow-storage kernels.

    A reduction accumulator is such an intermediate (gh-ocannl-639): every rendering of an accumulation nest — the plain serial fallback included — holds the accumulator at the resolved compute precision across the whole nest and narrows it once at the store, so the effective accumulation width is this policy's, never a property of which schedule happened to place the accumulator in a register. (Narrowing POINTS beyond that single one remain a property of a schedule's reduction structure: a k-blocked schedule stores storage-precision partials at its block boundaries by construction.)

    On by default: it strictly increases accuracy relative to per-operator rounding and is the precondition for narrow storage being a speedup rather than a pessimization on CPU. Turn it off to recover the pre-gh-517 semantics, where every operator rounds to the target node's storage precision.

    The GPU backends' compute precision is unaffected either way — they have native 16-bit types and arithmetic, so pointwise narrow arithmetic computes where it stores. Their reduction-accumulator residency follows the tensor-unit formats (gh-ocannl-663): CUDA's bf16 mma legs hold f32 per-lane registers, so its serial bf16 legs widen to match, and fp8 — which has an accumulator format on no backend — takes f32 residency everywhere; bf16 on HIP/Metal (whose tiles accumulate in storage-width fragments) keeps storage residency so serial and tensorized legs stay width-uniform per backend. f16 residency is fp16_arithmetic's question, not this knob's (gh-ocannl-680). This knob reaches the GPU accumulators only where per-step narrowing can be restored SCHEDULE-UNIFORMLY: fp8 on CUDA and HIP (nothing tensorizes fp8 destinations). CUDA's bf16 residency is structural — the mma accumulate is hardware-f32, so narrowing only the serial legs would resurrect the schedule-dependent width — and so is Metal's fp8 one: MSL has no fp8 type, every fp8 computation there runs in f32 (Metal_backend's compute_prec).

    *)
  3. fp16_arithmetic : fp16_mode;
    (*

    How f16 computes and accumulates, per fp16_mode (gh-ocannl-680). The narrow request is fp16-specific because fp16 is the one narrow format a CPU can execute natively — bf16 has no C type and no general ARM/x86 arithmetic, and stays emulated by design. The asymmetry with narrow_compute_f32 is deliberate: computing in fp16 trades accuracy for throughput, while widening to f32 trades nothing — which is also why Fp16_auto rather than Fp16_narrow is the default, and why the narrow request only takes effect where the target's arithmetic is genuinely 16-bit (Ir.Backend_intf.hardware_limits.native_fp16_arithmetic).

    *)
}
val t_of_sexp : Sexplib0.Sexp.t -> t
val sexp_of_t : t -> Sexplib0.Sexp.t
val compare : t -> t -> Base.int
val equal : t -> t -> Base.bool
val default : unit -> t
val fingerprint : t -> string

A stable, exhaustive rendering of a policy, for cache keys and digests (gh-ocannl-568). Derived from the sexp rather than spelled out field by field, so a knob added to this deliberately open-ended record enters every fingerprint by construction — the failure mode being guarded against is precisely a policy field that a cache key forgot about.

val policy : t Base.option Base.ref
val get : unit -> t

The current policy; reads the global config on first use.

val set_policy : t -> Base.unit

Programmatic override, e.g. per-experiment toggles from training scripts. Call before compilation; routines already compiled keep the numerics they were compiled with.

val fp16_accum_wide : unit -> bool

Whether the current policy is Fp16_wide: f16 reduction accumulators reside in f32 on every backend (gh-ocannl-680). Consulted by every backend's accum_prec and by the mma seeding gate in Sketch_families.mma_tile_for_precisions — one predicate on both sides of the gh-ocannl-545 seam, so seeding and emission cannot drift apart on which f16 sites tensorize.

val cpu_compute_prec : native_fp16_arithmetic:Base.bool -> Ops.prec -> Ops.prec

The compute precision the CPU backends resolve a storage precision to under the current policy: fp16 stays fp16 only where fp16_arithmetic requests it (Fp16_narrow) AND the target's arithmetic is genuinely 16-bit (gh-ocannl-516); every other narrow float computes in f32 under narrow_compute_f32 (gh-ocannl-517); everything else is itself. The single source of truth shared by Cc_backend.compute_prec (emission) and autotune's sketch seeding (the candidate pre-filter and the packed-Stage tile precisions, gh-ocannl-575) — the gh-ocannl-545 lesson: when seeding and emission can disagree about a gate, candidates get timed under labels their rendering does not honor.

val cpu_accum_prec : native_fp16_arithmetic:Base.bool -> Ops.prec -> Ops.prec

The accumulator residency the CPU backends resolve a storage precision to: cpu_compute_prec, except that Fp16_wide's contract — f32 f16-accumulators on every backend, unconditionally — holds even where narrow_compute_f32 = false leaves the f16 compute at storage width (gh-ocannl-680). Like cpu_compute_prec this is the single source of truth shared by Cc_backend.accum_prec (emission) and autotune's sketch seeding: where the two diverge, a C-tile rendering cannot honor the residency and both the emission (C_syntax.try_register_tile) and the seeding pre-filter must decline (Codex P1 round 1 on staging PR #477).