From 9852a634568237470978c51c9ac84357dfb919c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20L=C3=BCning?= Date: Thu, 22 Oct 2026 11:54:31 +0200 Subject: [PATCH 1/3] defk-w8r.3: rank parameters in declaration order, so a guard between two arguments bounds the later one A gather loop (bench/gather_layer.exs) lists the checks its hot loop keeps. Most of the handwired study's list was already proven away; one was not for a reason of ranking: facts land on a condition's newest atom, and parameters ranked by their C names, so base <= length(x) bounded the length and not base, and base + idx[j] kept its overflow check. The facts scope now carries the parameters' declaration order, and the ranking (newest/2, the product's canonical form) reads it; a scope without one still ranks by name (the unit tests' scopes). The gate shows one module changed, which lost a range-limit test; the guarded gather loop runs about 0.75 ns per term where it was 0.9-1.1; the compiler does +0.5% of its work. Recorded as docs/performance.md 6.45; the rule for users in docs/language.md (raising guards). --- bench/gather_layer.exs | 114 +++++++++++++++++++++++++++++++ docs/adr/0007-symbolic-bounds.md | 8 ++- docs/language.md | 8 +++ docs/performance.md | 80 +++++++++++++++++++++- lib/defk/compiler.ex | 9 ++- lib/defk/facts.ex | 84 +++++++++++++---------- test/condition_facts_test.exs | 62 ++++++++++++++++- test/product_facts_test.exs | 2 +- 8 files changed, 323 insertions(+), 44 deletions(-) create mode 100644 bench/gather_layer.exs diff --git a/bench/gather_layer.exs b/bench/gather_layer.exs new file mode 100644 index 00000000..41f452ba --- /dev/null +++ b/bench/gather_layer.exs @@ -0,0 +1,114 @@ +# A gather loop: which runtime checks stay in its hot loop, and what each +# costs. A sparse layer over an [f32] weight array, with the input index of +# each term in an [i32] array: output r is the sum over t < k of +# w[r * k + t] * x[base + idx[r * k + t]]. The fast-path report lists every +# check the compiler kept in the loop and the fact that would drop it; +# the timing gives the cost per output row. docs/performance.md 6.45. +# +# mix run bench/gather_layer.exs [rounds] +# +# Each number is the best over the rounds of the us per output row over +# one call (n rows of k terms); other processes' CPU is printed before +# each block (Defk.Bench.other_cpu/0): at most one core counts as quiet. +rounds = String.to_integer(List.first(System.argv()) || "9") + +defmodule Gather.Kernels do + use Defk, report: :full + + # the shape from the arrays: n rows of k terms in w, one index per term + defk layer(w :: [f32], idx :: [i32], x :: [f32], k :: i64, base :: i64) :: [f32] do + n = div(length(w), k) + out = alloc(f32, n) + + for r <- 0..(n - 1)//1 do + out[r] = + for t <- 0..(k - 1)//1, reduce: 0.0 do + acc -> acc + w[r * k + t] * x[base + idx[r * k + t]] + end + end + + out + end + + # the same with the shape and the base stated by raising guards + defk layer_guarded(w :: [f32], idx :: [i32], x :: [f32], k :: i64, base :: i64) :: [f32] do + if not (k > 0 and length(idx) == length(w) and base >= 0 and base <= length(x)), + do: raise(ArgumentError, "shape") + + n = div(length(w), k) + out = alloc(f32, n) + + for r <- 0..(n - 1)//1 do + out[r] = + for t <- 0..(k - 1)//1, reduce: 0.0 do + acc -> acc + w[r * k + t] * x[base + idx[r * k + t]] + end + end + + out + end + + # the NFA study's one fact: a product of two band(_, 1) values is 0 or 1 + defk bit_product(a :: [i64], b :: [i64]) :: i64 do + n = min(length(a), length(b)) + + for i <- 0..(n - 1)//1, reduce: 0 do + acc -> + hit = band(a[i], 1) + ext = band(b[i], 1) + acc + hit * (1 - ext) + end + end +end + +defmodule Gather.Elixir do + # the same sum in Elixir, as the agreement reference + def layer(w, idx, x, k, base) do + n = div(byte_size(w), 4 * k) + + for r <- 0..(n - 1), into: <<>> do + acc = + Enum.reduce(0..(k - 1), 0.0, fn t, acc -> + j = r * k + t + <> = binary_part(w, 4 * j, 4) + <> = binary_part(idx, 4 * j, 4) + <> = binary_part(x, 4 * (base + iv), 4) + acc + wv * xv + end) + + <> + end + end +end + +:rand.seed(:exsss, {4, 5, 6}) +n = 4096 +k = 16 +m = 1024 +base = 512 +w = for _ <- 1..(n * k), into: <<>>, do: <<:rand.uniform() * 2 - 1::float-32-native>> +idx = for _ <- 1..(n * k), into: <<>>, do: <<:rand.uniform(m) - 1::signed-32-native>> +x = for _ <- 1..(m + base), into: <<>>, do: <<:rand.uniform() * 2 - 1::float-32-native>> + +ref = Gather.Elixir.layer(w, idx, x, k, base) +^ref = Gather.Kernels.layer(w, idx, x, k, base) +^ref = Gather.Kernels.layer_guarded(w, idx, x, k, base) + +Defk.Report.print(Gather.Kernels) + +best = fn f -> + Enum.min(for _ <- 1..rounds, do: elem(:timer.tc(f), 0)) / n +end + +IO.puts( + "\n#{n} rows x #{k} terms, best of #{rounds} (other CPU: #{Float.round(Defk.Bench.other_cpu() * 1.0, 2)} cores)" +) + +for {name, f} <- [ + {"layer", fn -> Gather.Kernels.layer(w, idx, x, k, base) end}, + {"layer_guarded", fn -> Gather.Kernels.layer_guarded(w, idx, x, k, base) end} + ] do + IO.puts( + " #{String.pad_trailing(name, 16)} #{:erlang.float_to_binary(best.(f), decimals: 3)} us per row" + ) +end diff --git a/docs/adr/0007-symbolic-bounds.md b/docs/adr/0007-symbolic-bounds.md index 92e87adf..884b157d 100644 --- a/docs/adr/0007-symbolic-bounds.md +++ b/docs/adr/0007-symbolic-bounds.md @@ -26,7 +26,9 @@ Replace the fact model with one representation: - **Atoms** are the C variables of i64 bindings and the lengths of array bindings, ranked by binding order (`fresh/2`'s counter; parameters - first). + first, in declaration order, carried in the facts scope since + `defk-w8r.3`: before that they ranked by name, so a guard between two + parameters could land on the wrong one). - **Facts** are `q * x <= P` and `q * x >= P` for an atom or a product of two atoms `x`, with `q >= 1` and `P` a polynomial of degree at most 2 over atoms ranked below `x`, plus the constant `lo`/`hi` kept as they are. @@ -90,7 +92,9 @@ Replace the fact model with one representation: past the ceiling. Each statement's reads walked once (`defk-o08.4`, 6.40) took 8.6% more off: +7.4% of the work before step 1 (-1.0% without `SatEx.Kernels`), under the ceiling again. The report's hint search only - under `report: :full` (`defk-o08.5`, 6.41): +3.5% (-2.2%). + under `report: :full` (`defk-o08.5`, 6.41): +3.5% (-2.2%). Parameters + ranked in declaration order instead of by name (`defk-w8r.3`, 6.45): + +0.5% (+0.3%); the chain at about +4.0% (-1.9%). - **Raising guards become the way to state facts about arguments** in a kernel, which the language docs would describe. - **Out of scope:** degree 3 and nested products, facts across loop diff --git a/docs/language.md b/docs/language.md index d4487cb2..a2791886 100644 --- a/docs/language.md +++ b/docs/language.md @@ -2171,6 +2171,14 @@ that does not raise says, by the rules for [conditions](#reading): `if n != len, do: raise(...)` gives `n == len`; `if a and b, do: raise(...)` gives nothing, as `not a or not b` names no single fact. +A condition between two arguments bounds the one declared later by the +earlier one. In `defk gather(idx :: [i32], x :: [f32], base :: i64)`, the +guard `if base < 0 or base > length(x), do: raise(...)` bounds `base`, so +`base + idx[i]` needs no overflow check (an `[i32]` element is within +32 bits). Declared as `(base :: i64, x :: [f32])`, the same guard bounds +the length of `x` by `base` instead, which proves nothing about `base`: +declare an offset after the array it is compared with. + ### Blocks Every block that needs a value ends in an expression; an empty block is diff --git a/docs/performance.md b/docs/performance.md index 647d7f51..ef9a4c2c 100644 --- a/docs/performance.md +++ b/docs/performance.md @@ -2956,6 +2956,83 @@ s[0] = a * b # the write rounds to float32 (raises if the value does not p = s[0] # read back the rounded value as f64 ``` +### 6.45 Gather loops: a guard now bounds the parameter declared later, which drops the offset's overflow check; the rest of the checks are about contents + +A sparse layer gathers an input per term: `out[r] = sum of w[r * k + t] * +x[base + idx[r * k + t]]` over an `[f32]` weight array, `[i32]` indices +and an `[f32]` input (`bench/gather_layer.exs`, `layer/5`; the guarded +twin states `k > 0`, `length(idx) == length(w)` and `0 <= base <= +length(x)` as a raising guard). The handwired study (6.44's prototype, +deleted; its numbers are the reference point only) had its layer at 0.378 +us per item against 0.069 us for the hand-written C float loop, and listed +the checks in each term. Read again on today's compiler, most of that list +was already gone, one proof was missing for a reason of ranking, and what +stays is about array contents. + +- **The checks in the hot loop, per term** (the fast-path report, `use + Defk, report: :full`; the guarded kernel unless said otherwise): + + | check | before | after | why | + |---|---|---|---| + | `r * k`, `r * k + t`: overflow | dropped | dropped | the loop bounds and the product rule (6.37) | + | `w[r * k + t]`: bounds | dropped | dropped | `n = div(length(w), k)` (6.37) | + | `idx[r * k + t]`: bounds | dropped with the guard (kept without: "it would follow from k * n <= length(idx)") | the same | `length(idx) == length(w)` | + | `base + idx[...]`: overflow | **kept**, with or without the guard | **dropped** with the guard | the guard's `base <= length(x)` now bounds `base`; an `[i32]` element is within 32 bits | + | `x[base + idx[...]]`: bounds | kept | kept | depends on `idx`'s contents; ADR-0007 states no facts about contents | + | `w[...]`, `x[...]`: finite read (`defk_in_f64`) | kept | kept | an input `[f32]` may hold inf or NaN bits | + | `w * x`, `acc + ...`: non-finite result | kept | kept | float values have no facts | + | `out[r] = acc`: f32 range (`defk_to_f32`), once per row | kept | kept | the same | + | `n - 1`, `k - 1`: overflow (loop headers, once) | dropped with the guard | the same | `k > 0`, `n = div(...)` | + + The NFA study's one fact, a product of two `band(_, 1)` values: `hit * + (1 - ext)` had no overflow check before this change either (`band`'s + facts give 0..1, the product rule multiplies the ranges); the + accumulator's add keeps its check (facts across iterations are out of + ADR-0007's scope). The inner loop runs flagged in both kernels: every + kept check sets a flag tested once per strip (6.5), so each costs an + operation and an or, not a branch, and clang reports the loop as not + vectorised for its in-order float reduction, not for a check. +- **What blocked the one proof.** Facts are stated on the newest atom of a + condition, and parameters ranked by their C names (`p_base` before + `p_x`), so `base <= length(x)` was stored as a lower bound on `length(x)` + and said nothing about `base`. Parameters now rank in declaration order + (the design's "parameters first, by position"), carried in the facts + scope, so the guard bounds `base` and `base + idx[j]` is within + `length(x) + 2^31`. The rule to know: a condition between two arguments + bounds the one declared later, so declare an offset after the array it + is compared with (docs/language.md, raising guards). +- **The gate** (`mix dump_c` on both sides, 113 modules): one module's C + changed, `Defk.ProductFactsTest.K`, which lost one range-limit test on a + loop bound (`dim`, now bounded by its guard); no kernel gained a check. + The catalog's bounds (3,301) and overflow (6,050) call sites are + unchanged: no example kernel has a guard between two parameters in the + wrong name order. The report's hint for a product now names the factors + in declaration order (`n * dim <= length(m)`, was `dim * n`). +- **Run time** (`bench/gather_layer.exs`, 4,096 rows of 16 terms, best of + 9, us per row, two interleaved runs a side): the unguarded kernel, whose C + did not change, 0.018 / 0.018 on `main` (one first run 0.023) and 0.018 + / 0.018 on the branch; the guarded kernel 0.018 / 0.014 on `main` and + 0.012 / 0.012 on the branch, about 0.75 ns per term where it was + 0.9-1.1. So the one dropped check is worth 15-30% of this loop, and the + loop is now 1.5x the unguarded one. Against the prototype's 0.378 us + per item (a different kernel on a loaded machine) nothing is comparable; + the hand-written C of that study is gone with it. +- **Compiler time** (two interleaved `mix dump_c` rounds a side, + `dev/compile_time.exs`): +0.5% of + the compiler's work (reductions; +0.3% without `SatEx.Kernels`, which + dominates the prover's cost), +0.8% of its time (-0.3% without), with + `SatEx.Kernels` +0.29M reductions. The chain of ADR-0007 is at about + +4.0% of the work before step 1 (-1.9% without `SatEx.Kernels`), under + its ceiling. +- **Conditions:** M-series Mac, on battery; other processes at 0.1-0.7 cores before + each timed run (the ps quiet test); the compiler-time rounds on the same + machine, one job at a time. +- **Source:** `defk-w8r.3`, [`bench/gather_layer.exs`](https://github.com/DanielLuning/defk/blob/main/bench/gather_layer.exs); the proof's + tests: `test/condition_facts_test.exs` ("a guard between two + parameters": the gather with both name orders, the extremes of the + dropped check, and the agreement properties). +- **Status:** measured. + --- ## 7. When a hand-written or wrapper NIF is still the answer @@ -3300,4 +3377,5 @@ example or close a workload ticket, add its entries and its line here. `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.6`, `defk-w8r.2`, `defk-25s` ([`bench/call_cost.exs`](https://github.com/DanielLuning/defk/blob/main/bench/call_cost.exs)), - `defk-vcx.2` ([`bench/elixir_mode.exs`](https://github.com/DanielLuning/defk/blob/main/bench/elixir_mode.exs)). + `defk-vcx.2` ([`bench/elixir_mode.exs`](https://github.com/DanielLuning/defk/blob/main/bench/elixir_mode.exs)), + `defk-w8r.3` ([`bench/gather_layer.exs`](https://github.com/DanielLuning/defk/blob/main/bench/gather_layer.exs)). diff --git a/lib/defk/compiler.ex b/lib/defk/compiler.ex index 42dd683b..138dee5e 100644 --- a/lib/defk/compiler.ex +++ b/lib/defk/compiler.ex @@ -718,9 +718,12 @@ defmodule Defk.Compiler do {p, Map.merge(val(c, t, c), array_ids(t))} end) + # the parameters rank in declaration order (Defk.Facts, the scope) + scope = Facts.scope(for {p, _} <- k.params, do: vars[p].c) + env = %{ vars: vars, - facts: Enum.reduce(vars, Facts.scope(), fn {_, b}, s -> Facts.bind(s, b) end), + facts: Enum.reduce(vars, scope, fn {_, b}, s -> Facts.bind(s, b) end), sigs: sigs, inlining: [{k.name, k.arity}], ret: k.ret, @@ -2294,7 +2297,7 @@ defmodule Defk.Compiler do case op do :+ -> {"add", Facts.add_facts(va, vb), Facts.add_range(va, vb)} :- -> {"sub", Facts.sub_facts(va, vb), Facts.sub_range(va, vb)} - :* -> {"mul", Facts.mul_facts(va, vb), Facts.mul_range(va, vb)} + :* -> {"mul", Facts.mul_facts(va, vb, env.facts), Facts.mul_range(va, vb)} end v = Facts.put(val(nil, :i64), facts) @@ -6358,7 +6361,7 @@ defmodule Defk.Compiler do nil map_size(d.t) == 1 -> - case Facts.narrowing(d) do + case Facts.narrowing(d, env.facts) do {x, :lo, b} -> "#{names[x]} >= #{b}" {x, :hi, b} -> "#{names[x]} <= #{b}" end diff --git a/lib/defk/facts.ex b/lib/defk/facts.ex index fe4b80d8..8d9136dc 100644 --- a/lib/defk/facts.ex +++ b/lib/defk/facts.ex @@ -111,9 +111,17 @@ defmodule Defk.Facts do # {:len, c}). The compiler's env carries it and it is lexical like the # env; a binding's value keeps the same facts as its entry. An entry # outlives a shadowing binding, as the C variable is assigned once where - # it is in scope. + # it is in scope. The scope also holds the kernel's parameter order under + # @order (the C names in declaration order, each with its position), + # which ranks the parameter atoms (rank/2): a condition between two + # parameters then states its fact on the later one, as it does for two + # bindings. A scope made with no parameters ranks them by name. - def scope, do: %{} + @order :order + + def scope(params \\ []), do: %{@order => Map.new(Enum.with_index(params))} + + defp order(scope), do: Map.get(scope, @order, %{}) # the scope with binding v's facts def bind(scope, %{t: :i64, c: c} = v), do: Map.put(scope, c, facts(v)) @@ -129,7 +137,7 @@ defmodule Defk.Facts do rel |> holds(true?) |> Enum.reduce(scope, fn d, scope -> - {x, kind, b} = narrowing(d) + {x, kind, b} = narrowing(d, scope) c = binding_of(x) Map.put(scope, c, with_fact(facts_of(scope, c), x, kind, b)) end) @@ -310,11 +318,11 @@ defmodule Defk.Facts do defp negated_op(op), do: %{<: :>=, <=: :>, >: :<=, >=: :<, ==: :!=, ===: :!==, !=: :==, !==: :===}[op] - # D <= 0 as a fact on D's newest monomial x, over older ones only: - # {x, :lo | :hi, constant} when the rest of D is a constant, else - # {x, :lb | :ub, {q, form}} - def narrowing(%{t: t} = d) when map_size(t) > 0 do - {x, c} = newest(t) + # D <= 0 as a fact on D's newest monomial x (by the scope's ranking), over + # older ones only: {x, :lo | :hi, constant} when the rest of D is a + # constant, else {x, :lb | :ub, {q, form}} + def narrowing(%{t: t} = d, scope) when map_size(t) > 0 do + {x, c} = newest(t, order(scope)) rest = %{d | t: Map.delete(t, x)} const? = map_size(rest.t) == 0 @@ -480,7 +488,7 @@ defmodule Defk.Facts do do: form, else: best - {x, c} = newest(form.t) + {x, c} = newest(form.t, lookup.(:order)) rest = %{form | t: Map.delete(form.t, x)} {lo, hi, lbs, ubs, fx} = mono(x, lookup) stated = if state == :tainted, do: :tainted, else: :ok @@ -509,8 +517,10 @@ defmodule Defk.Facts do # An atom's facts: array a's own (the one a proof is about), else its # binding's in scope, else none. A binding's exact form is never its own # atom (bound/1 records the value's), so it is a bound over older atoms. + # Asked :order, it gives the scope's parameter order (rank/2). defp lookup(scope, a) do fn + :order -> order(scope) {:len, c} when a != nil and c == a.c -> facts(a) {_, c} -> facts_of(scope, c) end @@ -560,7 +570,7 @@ defmodule Defk.Facts do defp le?(_form, _lookup, 0, _support), do: {false, 0} defp le?(form, lookup, budget, support) do - {x, c} = newest(form.t) + {x, c} = newest(form.t, lookup.(:order)) rest = %{form | t: Map.delete(form.t, x)} {lo, hi, lbs, ubs, _} = mono(x, lookup) @@ -605,7 +615,7 @@ defmodule Defk.Facts do # a monomial's constant range and relative bounds, and an atom's facts: # {lo, hi, lbs, ubs, facts or nil} - defp mono({:mul, y, z}, lookup), do: product(y, z, lookup.(y), lookup.(z)) + defp mono({:mul, y, z}, lookup), do: product(y, z, lookup.(y), lookup.(z), lookup.(:order)) defp mono({:len, _} = x, lookup) do f = lookup.(x) @@ -625,7 +635,7 @@ defmodule Defk.Facts do # product), y's stated constant bounds among them. A bound of y of degree # 2 would give degree 3 and is left out. The product's constant range is # the factors' multiplied. - defp product(y, z, fy, fz) do + defp product(y, z, fy, fz, order) do {zlo, zhi} = zr = monomial_range(z, fz) yr = monomial_range(y, fy) {ylbs, yubs} = monomial_bounds(y, fy) @@ -635,8 +645,8 @@ defmodule Defk.Facts do {lbs, ubs} = cond do - zlo >= 0 -> {times(lows, z), times(highs, z)} - zhi <= 0 -> {times(highs, z), times(lows, z)} + zlo >= 0 -> {times(lows, z, order), times(highs, z, order)} + zhi <= 0 -> {times(highs, z, order), times(lows, z, order)} true -> {[], []} end @@ -653,8 +663,8 @@ defmodule Defk.Facts do defp const_bound(k), do: [{1, form_const(k)}] # bounds {q, p} on y as bounds on y * z (the caller picks the direction) - defp times(bounds, z), - do: for({q, p} <- bounds, degree(p) <= 1, do: {q, form_mul(p, form_mono(z))}) + defp times(bounds, z, order), + do: for({q, p} <- bounds, degree(p) <= 1, do: {q, form_mul(p, form_mono(z), order)}) # a monomial's constant bounds: a length is always in 0..2^61 - 1, an i64 # in -2^63..2^63 - 1 @@ -674,21 +684,21 @@ defmodule Defk.Facts do defp support_of({:mul, {_, a}, {_, b}}, support), do: [a, b | support] defp support_of({_, c}, support), do: [c | support] - # the newest monomial is replaced first: parameters are the oldest, then - # the bindings in fresh/2's order (their C names carry its counter); a - # product ranks with its newer factor, before that factor alone, then by - # its older factor + # the newest monomial is replaced first: parameters are the oldest, in + # declaration order (`order`, the scope's; by name in a scope that holds + # none), then the bindings in fresh/2's order (their C names carry its + # counter); a product ranks with its newer factor, before that factor + # alone, then by its older factor # the newest monomial of a form's terms and its coefficient (one term # needs no ranking) - defp newest(t) when map_size(t) == 1, do: hd(Map.to_list(t)) - defp newest(t), do: Enum.max_by(t, fn {m, _} -> rank(m) end) + defp newest(t, _order) when map_size(t) == 1, do: hd(Map.to_list(t)) + defp newest(t, order), do: Enum.max_by(t, fn {m, _} -> rank(m, order) end) - defp rank({:mul, x, y}), do: {atom_rank(x), 1, atom_rank(y)} - defp rank({_, "p_" <> _ = c}), do: {{0, c}, 0, 0} - defp rank({_, c}), do: {counter(c, byte_size(c), 0, 1), 0, 0} + defp rank({:mul, x, y}, order), do: {atom_rank(x, order), 1, atom_rank(y, order)} + defp rank(a, order), do: {atom_rank(a, order), 0, 0} - defp atom_rank({_, "p_" <> _ = c}), do: {0, c} - defp atom_rank({_, c}), do: counter(c, byte_size(c), 0, 1) + defp atom_rank({_, "p_" <> _ = c}, order), do: {0, Map.get(order, c, c)} + defp atom_rank({_, c}, _order), do: counter(c, byte_size(c), 0, 1) # the number after the last "_" of c, read from the end: {1, n}, or # {0, c} for a name without one @@ -878,8 +888,8 @@ defmodule Defk.Facts do # a product: lo..hi from the operands' (nil when one is unbounded), and # for a constant k >= 1 times v, v's facts scaled by k; the exact form is # the operands' multiplied while it stays of degree 2 (`r * dim`, - # `(n - 1) * m`), none beyond - def mul_facts(a, b) do + # `(n - 1) * m`), none beyond; the scope ranks the product's factors + def mul_facts(a, b, scope \\ %{}) do {fa, fb} = {facts(a), facts(b)} f = @@ -899,7 +909,7 @@ defmodule Defk.Facts do case {const(a), const(b)} do {k, _} when is_integer(k) -> (e = eq(b)) && form_scale(e, k) {_, k} when is_integer(k) -> (e = eq(a)) && form_scale(e, k) - _ -> both(eq(a), eq(b), &form_mul/2) + _ -> both(eq(a), eq(b), &form_mul(&1, &2, order(scope))) end %{f | eq: eq} @@ -1113,15 +1123,16 @@ defmodule Defk.Facts do end) end - # the product of two forms, or nil when it would be of degree 3 or more - def form_mul(%{t: ta} = a, b) when map_size(ta) == 0, do: form_scale(b, a.k) - def form_mul(a, %{t: tb} = b) when map_size(tb) == 0, do: form_scale(a, b.k) + # the product of two forms, or nil when it would be of degree 3 or more; + # `order` ranks the factors of each product monomial + def form_mul(%{t: ta} = a, b, _order) when map_size(ta) == 0, do: form_scale(b, a.k) + def form_mul(a, %{t: tb} = b, _order) when map_size(tb) == 0, do: form_scale(a, b.k) - def form_mul(a, b) do + def form_mul(a, b, order) do if degree(a) + degree(b) <= 2 do cross = for {x, cx} <- a.t, {y, cy} <- b.t, reduce: form_const(0) do - acc -> form_add(acc, %{k: 0, t: %{mul_mono(x, y) => cx * cy}}) + acc -> form_add(acc, %{k: 0, t: %{mul_mono(x, y, order) => cx * cy}}) end form_add(form_scale(%{a | k: 0}, b.k), form_scale(%{b | k: 0}, a.k)) @@ -1131,7 +1142,8 @@ defmodule Defk.Facts do end # the product of two atoms, its newer factor first - defp mul_mono(x, y), do: if(atom_rank(x) >= atom_rank(y), do: {:mul, x, y}, else: {:mul, y, x}) + defp mul_mono(x, y, order), + do: if(atom_rank(x, order) >= atom_rank(y, order), do: {:mul, x, y}, else: {:mul, y, x}) def form_scale(form, 1), do: form def form_scale(_form, 0), do: form_const(0) diff --git a/test/condition_facts_test.exs b/test/condition_facts_test.exs index a2fb6a79..5532438f 100644 --- a/test/condition_facts_test.exs +++ b/test/condition_facts_test.exs @@ -138,6 +138,30 @@ defmodule Defk.ConditionFactsTest.K do acc -> if i + k >= 0 and i + k < length(x), do: acc + x[i + k], else: acc end end + + # A guard between two parameters states its fact on the one declared + # later, whatever their names: base <= length(x) bounds base (declared + # after x), so base + idx[i], an i32 element, fits i64 with no check. The + # gather x[base + idx[i]] keeps its bounds check: it depends on the + # array's contents. + defk gather(idx :: [i32], x :: [f32], base :: i64) :: f64 do + if not (base >= 0 and base <= length(x)), do: raise(ArgumentError, "base") + + for i <- 0..(length(idx) - 1)//1, reduce: 0.0 do + acc -> acc + x[base + idx[i]] + end + end + + # the same with the offset's name sorting after the array's: the same + # proof (a guard bounds the parameter declared later, never the earlier + # one: declared before the array, `off` would keep its check) + defk gather_named(ia :: [i32], as :: [f32], off :: i64) :: f64 do + if not (off >= 0 and off <= length(as)), do: raise(ArgumentError, "off") + + for i <- 0..(length(ia) - 1)//1, reduce: 0.0 do + acc -> acc + as[off + ia[i]] + end + end end # the same unguarded kernel without report: :full: its note names no fact @@ -183,6 +207,7 @@ defmodule Defk.ConditionFactsTest do defp kept(kernel), do: kept_bounds(K, kernel) defp f64s(xs), do: G.pack(:f64, Enum.map(xs, &(&1 * 1.0))) + defp f32s(xs), do: G.pack(:f32, Enum.map(xs, &(&1 * 1.0))) describe "a raising guard and an if arm: a rolling window" do test "x[i - w] keeps no bounds check after a raise when w < 1" do @@ -315,6 +340,39 @@ defmodule Defk.ConditionFactsTest do end end + describe "a guard between two parameters" do + @i32_max 0x7FFFFFFF + @i32_min -0x80000000 + + # the parameters rank in declaration order, so the guard's fact lands on + # the later one whichever name sorts first + for {kernel, sum} <- [{:gather, "base + idx[i]"}, {:gather_named, "off + ia[i]"}] do + test "#{kernel}: the offset plus an i32 element needs no overflow check" do + assert {:dropped, "#{unquote(sum)}: no overflow check"} in notes(unquote(kernel), :check) + # the gather itself depends on the indices: its check stays + assert [text] = kept(unquote(kernel)) + assert text =~ "bounds check kept; nothing proves 0 <= #{unquote(sum)}" + + x = f32s(Enum.to_list(1..8)) + + for idx <- [[], [0], [7, 0, 3], [-1], [8]], base <- [0, 1, 8] do + assert {_, _} = agrees(unquote(kernel), [G.pack(:i32, idx), x, base]) + end + + # the extremes of the dropped check: the sum fits, the access raises + for idx <- [@i32_max, @i32_min], base <- [0, 8] do + assert {:raise, %Enum.OutOfBoundsError{}} = + agrees(unquote(kernel), [G.pack(:i32, [idx]), x, base]) + end + + for base <- [-1, 9, @i64_min, @i64_max] do + assert {:raise, %ArgumentError{}} = + agrees(unquote(kernel), [G.pack(:i32, [0]), x, base]) + end + end + end + end + describe "flagged strips" do test "a guard on a value the strip computes with a check makes no access fixed" do c = kernel_c(K, "guarded_shift") @@ -359,7 +417,9 @@ defmodule Defk.ConditionFactsTest do shift_add: [args: StreamData.fixed_list([G.array(:i64), G.array(:i64), G.i64(-3..20)])], shift_add_unguarded: [ args: StreamData.fixed_list([G.array(:i64), G.array(:i64), G.i64(-3..20)]) - ] + ], + gather: [args: StreamData.fixed_list([G.array(:i32), G.array(:f32), G.i64(-3..20)])], + gather_named: [args: StreamData.fixed_list([G.array(:i32), G.array(:f32), G.i64(-3..20)])] ]) # ------------------------------------------------------ soundness -- diff --git a/test/product_facts_test.exs b/test/product_facts_test.exs index cb22b504..3b7db531 100644 --- a/test/product_facts_test.exs +++ b/test/product_facts_test.exs @@ -207,7 +207,7 @@ defmodule Defk.ProductFactsTest do test "without the shape, the report names the product's bound" do assert kept(:unshaped) == [ "m[r * dim + j]: bounds check kept; nothing proves r * dim + j < length(m) " <> - "(it would follow from dim * n <= length(m))" + "(it would follow from n * dim <= length(m))" ] end end From 350542e93846316425f714850efa5147076fa3c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20L=C3=BCning?= Date: Thu, 22 Oct 2026 12:32:37 +0200 Subject: [PATCH 2/3] defk-w8l: one countdown for the safepoint budget instead of two counters The yield bookkeeping of a kernel kept two values live, the tick count and the budget; a safepoint now counts one value down from the budget and tests it against zero, and the budget lives in the clock, where defk_tick keeps it anyway. Same semantics (ticks >= budget is budget - ticks <= 0; a resume restores the saved budget). Measured (docs/performance.md 6.46): fuzzy_search's per-word gap to its yield: false twin falls from +30% to +16%; Keccak's round loop is unchanged (12 spills per round, 1.3x), and the entry shows why: 8 of its 12 spills are the safepoint's saves and 3 the resume dispatch, none the counters. Two other variants (charge a plain short loop on entry; no bookkeeping register at all) gained nothing and are recorded. bench/keccak_yield.exs counts the spills and times 16 MB; the tick gap and the test suite are unchanged. --- bench/keccak_yield.exs | 115 +++++++++++++++++++++++++++++++++++++++++ docs/performance.md | 97 ++++++++++++++++++++++++++++++++-- lib/defk/compiler.ex | 6 +-- priv/defk_runtime.h | 2 +- 4 files changed, 213 insertions(+), 7 deletions(-) create mode 100644 bench/keccak_yield.exs diff --git a/bench/keccak_yield.exs b/bench/keccak_yield.exs new file mode 100644 index 00000000..dea9b22e --- /dev/null +++ b/bench/keccak_yield.exs @@ -0,0 +1,115 @@ +# Yield bookkeeping in a hot short loop: the Keccak round loop (24 trips, no +# safepoint inside) in the yielding kernel against the same kernel with +# yield: false. Two signals: the stack spills in the hottest loop of the +# compiled C (cc -S with the build's flags; the basic block with the most +# `ror` instructions; loads and stores against [sp]), which do not depend +# on load, and the time for one 16 MB message, interleaved. The kernels +# are examples/keccak.exs' own, read from the file and compiled twice. +# docs/performance.md 6.8 and 6.46. +# +# mix run bench/keccak_yield.exs [rounds] +rounds = String.to_integer(List.first(System.argv()) || "7") + +src = File.read!("examples/keccak.exs") +{c0, _} = :binary.match(src, "defmodule Keccak.Constants") +{k0, _} = :binary.match(src, "kernels =\n quote do") +{k1, _} = :binary.match(src, "\nModule.create(Keccak.Kernels") +constants = binary_part(src, c0, k0 - c0) +kernels = binary_part(src, k0, k1 - k0) +# every kernel head gets yield: false in the blocking twin +blocking = Regex.replace(~r/(defk \w+\(.*\) :: \S+) do$/m, kernels, "\\1, yield: false do") + +{yielding_ast, _} = Code.eval_string(constants <> "\n" <> kernels) +{blocking_ast, _} = Code.eval_string(blocking) + +Module.create(KY.Yield, yielding_ast, Macro.Env.location(__ENV__)) +Module.create(KY.Blocking, blocking_ast, Macro.Env.location(__ENV__)) + +defmodule KY.Spills do + # The stack loads and stores in the hottest loop of a module's C: the + # basic block of the assembly with the most `ror` instructions. + def count(mod, name) do + dir = Path.join("tmp", "keccak_yield") + File.mkdir_p!(dir) + c = Path.join(dir, name <> ".c") + s = Path.join(dir, name <> ".s") + File.write!(c, mod.__defk_c_source__()) + + flags = + ~w(-O3 -ffp-contract=off -std=gnu11 -fPIC -Wall -Wno-unused-label -Wno-unused-variable -fstack-protector-strong -D_FORTIFY_SOURCE=2 -fno-strict-overflow -fno-builtin) + + {_, 0} = + System.cmd( + "cc", + ["-S"] ++ flags ++ ["-I", Defk.Build.erts_include(), "-I", "priv", "-o", s, c], + stderr_to_stdout: true + ) + + blocks = + s + |> File.read!() + |> String.split("\n") + |> Enum.chunk_while( + [], + fn line, acc -> + if Regex.match?(~r/^\S+:/, line), + do: {:cont, Enum.reverse(acc), [line]}, + else: {:cont, [line | acc]} + end, + fn acc -> {:cont, Enum.reverse(acc), []} end + ) + + {block, rors} = + blocks + |> Enum.map(&{&1, Enum.count(&1, fn l -> l =~ ~r/^\s+ror/ end)}) + |> Enum.max_by(&elem(&1, 1)) + + # the loop body ends at its back-edge; what follows in the same block + # (no label) is the exit path, run once per enclosing iteration + block = Enum.take_while(block, &(not (&1 =~ ~r/^\s+b\.\w+/))) ++ ["b."] + + stores = Enum.count(block, &(&1 =~ ~r/^\s+st[pr]\b.*\[sp/)) + loads = Enum.count(block, &(&1 =~ ~r/^\s+ld[pr]\b.*\[sp/)) + + %{ + rors: rors, + stores: stores, + loads: loads, + instructions: Enum.count(block, &(&1 =~ ~r/^\s+[a-z]/)) + } + end +end + +big = :crypto.strong_rand_bytes(16 * 1024 * 1024) +^big = big +true = KY.Yield.keccak256(big) == KY.Blocking.keccak256(big) + +for {name, mod} <- [{"yielding", KY.Yield}, {"blocking", KY.Blocking}] do + %{rors: r, stores: st, loads: ld, instructions: n} = KY.Spills.count(mod, name) + + IO.puts( + "#{String.pad_trailing(name, 10)} round loop: #{st} stack stores, #{ld} stack loads, #{r} ror, #{n} instructions" + ) +end + +t = fn f -> elem(:timer.tc(f), 0) / 1000 end + +IO.puts( + "\n16 MB keccak256, best and median of #{rounds} interleaved (other CPU: #{Float.round(Defk.Bench.other_cpu() * 1.0, 2)} cores)" +) + +pairs = + for _ <- 1..rounds do + {t.(fn -> KY.Yield.keccak256(big) end), t.(fn -> KY.Blocking.keccak256(big) end)} + end + +med = fn l -> Enum.at(Enum.sort(l), div(length(l), 2)) end +ys = Enum.map(pairs, &elem(&1, 0)) +bs = Enum.map(pairs, &elem(&1, 1)) + +IO.puts(" yielding #{Float.round(Enum.min(ys), 2)} / #{Float.round(med.(ys), 2)} ms") +IO.puts(" blocking #{Float.round(Enum.min(bs), 2)} / #{Float.round(med.(bs), 2)} ms") + +IO.puts( + " ratio #{Float.round(Enum.min(ys) / Enum.min(bs), 3)}x (best), #{Float.round(med.(ys) / med.(bs), 3)}x (median)" +) diff --git a/docs/performance.md b/docs/performance.md index ef9a4c2c..ca5f22ba 100644 --- a/docs/performance.md +++ b/docs/performance.md @@ -1727,7 +1727,8 @@ for LLVM. Resuming through each loop's header fixed it. "a safepoint every iteration" on the word loop. Each word is now a few ns of work, and yielding costs +19% (4.91-4.99 vs 4.11-4.20 ms, ~17 yields per query); `DEFK_SLICE_US=10000000` kept the gap. Under load defk gives - ~0.79x the blocking build's req/s. Open as `defk-w8r.1`. + ~0.79x the blocking build's req/s. Quiet it was +30%; one countdown + instead of two counters took it to +16% (6.46). - **Conditions:** `defk-nua`/`defk-j3h` load not recorded; `defk-klw` quiet (load average 3-6, no builds); `defk-l2g` load average 4-7; Linux not measured. - **Source:** `defk-nua` comment 2026-10-05, `defk-j3h` comment 2026-10-05, `defk-klw`, `defk-l2g`, [`fuzzy_search/README.md`](https://github.com/DanielLuning/defk/blob/main/examples/fuzzy_search/README.md), [results snapshot](https://github.com/DanielLuning/defk/blob/main/docs/project.md). - **Status:** measured; the Myers figures provisional. @@ -1839,7 +1840,9 @@ changed speed by 1.5x. (9-11 stores per round); `yield: false` 18.2-18.6 ms with 0 spills. Side effects: `xxh64` 4 MB 0.36-0.40 -> 0.175-0.182 ms (about 2x); siphash 1k keys 0.054-0.057 -> 0.043-0.044 ms. The remaining ~10% against `yield: - false` is yield bookkeeping held in registers (`defk-w8l`, open). + false` was read as yield bookkeeping held in registers; 6.46 measured it: + the counters are none of it, the safepoint's saves and the resume + dispatch are, and quiet the gap is 1.3x. - **Conditions:** under load (spill counts do not depend on load). - **Source:** `defk-zep` comment 2026-10-10 (f81c2cd, merge 522e7f2), [`keccak.exs`](https://github.com/DanielLuning/defk/blob/main/examples/keccak.exs). - **Status:** provisional (timings); the older "28 ms" and "0.55x of ex_keccak" figures are superseded. @@ -3033,6 +3036,93 @@ stays is about array contents. dropped check, and the agreement properties). - **Status:** measured. +### 6.46 Yield bookkeeping: one countdown instead of two counters halves fuzzy_search's per-word cost; Keccak's spills come from the safepoint's saves and the resume dispatch, not from the counters + +Two hot short loops paid for yielding where the yields themselves are +free (6.4): Keccak's round loop (24 trips, no safepoint inside; the +block loop around it has one per iteration) spilled per round in the +yielding kernel and not under `yield: false`, and fuzzy_search's word loop +(a safepoint per word, as each word holds a short inner loop) ran +19-31% +over its `yield: false` twin. `bench/keccak_yield.exs` compiles the +example's kernels twice and counts the stack loads and stores in the +hottest round block of the assembly (`cc -S` with the build's flags, the +block with the most `ror`, cut at its back-edge: the stores after it are +the loop's exit path, once per block) beside the 16 MB time; +`examples/fuzzy_search/bench/yield_cost.exs` gives the per-word gap. + +- **Before** (quiet): Keccak 12 stack stores and 12 loads per round, 164 + instructions, against 0 / 0 and 109 under `yield: false`; 16 MB 23.1 / + 23.3 ms (best / median of 7) against 17.2 / 17.6, 1.32-1.34x. The + 6.8 figures (9-11 spills, 20.7 vs 18.3 ms) were under load and counted + the exit path differently; quiet, the gap is a third. fuzzy_search: + yielding 5.1-5.4 ms a query against 3.9-4.1 blocking, +30-31% (three + runs; `defk-l2g`'s +19% was under load), 18-19 yields a query: about + 5 ns per word on 17. +- **The counters** (`defk-w8l`'s experiment (a); each variant changes + every yielding kernel's C): + - *V1, one countdown.* `defk_ticks` counts down from the budget and a + safepoint tests `<= 0`; the budget lives only in the clock + (`defk_clk.budget`), where `defk_tick` keeps it anyway. Keccak: 12 / 12 + spills, 23.3 / 23.5 ms, unchanged. fuzzy_search: 4.6-4.8 ms, +16-17% + (three runs: +17.4, +16.2, +15.7), 16.5 yields a query: about 3 ns + per word. **Adopted**: it removes one live value and one compare per + safepoint, and the semantics are the same (ticks >= budget is + budget - ticks <= 0; the resume restores the saved budget as before). + - *V2, charge a plain short loop on entry* (as a loop a halt can leave + already is): Keccak 12 / 12, 23.0 / 23.2 ms; fuzzy_search +21%. Alone + or with V1 (+17.5%) nothing beyond V1; not adopted. + - *V3, no bookkeeping register at all*: the countdown in the frame + (`F->ticks`), the dispatch test on `F->resume`, `env` in the clock so + the tick call needs no register. Keccak 12 / 12 spills, 22.6 / 23.1 + ms: unchanged. fuzzy_search +19.6% (two runs): the memory + read-modify-write per word costs more than the register it frees. + Not adopted. +- **Where Keccak's spills come from** (the yielding kernel's C with one + piece of the safepoint removed, assembled, the same count; the C of V3, + so no counter is in a register): as emitted 12 stores / 12 loads; the + tick call removed 15 / 16; the saves (`DEFK_SAVE`, the stores of the + enclosing loops' live locals and the 25 lanes into the frame at a yield) + removed 4 / 4; call and saves removed 4 / 4; no safepoint at all but the + resume dispatch kept 4 / 4; no dispatch either 1 / 1 and 118 + instructions, the `yield: false` shape. So 8 of the 12 spills are the + saves and 3 the dispatch (the `if (resuming) switch` at each loop body's + top and the arrival labels in front of the loops), and the counters are + none of them. The 25 lanes are the block loop's accumulators, live in + both kernels; what the saves change is clang's allocation around a cold + block that reads 35 values. Neither can go without a redesign (the saves + are the resume; the dispatch is how a resume re-enters the loops through + their headers, 6.4), so Keccak keeps its 1.3x and 6.8's "bookkeeping + held in registers" is superseded by this entry. +- **fuzzy_search's per-word cost, what remains after V1** (timing only, + the variants break resuming; two runs each): the resume + dispatch compiled out (`DEFK_RESUMING 0`: a resumed call re-enters only + through the kernel's top dispatch) +25-26%, worse, with more yields a + query (17.6): not a measurement of the test's cost, so it stays at "a + load and a branch per word"; the inner loop's strip form compiled out + (`DEFK_SHORT(R) 1`, so each word's loop is the plain loop and its trips + are charged on entry) +15-16% against V1's +17.6-18.4% in the same + session: about 2 points, inside the noise. What remains is the shape of + the word loop's body in a kernel that can yield, as in Keccak. +- **A cheaper shape for the outer loop:** one safepoint per N words would + let N x DEFK_STRIP inner trips run unchecked, past the tick-gap + contract; charging the outer loop in strips by the inner loop's trip + count is what the per-iteration safepoint already does (the inner loop + charges its trips on entry, the outer safepoint tests the countdown), + and after V1 that test is one subtract and one branch per word. The + per-word cost that remains is code shape, as in Keccak, not the check. +- **Checks:** `bench/tick_gap.exs` (3 runs a side): the yielding kernel's p99 + gap 2.27 ms on the branch against 2.25 on `main`, worst 2.3-2.5 against + 2.3; the early-exit kernel 2.27 / 2.27; unchanged. `mix test` green, the + forced-yield tests included (2309 passed). +- **Conditions:** M-series Mac, on battery, other processes at 0.2-0.8 + cores before each Keccak block (one block at 2.0: V1+V2, whose numbers + are not used); fuzzy_search runs on 12 schedulers, 20 queries x 5 + rounds, medians. +- **Source:** `defk-w8l` (and `defk-w8r.1`, merged into it), [`bench/keccak_yield.exs`](https://github.com/DanielLuning/defk/blob/main/bench/keccak_yield.exs), + [`examples/fuzzy_search/bench/yield_cost.exs`](https://github.com/DanielLuning/defk/blob/main/examples/fuzzy_search/bench/yield_cost.exs); `DEFK_SP` and + `DEFK_TICKS` in `lib/defk/compiler.ex` (`sp_macro/3`, `run_preamble/1`). +- **Status:** measured. + --- ## 7. When a hand-written or wrapper NIF is still the answer @@ -3378,4 +3468,5 @@ example or close a workload ticket, add its entries and its line here. `defk-o08.2`, `defk-o08.3`, `defk-o08.4`, `defk-o08.5`, `defk-o08.6`, `defk-w8r.2`, `defk-25s` ([`bench/call_cost.exs`](https://github.com/DanielLuning/defk/blob/main/bench/call_cost.exs)), `defk-vcx.2` ([`bench/elixir_mode.exs`](https://github.com/DanielLuning/defk/blob/main/bench/elixir_mode.exs)), - `defk-w8r.3` ([`bench/gather_layer.exs`](https://github.com/DanielLuning/defk/blob/main/bench/gather_layer.exs)). + `defk-w8r.3` ([`bench/gather_layer.exs`](https://github.com/DanielLuning/defk/blob/main/bench/gather_layer.exs)), + `defk-w8l` ([`bench/keccak_yield.exs`](https://github.com/DanielLuning/defk/blob/main/bench/keccak_yield.exs)). diff --git a/lib/defk/compiler.ex b/lib/defk/compiler.ex index 138dee5e..5d2fd080 100644 --- a/lib/defk/compiler.ex +++ b/lib/defk/compiler.ex @@ -5852,7 +5852,7 @@ defmodule Defk.Compiler do defp run_preamble(yields?) do if yields?, do: - "int defk_rs = F->resume;\nint64_t defk_ticks = 0;\nint64_t defk_budget = defk_rs ? F->budget : DEFK_BUDGET0;\ndefk_clock defk_clk;\ndefk_clock_init(&defk_clk, ctx);\n", + "int defk_rs = F->resume;\ndefk_clock defk_clk;\ndefk_clock_init(&defk_clk, ctx);\ndefk_clk.budget = defk_rs ? F->budget : DEFK_BUDGET0;\nint64_t defk_ticks = defk_clk.budget;\n", else: "" end @@ -5935,8 +5935,8 @@ defmodule Defk.Compiler do inputs = k |> input_aliases(saved) |> Enum.flat_map(&elem(&1, 1)) |> Enum.uniq() "#define DEFK_SAVE#{n} #{Enum.map(saved ++ inputs, &"F->#{&1} = #{&1}; ")}\n" end) <> - "#define DEFK_SP(N, W) if (DEFK_UNLIKELY((defk_ticks += (W)) >= defk_budget)) { defk_ticks = 0; if (!(defk_budget = defk_tick(env, &defk_clk, defk_budget))) { if (DEFK_UNLIKELY(F->resume)) { defk_lost_resume(ctx, F->resume, N); return DEFK_ERR; } DEFK_SAVE##N F->resume = N; F->budget = defk_clk.budget; return DEFK_YIELD; } }\n" <> - "#define DEFK_SHORT(R) DEFK_LIKELY((R) < DEFK_STRIP)\n#define DEFK_TICKS(W) defk_ticks += (W);\n#define DEFK_RESUMING DEFK_UNLIKELY(defk_rs)\n" + "#define DEFK_SP(N, W) if (DEFK_UNLIKELY((defk_ticks -= (W)) <= 0)) { if (!(defk_ticks = defk_tick(env, &defk_clk, defk_clk.budget))) { if (DEFK_UNLIKELY(F->resume)) { defk_lost_resume(ctx, F->resume, N); return DEFK_ERR; } DEFK_SAVE##N F->resume = N; F->budget = defk_clk.budget; return DEFK_YIELD; } }\n" <> + "#define DEFK_SHORT(R) DEFK_LIKELY((R) < DEFK_STRIP)\n#define DEFK_TICKS(W) defk_ticks -= (W);\n#define DEFK_RESUMING DEFK_UNLIKELY(defk_rs)\n" else @no_yield_macros end diff --git a/priv/defk_runtime.h b/priv/defk_runtime.h index 857d4734..10fc5aa8 100644 --- a/priv/defk_runtime.h +++ b/priv/defk_runtime.h @@ -62,7 +62,7 @@ * * kernel:start * DEFK_SP DEFK_SAVE DEFK_SAVE DEFK_SHORT DEFK_TICKS DEFK_RESUMING defk_rs - * defk_ticks defk_budget defk_clk defk_funcs defk_slot defk_z0 defk_a + * defk_ticks defk_clk defk_funcs defk_slot defk_z0 defk_a * defk_l defk_halt defk_r defk_rp defk_s_ defk_lit_ * kernel:end */ From 01baee4f08f1113c5fa713114b838eaddd7edf79 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20L=C3=BCning?= Date: Thu, 22 Oct 2026 12:35:50 +0200 Subject: [PATCH 3/3] defk-w8l: state 6.8's count as a fact, not a method; drop a no-op line in the bench --- bench/keccak_yield.exs | 1 - docs/performance.md | 7 ++++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/bench/keccak_yield.exs b/bench/keccak_yield.exs index dea9b22e..fef493e8 100644 --- a/bench/keccak_yield.exs +++ b/bench/keccak_yield.exs @@ -81,7 +81,6 @@ defmodule KY.Spills do end big = :crypto.strong_rand_bytes(16 * 1024 * 1024) -^big = big true = KY.Yield.keccak256(big) == KY.Blocking.keccak256(big) for {name, mod} <- [{"yielding", KY.Yield}, {"blocking", KY.Blocking}] do diff --git a/docs/performance.md b/docs/performance.md index ca5f22ba..3927feb4 100644 --- a/docs/performance.md +++ b/docs/performance.md @@ -3052,9 +3052,10 @@ the loop's exit path, once per block) beside the 16 MB time; - **Before** (quiet): Keccak 12 stack stores and 12 loads per round, 164 instructions, against 0 / 0 and 109 under `yield: false`; 16 MB 23.1 / - 23.3 ms (best / median of 7) against 17.2 / 17.6, 1.32-1.34x. The - 6.8 figures (9-11 spills, 20.7 vs 18.3 ms) were under load and counted - the exit path differently; quiet, the gap is a third. fuzzy_search: + 23.3 ms (best / median of 7) against 17.2 / 17.6, 1.32-1.34x. 6.8's + 9-11 spills were counted on the compiler of 2026-10-10 and its 20.7 vs + 18.3 ms under load; today, with the exit path left out, the count is 12 + / 12, and quiet the gap is a third. fuzzy_search: yielding 5.1-5.4 ms a query against 3.9-4.1 blocking, +30-31% (three runs; `defk-l2g`'s +19% was under load), 18-19 yields a query: about 5 ns per word on 17.