Skip to content

ADR-013 — Float reduction reassociation policy

  • Identifier: ADR-013
  • Title: Float reduction reassociation policy
  • Status: Accepted
  • Source: extracted verbatim from the Engineering PRD, docs/prd/08-kernel-design.md (REQ-DOC-004). From M0 onward this file is the canonical, living ADR record; status changes happen here and in the index, with the PRD text remaining the historical record.

ADR-013 — Float reduction reassociation policy. Status: Accepted. Context: single-accumulator FP reduction is latency-bound, wasting 6–12× throughput (Survey §3.9); Charter §7.4 requires an explicit reassociation policy, prohibits -ffast-math, and demands per-(version, ISA) determinism. Problem: fix an accumulation order that is fast, deterministic, and specifiable. Alternatives: (1) strict left-fold — rejected: forfeits ILP (Survey §3.9); (2) compiler-chosen (-ffast-math/pragmas) — rejected: nondeterministic across compilers, charter-prohibited; (3) pairwise/tree over whole batch — rejected: needs O(log n) staging or recursion, complicates masking; (4) fixed blocked accumulation (selected): A accumulator registers of the backend's lane width; main loop adds element blocks in order; accumulators combine pairwise (0+2),(1+3),then +; horizontal fold low→high lane; tail (n mod block) folded sequentially into the scalar result afterward, in index order. Accumulator counts (frozen): scalar A=1 — strict sequential left-fold, because the Charter (§7.4) designates the scalar reference as the strict-order recourse; the scalar backend therefore knowingly sacrifices float-sum ILP throughput (Survey §3.9), and this is stated in the K6 doc page and ledger interpretation. NEON/AVX2/AVX-512: A=4 vectors (f32 lanes: 16/32/64; f64: 8/16/32). Note the corollary for baselines: since compilers cannot reassociate FP without fast-math (charter-prohibited), the autovec float-sum baselines are also strict-order — the verdict block for K6 float sums compares explicit-SIMD reassociated variants against a strict baseline and shall say so explicitly. Consequences: explicit backends get better worst-case error than left-fold; the testkit implements the policy generically (parameterized by the per-ISA accumulator layout, with A=1 reproducing the scalar backend exactly) so differential tests have an exact float oracle (12 §2, REQ-TEST-004); changing A or the fold order is a semantic change requiring a version bump. Reconsideration: ledger evidence that A=4 vectors starves a µarch (then bump A via minor version with CHANGELOG semantic note). Related: REQ-K6-003, REQ-API-006.