From 0b6c302ffccb4e7a02e47b5dc376f94040647e9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20L=C3=BCning?= Date: Tue, 20 Oct 2026 14:42:33 +0200 Subject: [PATCH] defk-o08.6: rolling_stats mean_std raises on a bad window, so its loop keeps no bounds check A raising guard 'if w < 1 or w > n' before the loop gives 1 <= w <= n, which proves x[i - w] and both out writes: the module's report lists no kept bounds check (was 3), the flagged strip carries float checks only, and clang's remark no longer cites the array bounds (the sliding sums still keep the loop scalar). A window outside 1..length(x) now raises ArgumentError at the call. non_finite_test's mixed-error strip case moves to an unguarded copy of the kernel; the catalog kernel gets a test of its guard (docs/performance.md 6.42). Closes the last gap of epic defk-o08. --- docs/performance.md | 25 ++++++++++++++- examples/rolling_stats.exs | 12 ++++++-- test/non_finite_test.exs | 63 ++++++++++++++++++++++++++++++++++++-- 3 files changed, 95 insertions(+), 5 deletions(-) diff --git a/docs/performance.md b/docs/performance.md index eb1861c8..0c2c99d2 100644 --- a/docs/performance.md +++ b/docs/performance.md @@ -2633,6 +2633,29 @@ else: 0))`; it now says `if first < 0 and n > 0, do: raise(ArgumentError, without `report: :full`). - **Status:** measured, provisional. +### 6.42 A raising guard on the window drops every bounds check in rolling_stats' loop + +- **Change:** `mean_std` in `rolling_stats.exs` raises `ArgumentError` for a + window outside `1..length(x)`, one guard `if w < 1 or w > n` before the + loop. Past it `1 <= w <= n` (an `or` that is false narrows both sides), + which proves `x[i - w]` under `i >= w`, and `out[i - w + 1]` and + `out[m + i - w + 1]` with `m = n - w + 1 >= 1` and `length(out) == 2 * m`. +- **The C** (fast-path report under `report: :full`): bounds checks kept + 3 -> 0; the loop's flagged strip carried float, overflow and bounds checks + and now carries float checks only (the index arithmetic's overflow checks + went with the bounds facts). clang still does not vectorise the loop: its + remark lost "cannot identify array bounds" but keeps the sliding sums, + a recurrence ("value that could not be identified as reduction is used + outside the loop"), so no speed-up is expected from vector code. Not + timed: the stored row is stale until the maintainer asks for a new + measurement (docs/agents/runs.md). +- **Behaviour:** a window of 0, a negative one or one longer than the input + raises `ArgumentError` at the call instead of failing later in the loop; + the example's check (one valid window) passes. +- **Source:** `defk-o08.6`, [`rolling_stats.exs`](https://github.com/DanielLuning/defk/blob/main/examples/rolling_stats.exs); the + compiler side is `defk-9za` / `defk-b38` (6.34). +- **Status:** C and report checked; not timed. + --- ## 7. When a hand-written or wrapper NIF is still the answer @@ -2940,4 +2963,4 @@ example or close a workload ticket, add its entries and its line here. `defk-sve`, `defk-sve.1` ([`state-copy-cost.md`](https://github.com/DanielLuning/defk/blob/main/docs/research/state-copy-cost.md)), `defk-ulk`, `defk-ulk.1` ([`simd.md`](https://github.com/DanielLuning/defk/blob/main/docs/research/simd.md)), `defk-33b`, `defk-ulk.4`, `defk-52v.15` ([`cdcl_sat.exs`](https://github.com/DanielLuning/defk/blob/main/examples/cdcl_sat.exs)), `defk-tif`, `defk-gqk`, `defk-6ag`, `defk-7dm` ([`bench/port_roundtrip.exs`](https://github.com/DanielLuning/defk/blob/main/bench/port_roundtrip.exs)), `defk-1ub`, - `defk-o08.2`, `defk-o08.3`, `defk-o08.4`, `defk-o08.5`. + `defk-o08.2`, `defk-o08.3`, `defk-o08.4`, `defk-o08.5`, `defk-o08.6`. diff --git a/examples/rolling_stats.exs b/examples/rolling_stats.exs index 880f6c6a..8fe4622c 100644 --- a/examples/rolling_stats.exs +++ b/examples/rolling_stats.exs @@ -10,7 +10,9 @@ # step), so both versions start from the same bytes. # # Both sides return the same thing: one packed binary of the n - w + 1 means -# followed by the n - w + 1 standard deviations (f64, native endian). +# followed by the n - w + 1 standard deviations (f64, native endian). The +# kernel raises ArgumentError for a window outside 1..n: that raising guard +# is what lets the compiler drop every bounds check in its loop. # # Elixir baseline: optimised. Best of 7 runs after a warm-up, 1M samples, # w = 60, 12 schedulers, shared machine (provisional: other benchmarks were @@ -52,9 +54,15 @@ defmodule Rolling.Kernels do use Defk # Sliding sums: O(n) regardless of window size. Returns means then stddevs, - # n - w + 1 values each, packed into one array. + # n - w + 1 values each, packed into one array. A window outside + # 1..length(x) raises ArgumentError. defk mean_std(x :: [f64], w :: i64) :: [f64] do n = length(x) + + # a raising guard: past it 1 <= w <= n, which proves x[i - w] and both + # out writes in range (docs/language.md, "Preconditions: raising guards") + if w < 1 or w > n, do: raise(ArgumentError, "the window must be in 1..length(x)") + m = n - w + 1 out = alloc(f64, 2 * m) diff --git a/test/non_finite_test.exs b/test/non_finite_test.exs index 2a3c2554..d85af8cb 100644 --- a/test/non_finite_test.exs +++ b/test/non_finite_test.exs @@ -261,6 +261,38 @@ defmodule Defk.NonFiniteTest.K do end end +# examples/rolling_stats.exs's mean_std before its raising guard on w: a bad +# window reaches the loop, so a strip mixes a non-finite read with a read +# past the end or a zero divisor +defmodule Defk.NonFiniteTest.Rolling do + use Defk + + defk mean_std(x :: [f64], w :: i64) :: [f64] do + n = length(x) + m = n - w + 1 + out = alloc(f64, 2 * m) + + _ = + for i <- 0..(n - 1)//1, reduce: {0.0, 0.0} do + {s, q} -> + v = x[i] + old = if i >= w, do: x[i - w], else: 0.0 + s2 = s + v - old + q2 = q + v * v - old * old + + if i >= w - 1 do + mean = s2 / w + out[i - w + 1] = mean + out[m + i - w + 1] = sqrt(max(q2 / w - mean * mean, 0.0)) + end + + {s2, q2} + end + + out + end +end + defmodule Defk.NonFiniteTest do use ExUnit.Case, async: true use Defk.Properties @@ -617,7 +649,9 @@ defmodule Defk.NonFiniteTest do end test "rolling mean_std raises its first error: a NaN read before the read past the end" do - rolling = fn x, w -> Defk.Test.assert_agrees(Rolling.Kernels, :mean_std, [x, w]) end + rolling = fn x, w -> + Defk.Test.assert_agrees(Defk.NonFiniteTest.Rolling, :mean_std, [x, w]) + end for n <- [100, 2 * @strip + 3], p <- G.strip_positions(n), p < n - 1 do # w = -1 reads x[i + 1]: past the end at i = n - 1, after the NaN @@ -631,11 +665,36 @@ defmodule Defk.NonFiniteTest do end # the window sums check the reads they add, once per strip (seen_later/1) - c = File.read!(String.replace_suffix(Rolling.Kernels.__defk_lib__(), ".so", ".c")) + c = + File.read!(String.replace_suffix(Defk.NonFiniteTest.Rolling.__defk_lib__(), ".so", ".c")) + assert c =~ "defk_in_f64_later(ctx, " assert c =~ "#define defk_get_f64 DEFK_NF_get_f64" end + test "the catalog's mean_std raises on a bad window before reading, and keeps its strip checks" do + rolling = fn x, w -> Defk.Test.assert_agrees(Rolling.Kernels, :mean_std, [x, w]) end + n = 2 * @strip + 3 + + # its raising guard runs before the loop: no read, no zero divisor + for w <- [-1, 0, n + 1] do + assert {:raise, %ArgumentError{message: "the window must be in 1..length(x)"}} = + rolling.(with_bad(n, 5, 1.0e200), w) + end + + for p <- G.strip_positions(n) do + assert {:raise, %ArgumentError{}} = rolling.(with_bad(n, p, :nan), 3) + end + + assert {:ok, _} = rolling.(with_bad(n, -1, nil), n) + + # past the guard every access is in range; the window sums still check + # the reads they add once per strip + c = File.read!(String.replace_suffix(Rolling.Kernels.__defk_lib__(), ".so", ".c")) + assert c =~ "defk_in_f64_later(ctx, " + refute c =~ "#define defk_get_f64 DEFK_NF_get_f64" + end + test "mixed-error strips run flagged, with no unchecked access to a computed index" do c = File.read!(String.replace_suffix(K.__defk_lib__(), ".so", ".c")) assert c =~ "#define defk_get_in_f64 DEFK_NF_get_in_f64"