tileinterp

with_gpu_interp, and beside its answer one line per launch in the order they ran: the kernel's name, then ok or the kind of the refusal (interp.unsupported_op, interp.ub, ...). scripts/tileinterp-diff reads these to know which kernels a case actually interpreted.

Run body with every launch interpreted (interp.interp_kernel) at the grid the launch names, the kernel found by name through progs. Every other Gpu operation goes to the handler outside, which is normally std/gpu's with_gpu_fake:

with_gpu_fake(map.empty(), () => with_gpu_interp(name => map.get(progs, name), body))

A refused launch answers Err with the interpreter's kind and message, and a name progs does not know answers gpu.no_kernel.

Whether name is a float format the interpreter models.

Whether name is a float format that exists and is not modelled.

The width of a float format in bits.

The rounding a dialect attribute spells (nearest_even, nearest_away, zero, negative_inf, positive_inf).

x rounded into format fmt in direction mode. The fp8 and fp4 formats take no direction (their ftof allows nearest-even only, and f8E8M0FNU's zero is the one function std/narrow has for it): the direction is ignored there, because tileir refuses a pair that disagrees before a kernel can be recorded.

x rounded into fmt to nearest, ties to even: what every plain operation of the format does to its exact result.

The pattern of x, a value of fmt, in the low float_width(fmt) bits of an Int (never negative, but for binary64's own sign bit).

The value of fmt whose pattern is the low bits of b; a NaN pattern keeps its payload (see nan_bits).

x with the subnormals of fmt replaced by the zero of their sign: the dialect's flush_to_zero. A format with no subnormal range of its own (the fp8 and fp4 ones, which the attribute never applies to) is left.

Why a launch failed: kind is one of interp.unsupported_op (an instruction or format this subset does not model, refused before anything ran), interp.ub (undefined behaviour the kernel reached: an out-of-bounds access, a use of an undefined lane, a false assume, an integer division by zero, a non-saturating ftoi of a value out of range, a broken inbounds promise, a loop past the step limit), interp.bad_launch (the launch does not fit the kernel: buffer or scalar counts, a buffer whose format is not the parameter's) or interp.internal (a defect of this package). message names the instruction.

How many iterations one loop or for may run before the launch is refused as interp.ub: a loop whose exit never comes does not fail on the device, it runs until something kills it.

The bit width of an integer format, or 0 for any other name.

v wrapped into the signed range of w bits (an i1 is 0 or 1).

The first instruction or format of k this subset does not interpret, said as the refusal will say it, or None when every instruction and every format in it is modelled. The interpreter refuses a launch with exactly this message and kind interp.unsupported_op before anything runs, and raises that kind nowhere else.

Run k over the grid grid ([gx], [gx, gy] or [gx, gy, gz], missing axes 1) on the buffers ins of formats dtypes and the by-value arguments scalars, in the conventions of std/gpu's WideRefFn. Blocks run one after another, x fastest. The answer is each buffer a store reached, by its position among the buffers, with its whole contents. ub_checks (default on) refuses undefined behaviour the kernel reaches; off, an undefined lane reads NaN or 0 and the run goes on.

prog as the fake device runs a kernel: std/gpu's WideRefFn, lowered once here and interpreted over grid on every call. with_gpu_fake does not consult a launch's grid, so the grid is fixed when the function is made (with_gpu_interp in the device module reads it from each launch instead). A refused launch panics with <kind>: <message>, kinds as InterpError has them, because a WideRefFn has no error channel.

A rounding direction for the operations that take one.

The positive infinity.

A quiet NaN.

The sign bit of a binary64 pattern.

ln 2 to the nearest Float.

pi to the nearest Float.

The bit pattern of x (binary64), and its inverse.

The binary64 value whose bit pattern is b.

x is a NaN.

x is neither infinite nor a NaN.

The sign bit of x is set (so -0.0 and negative NaNs count).

x is a nonzero subnormal number.

The zero with the sign of x.

x with subnormals replaced by the zero of their sign: the dialect's flush_to_zero, which applies to the inputs and to the result.

The next binary64 value above x (toward +inf). +inf and NaN are their own successor; the successor of -0.0 and of +0.0 is the least positive subnormal.

The next binary64 value below x (toward -inf).

2^k as a Float, for any k binary64 can hold (subnormal results included).

x * 2^k by at most three exact steps, so that a result in the subnormal range is rounded once.

The binary exponent of a finite nonzero x: x = m * 2^e with m in [1, 2).

Dekker's product: (p, e) with p = fl(a * b) and a * b = p + e EXACTLY, provided neither the product nor the splits overflow and the product does not underflow. Callers scale into range first.

Knuth's TwoSum: (s, e) with s = fl(a + b) and a + b = s + e exactly, for finite operands whose sum does not overflow.

The ROUND-TO-ODD value of the exact sum s + e, where s = fl(x + y) and e is the error TwoSum reports: s itself when the sum was exact or its significand is already odd, otherwise the neighbour of s on the side of e, whose significand is odd. Rounding that value to nearest, or in any direction, at a format with at most 51 significand bits gives what rounding the EXACT sum once would (Boldo and Melquiond, "Emulation of FMA and correctly rounded sums: proved algorithms using rounding to odd", IEEE Trans. Computers 2008). It is the one device that lets binary64 stand in for a wider format in the fused operations below.

x + y rounded to odd (see odd_of); x and y finite.

a * b + c with ONE rounding to nearest, for binary64 operands: the fused multiply-add the dialect's fma performs. Boldo and Melquiond's algorithm: the exact product as uh + ul (Dekker), the sum c + uh as th + tl (TwoSum), v = RO(tl + ul), and RN(th + v). It needs the product where Dekker's split cannot overflow and ul cannot underflow (|a| and |b| below 2^500, |c| below 2^1000, |a b| between 2^-900 and 2^900). Outside that range, and for an infinity, a NaN or a zero product, it answers `a b + c`: exact where an operand is special, two roundings in the extreme-range case (docs/tileinterp-design.md 7.3).

The correctly rounded square root of x (ties cannot occur). NaN for a negative or NaN operand, x itself for either zero and for +inf.

x = m * 4^k with m in [1, 4), Newton's iteration for sqrt(m), then the exact test that picks the right neighbour: y is sqrt(m) rounded to nearest iff pred(y) * y < m <= y * succ(y), both products formed exactly by two_prod (the quarter-ulp-squared term that separates the true midpoint square from these products is below the granularity both sides of each comparison share, so it cannot change the answer).

The value r, the round-to-nearest result of an exact operation, moved to the directed result: err is the sign of exact - r (-1, 0 or 1).

a + b rounded in direction dir.

a * b rounded in direction dir.

a / b rounded in direction dir.

floor(x): the largest integer-valued Float not above x.

ceil(x): the smallest integer-valued Float not below x.

The IEEE remainder of truncated division, fmod: a - n * b with n the quotient truncated toward zero, computed exactly by long division on the binary exponents (the result is always representable).

e^x. The argument is divided by 2^10, the Taylor series of the small result summed to fourteen terms, and the answer squared ten times. Each squaring doubles the relative error, so the result is good to about 1024 ulps; that is 2e-13 relative, inside the tolerance tier by eight orders of magnitude.

2^x, exact at integer arguments.

ln x: x = m * 2^e with m in [1, 2), then Halley's iteration for the y with e^y = m, which converges cubically from the two-term guess.

log2 x, exact at powers of two.

1 / sqrt(x).

tanh x as 1 - 2 / (e^(2|x|) + 1) with the sign put back; past 20 the answer is 1 to the last bit. Small arguments lose relative accuracy to the subtraction but keep an absolute error near 1e-16, which is what the tolerance tier measures.

sinh x.

cosh x.

sin x. NaN for an infinite argument.

cos x. NaN for an infinite argument.

tan x.

atan x.

atan2(y, x), the angle of the point (x, y), with C's signed-zero and infinity conventions.

x^y with C's pow special cases: x^0 = 1 and 1^y = 1 for every operand (NaN included), a negative base only to an integer power, zero and infinity by the sign and parity rules.

a * b + c in format fmt, rounded once.

Binary64: Boldo and Melquiond's emulation (math.fma_f64). A narrower format: the product of two operands of at most 24 significand bits is exact in binary64, c is added by rounding to odd, and that value is rounded into fmt; rounding to odd first loses nothing for a format with at most 51 significand bits, so the second step is the only rounding.

acc + a * b for an m by k matrix a, a k by n matrix b and an m by n accumulator, all row major, accumulating into format out. See the header for the order and the roundings.

The block-scaled product of Ops.td's MmaFScaledOp: acc plus the sum over p of (a[i][p] * sa[i][p / v]) * (b[p][j] * sb[p / v][j]), where sa is m by k / v and sb is k / v by n. The scales are powers of two (f8E8M0FNU), so every factor and product is exact in binary64, and the sum is accumulated wide and rounded into f32 once, like the unscaled product into a narrower accumulator.

The integer product of mmai: acc plus the sum of the products of signed i8 operands, wrapped to the i32 accumulator. Integer addition is associative modulo 2^32, so the order is not a model, it is exact.