Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP: feat: integrate simp_mem with sym_n #179

Draft
wants to merge 53 commits into
base: main
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
53 commits
Select commit Hold shift + click to select a range
a5c4d44
feat: withBenchmark combinator for fine-grained benchmarking
alexkeizer Sep 26, 2024
8e44bd9
feat: aggregated benchmarks
alexkeizer Sep 26, 2024
0ab52f3
refactor: extract a `withHeartbeatsAndMs` combinator
alexkeizer Sep 26, 2024
1e71b8d
feat: withBenchmarksReport combinator
alexkeizer Sep 26, 2024
59d1c2d
feat: benchmark a less trivial condition, using the numBlocks register
alexkeizer Sep 26, 2024
50128e3
refactor: BenchT abbrev
alexkeizer Sep 26, 2024
8378162
fix: pc of SHA512 benchmark
alexkeizer Sep 26, 2024
7dc9282
fix: reinstate 150 step benchmark
alexkeizer Sep 26, 2024
93a3f81
feat: preserve insertion order of the first sample of an aggregated stat
alexkeizer Sep 26, 2024
1f948b8
Merge branch 'main' into benchmarks-v2
alexkeizer Sep 26, 2024
1c56f0e
fix: sorry-out alignment goals in benchmark
alexkeizer Sep 26, 2024
9443720
feat: macro to disable multiple linters
alexkeizer Sep 27, 2024
e838675
feat: change the behaviour of `benchmark` when `profiler` is set to t…
alexkeizer Sep 27, 2024
1123c54
feat: add benchmarks with kernel and linters disabled
alexkeizer Sep 27, 2024
430fd9e
fix: remove accidental profiler option
alexkeizer Sep 27, 2024
ff86cf1
feat: bail early if there are no runs in a benchmark
alexkeizer Sep 27, 2024
718d8d6
refactor: prefer traces over log
alexkeizer Sep 27, 2024
a2afadb
refactor: invoke lean directly to run benchmarks
alexkeizer Sep 27, 2024
99f3f0f
fix: print hash of HEAD when doing benchmarks
alexkeizer Sep 27, 2024
998dbbc
fix: actually use `BENCH`, which explicitly sets the number of runs
alexkeizer Sep 27, 2024
5253302
feat: `profiler` make target
alexkeizer Sep 27, 2024
8c0940a
feat: suppress benchmark trace nodes in the profiler
alexkeizer Sep 27, 2024
ff43937
refactor: drop a use of `h_sp?`
alexkeizer Oct 1, 2024
79bc06d
refactor: drop the other use of hSp
alexkeizer Oct 1, 2024
e887c14
refactor: remove `SymContext.h_sp?`
alexkeizer Oct 1, 2024
42142ef
refactor: simplify `sym1` simplification step
alexkeizer Oct 1, 2024
b48f168
feat: attempt to preserve stack alignment roof in AxEffect update
alexkeizer Oct 1, 2024
477d811
Merge branch 'main' into benchmarks-v3
alexkeizer Oct 2, 2024
7e08a4b
revert bad merge
alexkeizer Oct 2, 2024
1ef20d7
chore: rename `withHeartbeatsAndMs` -> `...AndMilliseconds`
alexkeizer Oct 2, 2024
193ba2d
remove `profilerDir` option
alexkeizer Oct 2, 2024
ca101bc
feat: write shell-scripts to automatically log benchmark/profile data…
alexkeizer Oct 2, 2024
5c94d37
fix: set profile file extension to `.json`
alexkeizer Oct 2, 2024
e1860ad
Squashed commit of benchmarks-v3 / PR #204
alexkeizer Oct 2, 2024
32614c3
chore: add more trace nodes, for better profiling data
alexkeizer Oct 2, 2024
6aca323
chore: add tags to trace nodes
alexkeizer Oct 2, 2024
df3ab2c
chore: reduce threshold in profiler
alexkeizer Oct 2, 2024
e24b5db
chore: reduce threshold in profiler
alexkeizer Oct 2, 2024
e5f62fe
feat: use `withCurrHeartbeats` to reset the heartbeat usage for each …
alexkeizer Oct 3, 2024
fb314f4
fix SHA512 benchmark to compute the correct expected value for all nu…
alexkeizer Oct 3, 2024
9628874
Merge branch 'main' into benchmarks-v3
alexkeizer Oct 3, 2024
2fc7ece
fix SHA512 benchmark to compute the correct expected value for all nu…
alexkeizer Oct 3, 2024
f13d7f0
feat: add 50 step benchmark
alexkeizer Oct 3, 2024
74b3b9c
feat: make benchmarks more robust against changes in `sym_n`
alexkeizer Oct 3, 2024
2fd9ccb
Merge branch 'benchmarks-v3' into better-tracing
alexkeizer Oct 3, 2024
147db12
Merge branch 'better-tracing' into snorkel-heartbeats
alexkeizer Oct 3, 2024
b8fa9b5
refactor: move tracing helpers to new `Sym/Common` file
alexkeizer Oct 3, 2024
366d482
feat: improve tracing for `AxEffects`
alexkeizer Oct 3, 2024
fa4030e
chore: make section names more meaningful
alexkeizer Oct 4, 2024
66ad4fd
refactor: extract out `MemoryEffects` structure
alexkeizer Oct 7, 2024
077b5da
fix `MemoryEffects.validate` to expect the right type
alexkeizer Oct 7, 2024
40cb6f2
feat: integrate simp_mem with sym_n
alexkeizer Oct 7, 2024
711cf60
remove helpers that were moved to common file
alexkeizer Oct 7, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
remove profilerDir option
The `trace.profiler.output` option has to be set when the frontend finishes the entire file. Therefore, it doesn't make sense to control it from within the benchmark elaborator: it's likely to do unexpected things if we have multiple benchmarks in the same file.

Instead, we should be setting the option from the makefile that runs the benchmark to begin with
  • Loading branch information
alexkeizer committed Oct 2, 2024
commit 193ba2dacd3ee35ff1f6c2590905a3343a98dac8
6 changes: 0 additions & 6 deletions Benchmarks/Command.lean
Original file line number Diff line number Diff line change
@@ -17,10 +17,6 @@ initialize
descr := "controls how many runs the `benchmark` command does. \
NOTE: this value is ignored when the `profiler` option is set to true"
}
registerOption `benchmark.profilerDir {
defValue := "profiles/"
descr := "where to put profile output files"
}
/- Shouldn't be set directly, instead, use the `benchmark` command -/
registerTraceClass `benchmark

@@ -63,9 +59,7 @@ elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do
)

if (← getBoolOption `profiler) then
let outDir := (← getOptions).getString `benchmark.profilerDir
opts := opts.setBool `trace.profiler true
opts := opts.setString `trace.profiler.output s!"{outDir}/{id.getId}"
n := 1 -- only run once, if `profiler` is set to true
else
opts := opts.setBool `trace.benchmark true