diff --git a/dev/compile_time.exs b/dev/compile_time.exs new file mode 100644 index 00000000..686e62d4 --- /dev/null +++ b/dev/compile_time.exs @@ -0,0 +1,107 @@ +# Compiler time: compare rounds of DEFK_COMPILE_TIME logs from two +# checkouts. One round is one dump of every kernel, its log one line per +# module, " " of a compile measured in a +# fresh process (Defk.__before_compile__): +# +# DEFK_COMPILE_TIME=tmp/base1.log DEFK_DUMP_C=tmp/c_base mix dump_c # in the base checkout +# DEFK_COMPILE_TIME=tmp/new1.log DEFK_DUMP_C=tmp/c_new mix dump_c # in the new one +# ... base2, new2, ..., interleaved so drift hits both sides ... +# elixir dev/compile_time.exs tmp/base*.log -- tmp/new*.log +# elixir dev/compile_time.exs --reductions tmp/base*.log -- tmp/new*.log +# +# Microseconds drift with the machine (a laptop's clock on battery moved a +# whole round by about 25% between runs); reductions, the work the BEAM +# counts, repeat to about 0.1% and are the figure to compare when the +# change is the compiler's own work. Only the modules every log has are +# compared, so kernels added between the two checkouts do not count as a +# cost, but a kernel edited between them does: check that the examples and +# test modules are unchanged. A module name compiled twice in one round +# (two files) is summed. Each side's figure is the median of its rounds, +# with and without SatEx.Kernels (examples/cdcl_sat.exs, thousands of kept +# checks: it dominates any prover cost). With no `--`, the logs are one +# side and only its medians are printed. + +{column, args} = + case System.argv() do + ["--reductions" | rest] -> {2, rest} + rest -> {1, rest} + end + +{base_paths, new_paths} = + case Enum.split_while(args, &(&1 != "--")) do + {base, ["--" | new]} -> {base, new} + {base, []} -> {base, []} + end + +if base_paths == [] do + IO.puts( + :stderr, + "usage: elixir dev/compile_time.exs [--reductions] [-- ]" + ) + + System.halt(2) +end + +read = fn path -> + for line <- File.read!(path) |> String.split("\n", trim: true), + [mod | figures] = String.split(line), + n = String.to_integer(Enum.at(figures, column - 1)), + reduce: %{}, + do: (acc -> Map.update(acc, mod, n, &(&1 + n))) +end + +{base, new} = {Enum.map(base_paths, read), Enum.map(new_paths, read)} + +common = + (base ++ new) + |> Enum.map(&MapSet.new(Map.keys(&1))) + |> Enum.reduce(&MapSet.intersection/2) + +median = fn xs -> + sorted = Enum.sort(xs) + n = length(sorted) + mid = div(n, 2) + + if rem(n, 2) == 1, + do: Enum.at(sorted, mid), + else: div(Enum.at(sorted, mid - 1) + Enum.at(sorted, mid), 2) +end + +total = fn round, mods -> mods |> Enum.map(&Map.fetch!(round, &1)) |> Enum.sum() end +without_sat = MapSet.delete(common, "SatEx.Kernels") + +side = fn rs -> + {median.(Enum.map(rs, &total.(&1, common))), median.(Enum.map(rs, &total.(&1, without_sat)))} +end + +show = + if column == 1, + do: fn us -> :erlang.float_to_binary(us / 1000, decimals: 1) <> " ms" end, + else: fn r -> :erlang.float_to_binary(r / 1.0e6, decimals: 2) <> "M reductions" end + +pct = fn a, b -> :erlang.float_to_binary(100 * (b - a) / a, decimals: 1) <> "%" end + +IO.puts( + "#{MapSet.size(common)} modules in every log; rounds: #{length(base)} base, #{length(new)} new" +) + +{b_all, b_wo} = side.(base) +IO.puts("base: #{show.(b_all)} (without SatEx.Kernels #{show.(b_wo)})") + +if new != [] do + {n_all, n_wo} = side.(new) + IO.puts("new: #{show.(n_all)} (without SatEx.Kernels #{show.(n_wo)})") + IO.puts("change: #{pct.(b_all, n_all)} (without SatEx.Kernels #{pct.(b_wo, n_wo)})") + + deltas = + for m <- common do + {m, median.(Enum.map(new, & &1[m])) - median.(Enum.map(base, & &1[m]))} + end + + IO.puts("largest changes by module (median):") + + deltas + |> Enum.sort_by(&(-abs(elem(&1, 1)))) + |> Enum.take(5) + |> Enum.each(fn {m, d} -> IO.puts(" #{m} #{if d >= 0, do: "+", else: ""}#{show.(d)}") end) +end diff --git a/docs/adr/0007-symbolic-bounds.md b/docs/adr/0007-symbolic-bounds.md index 7f860095..2c15385c 100644 --- a/docs/adr/0007-symbolic-bounds.md +++ b/docs/adr/0007-symbolic-bounds.md @@ -80,7 +80,12 @@ Replace the fact model with one representation: (products, `defk-pvt`) +1.7% (+0.9% without `SatEx.Kernels`) after cutting a second fact lookup per step and the ranking of one-term forms; the chain is at about +14%, under the ceiling, with about 1% left - (`docs/performance.md` 6.37). + (`docs/performance.md` 6.37). Measured again (2026-10-20) with a warm + compile in a fresh process (6.38; the method before included waiting + and heap noise): the chain cost +13.4% of the time but +20.8% of the + work (reductions), and the refactors after it another +13.5% / +7.3%. + The compiler is at about +29% of its time before step 1, past the + ceiling; the next step cuts first (the copy analysis, `defk-o08.3`). - **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/agents/runs.md b/docs/agents/runs.md index 968d2f11..d964836b 100644 --- a/docs/agents/runs.md +++ b/docs/agents/runs.md @@ -61,9 +61,23 @@ cores it uses. ## Compiler time -The compiler-time rounds (a temporary `:timer.tc` around -`Defk.Compiler.compile` in `Defk.__before_compile__`, interleaved `mix -dump_c` rounds on both sides) measure defk's compile, not `cc`, so they run -without `cc` too. Name the files when the change touches only some kernels, -and report `SatEx.Kernels` (`examples/cdcl_sat.exs`) on its own: it -dominates the prover's cost. +The compiler-time rounds measure defk's compile, not `cc`, so they run +without `cc` too. With `DEFK_COMPILE_TIME=` set, every module compiles +once more in a fresh process and logs that compile's microseconds and +reductions (`Defk.__before_compile__`, `timed_compile/2`). Run interleaved +rounds on both sides and compare them: + + DEFK_COMPILE_TIME=tmp/base1.log DEFK_DUMP_C=tmp/c_base mix dump_c # base checkout + DEFK_COMPILE_TIME=tmp/new1.log DEFK_DUMP_C=tmp/c_new mix dump_c # branch + ... base2, new2 ... + elixir dev/compile_time.exs --reductions tmp/base*.log -- tmp/new*.log + elixir dev/compile_time.exs tmp/base*.log -- tmp/new*.log + +Two rounds a side are enough for reductions, which repeat to about 0.1%; +microseconds drift with the machine (about 25% between runs on a laptop +on battery), so report them with the conditions. A full round takes about +a minute and a half. Name the files when the change touches only some +kernels, and report `SatEx.Kernels` (`examples/cdcl_sat.exs`) on its own: +it dominates the prover's cost. Do not time a module's first compile: under +`mix compile` it waits for the compiler's own modules (`docs/performance.md` +6.38). diff --git a/docs/performance.md b/docs/performance.md index 6447d776..57349453 100644 --- a/docs/performance.md +++ b/docs/performance.md @@ -2514,6 +2514,48 @@ else: 0))`; it now says `if first < 0 and n > 0, do: raise(ArgumentError, the whole suite under AddressSanitizer. - **Status:** measured, provisional. +### 6.38 Compiler time: measure a second compile in a fresh process; the chain and the refactors cost ~29% together + +- **The method before** (6.32-6.37) timed `Defk.Compiler.compile` once per + module under `mix dump_c`. That run is `compile --force`, so `lib` and + `test/support` compile in parallel, and the first kernel module + (`Examples.Kernels`) waited about 1 s for the compiler's own modules: of + a 2.5 s round, about 1.0 s was that wait (the module needs 13 ms warm). + A second compile in the same process was no better: `SatEx.Kernels` + then took either ~240 or ~510 ms on the same code (what the first + compile left on the heap), and a whole round moved by ~25% between two + runs on the laptop. +- **The method now:** `DEFK_COMPILE_TIME=` makes every module compile + once for its result and once more in a fresh process, which is measured: + microseconds and the process's reductions. `dev/compile_time.exs` + compares interleaved rounds of two checkouts on the modules both have. + Five compiles of `SatEx.Kernels`: 355-369 ms, 50.64-50.68 M reductions + (±2% and ±0.05%). Reductions are the figure to compare for a change to + the compiler's own work; time is the one a user feels. +- **Numbers** (99 modules both checkouts have, two rounds each, + interleaved, medians): before step 1 (`23e27970`) 105.8 M reductions / + 801 ms; after step 4 (`a371dcab`) 127.8 M / 909 ms; main (`b90ed0ff`) + 137.1 M / 1,032 ms. The symbolic-bounds chain: +20.8% reductions, +13.4% + time (without `SatEx.Kernels` +6.8%, +3.9%). The readability refactors + after it (`x3a`, `rt2`): +7.3% reductions, +13.5% time (+6.7%, +3.3%). + Together +29.5% reductions, +28.8% time (+14.0%, +7.3%). `SatEx.Kernels` + alone went from ~150 to ~340 ms. +- **What it means:** the chain's own +14% (6.37) holds for time but not for + work, and the compiler is about twice as far past its state before step + 1 as the +15% ceiling of ADR-0007 allows, half of it from refactors no + budget covered. Where the time is (one warm round, 2026-10-20): the copy + analysis's per-statement walks ~16% (`Copies.nested/3` 9.7%), the + prover ~3.5%, the report's hint search 2.4%, the strip classifier 2.4%; + the rest is spread over the lowering. +- **Conditions:** M-series Mac on battery, no quiet check; `cc` not run + (`DEFK_NO_CC=1`; the baseline with the `DEFK_NO_CC` change applied, a + tooling change). A few examples and test kernels changed between the + checkouts (`hash_chain.exs` gained a raising guard), so the 99 modules are + not all identical; `SatEx.Kernels` (`cdcl_sat.exs`) is. +- **Source:** `defk-o08.2`; `dev/compile_time.exs`; the harness in + `Defk.__before_compile__` (`timed_compile/2`). +- **Status:** measured, provisional. + --- ## 7. When a hand-written or wrapper NIF is still the answer @@ -2820,4 +2862,5 @@ example or close a workload ticket, add its entries and its line here. `defk-l2g`, `defk-yzw`, `defk-dtw.2`, `defk-dtw.20`, `defk-dtw.21`, `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-7dm` ([`bench/port_roundtrip.exs`](https://github.com/DanielLuning/defk/blob/main/bench/port_roundtrip.exs)), `defk-1ub`, + `defk-o08.2`. diff --git a/lib/defk.ex b/lib/defk.ex index ca69d1ec..e32f349d 100644 --- a/lib/defk.ex +++ b/lib/defk.ex @@ -439,12 +439,14 @@ defmodule Defk do adaptive? = Module.get_attribute(env.module, :defk_adaptive_slice) {c_src, all_sigs, report} = - Defk.Compiler.compile(env.module, kernels, env.file, - nif_name: nif_name, - fault_hooks: fault_hooks?, - adaptive_slice: adaptive?, - max_owned_bytes: max_owned_bytes!(env.module) - ) + timed_compile(env.module, fn -> + Defk.Compiler.compile(env.module, kernels, env.file, + nif_name: nif_name, + fault_hooks: fault_hooks?, + adaptive_slice: adaptive?, + max_owned_bytes: max_owned_bytes!(env.module) + ) + end) # a yielding kernel's NIF takes the run-queue hint: it is # renamed, and the kernel's function passes the hint @@ -520,6 +522,48 @@ defmodule Defk do File.write!(Path.join(dir, "#{inspect(module)}.c"), c_src) end + # DEFK_COMPILE_TIME=: every module compiled while it is set appends + # " " to , of a second compile + # run in a fresh process (dev/compile_time.exs). The first compile, whose + # result the module uses, is not measured: under `mix compile` it may wait + # for the compiler's own modules, compiled in parallel with the kernels, + # and that wait is not compiler work. A fresh process starts with a small + # heap, so the time does not depend on what the first compile left. Like + # DEFK_DUMP_C, a side channel: the module is unchanged. + defp timed_compile(module, compile) do + case System.get_env("DEFK_COMPILE_TIME") do + nil -> + compile.() + + log -> + result = compile.() + {us, reductions} = measured(compile) + File.write!(log, "#{inspect(module)} #{us} #{reductions}\n", [:append]) + result + end + end + + defp measured(compile) do + parent = self() + + {pid, mref} = + spawn_monitor(fn -> + {:reductions, r0} = Process.info(self(), :reductions) + {us, _} = :timer.tc(compile) + {:reductions, r1} = Process.info(self(), :reductions) + send(parent, {self(), us, r1 - r0}) + end) + + receive do + {^pid, us, reductions} -> + Process.demonitor(mref, [:flush]) + {us, reductions} + + {:DOWN, ^mref, :process, ^pid, reason} -> + raise "DEFK_COMPILE_TIME: the measured compile failed: #{inspect(reason)}" + end + end + # `use Defk, max_owned_bytes: n`: a positive integer of bytes that fits in # a uint64 (DEFK_MAX_OWNED), or nil (the runtime's default) defp max_owned_bytes!(module) do