Module Sarek_codegen.Sarek_ir_f16_narrowing

Which f32 -> f16 narrowings need sarek_f32_barrier (specs/f16-narrowing-barrier.md).

The DSL narrows in two steps: every f32 operation rounds to binary32, then the narrowing rounds that to binary16. The AMDGPU backend may fuse the operation feeding a narrowing into it (v_fma_mixlo_f16, v_add_f16, ...) and round once; the barrier forbids that. It is unnecessary when one rounding provably equals two:

The analysis is conservative: anything it cannot prove keeps the barrier.

type facts

What is known about the variables and arrays of one function body.

val of_kernel : Sarek_ir_types.kernel -> facts

Facts for a kernel body: its parameters, locals, shared arrays and every binding in its body.

Facts for a helper function body. Its parameters are not opaque (the helper is inlined, so the caller's arithmetic reaches them) and its array reads are never treated as opaque leaves.

val empty : facts

No facts: every variable unknown.

type form =
  1. | Barrier
  2. | Plain
  3. | Signed_product of Sarek_ir_types.expr * Sarek_ir_types.expr

How to emit the narrowing of the f32 expression e:

  • Barrier: through sarek_f32_barrier (nothing proved);
  • Plain: a bare narrowing; one rounding equals two whatever the compiler fuses into it;
  • Signed_product (a, b): e is a * b, exact in f32, but possibly a zero whose sign the fused form gets wrong (a * b + 0 turns -0 into +0). Emitted as a bare narrowing of a * b whose sign bit is then or-ed with sign a xor sign b: the sign of the exact product, which the fused and the unfused result share except on that zero.
val form : facts -> Sarek_ir_types.expr -> form
val needs_barrier : facts -> Sarek_ir_types.expr -> bool

needs_barrier facts e is form facts e = Barrier.

type bound = {
  1. kmax : float;
  2. qlo : int;
  3. qhi : int;
  4. binary16 : bool;
  5. nonzero : bool;
  6. nonneg : bool;
}

The bound the analysis proves for an exact f32 value: the value is k * 2^q with k an integer, |k| <= kmax, qlo <= q <= qhi; binary16 when it is moreover a binary16 value, nonzero when it is never a zero, nonneg when it is never negative and never -0. Exposed for the property test that checks the analysis against a reference evaluation.

val exact : facts -> Sarek_ir_types.expr -> bound option

exact facts e: Some b when every operation in e is exact in f32 (so e's f32 value is its exact real value) and that value satisfies b; None when this cannot be shown.