From 7393e1f98ee43b0df858da1bcc722d554dbebdc6 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 2 Oct 2024 17:02:23 -0500 Subject: [PATCH] Squashed commit of benchmarks-v3 / PR #204 --- .gitignore | 1 + Benchmarks.lean | 5 + Benchmarks/Command.lean | 121 ++++++++++++++------- Benchmarks/SHA512_150_noKernel_noLint.lean | 19 ++++ Benchmarks/SHA512_225_noKernel_noLint.lean | 19 ++++ Benchmarks/SHA512_400_noKernel_noLint.lean | 19 ++++ Benchmarks/SHA512_75.lean | 17 +++ Benchmarks/SHA512_75_noKernel_noLint.lean | 19 ++++ Makefile | 17 ++- README.md | 2 + lakefile.lean | 1 + scripts/benchmark.sh | 20 ++++ scripts/profile.sh | 20 ++++ 13 files changed, 241 insertions(+), 39 deletions(-) create mode 100644 Benchmarks/SHA512_150_noKernel_noLint.lean create mode 100644 Benchmarks/SHA512_225_noKernel_noLint.lean create mode 100644 Benchmarks/SHA512_400_noKernel_noLint.lean create mode 100644 Benchmarks/SHA512_75.lean create mode 100644 Benchmarks/SHA512_75_noKernel_noLint.lean create mode 100755 scripts/benchmark.sh create mode 100755 scripts/profile.sh diff --git a/.gitignore b/.gitignore index 6c2506f9..1e3e3f4d 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ /lake-packages/* /.lake/* *.log +/data/* diff --git a/Benchmarks.lean b/Benchmarks.lean index 7b7fcc0a..cc1f1c6b 100644 --- a/Benchmarks.lean +++ b/Benchmarks.lean @@ -3,6 +3,11 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Author(s): Alex Keizer -/ +import Benchmarks.SHA512_75 +import Benchmarks.SHA512_75_noKernel_noLint import Benchmarks.SHA512_150 +import Benchmarks.SHA512_150_noKernel_noLint import Benchmarks.SHA512_225 +import Benchmarks.SHA512_225_noKernel_noLint import Benchmarks.SHA512_400 +import Benchmarks.SHA512_400_noKernel_noLint diff --git a/Benchmarks/Command.lean b/Benchmarks/Command.lean index bf605c43..d27fca74 100644 --- a/Benchmarks/Command.lean +++ b/Benchmarks/Command.lean @@ -12,58 +12,103 @@ initialize defValue := false descr := "enables/disables benchmarking in `withBenchmark` combinator" } + registerOption `benchmark.runs { + defValue := (5 : Nat) + descr := "controls how many runs the `benchmark` command does. \ + NOTE: this value is ignored when the `profiler` option is set to true" + } + /- Shouldn't be set directly, instead, use the `benchmark` command -/ + registerTraceClass `benchmark variable {m} [Monad m] [MonadLiftT BaseIO m] in -def withHeartbeatsAndMs (x : m α) : m (α × Nat × Nat) := do +/-- Measure the heartbeats and time (in milliseconds) taken by `x` -/ +def withHeartbeatsAndMilliseconds (x : m α) : m (α × Nat × Nat) := do let start ← IO.monoMsNow let (a, heartbeats) ← withHeartbeats x let endTime ← IO.monoMsNow return ⟨a, heartbeats, endTime - start⟩ -elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do - logInfo m!"Running {id} benchmark\n" +/-- Adds a trace node with the `benchmark` class, but only if the profiler +option is *not* set. + +We deliberately suppress benchmarking nodes when profiling, since it generally +only adds noise +-/ +def withBenchTraceNode (msg : MessageData) (x : CommandElabM α ) + : CommandElabM α := do + if (← getBoolOption `profiler) then + x + else + withTraceNode `benchmark (fun _ => pure msg) x (collapsed := false) +/-- +Run a benchmark for a set number of times, and report the average runtime. + +If the `profiler` option is set true, we run the benchmark only once, with: +- `trace.profiler` to true, and +- `trace.profiler.output` set based on the `benchmark.profilerDir` and the + id of the benchmark +-/ +elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do + let originalOpts ← getOptions + let mut n := originalOpts.getNat `benchmark.runs 5 + let mut opts := originalOpts + opts := opts.setBool `benchmark true let stx ← `(command| - set_option benchmark true in example $declSig:optDeclSig $val:declVal ) - let n := 5 - let mut totalRunTime := 0 - -- geomean = exp(log((a₁ a₂ ... aₙ)^1/n)) = - -- exp(1/n * (log a₁ + log a₂ + log aₙ)). - let mut totalRunTimeLog := 0 - for i in [0:n] do - logInfo m!"\n\nRun {i} (out of {n}):\n" - let ((), _, runTime) ← withHeartbeatsAndMs <| - elabCommand stx - - logInfo m!"Proof took {runTime / 1000}s in total" - totalRunTime := totalRunTime + runTime - totalRunTimeLog := totalRunTimeLog + Float.log runTime.toFloat - - let avg := totalRunTime.toFloat / n.toFloat / 1000 - let geomean := (Float.exp (totalRunTimeLog / n.toFloat)) / 1000.0 - logInfo m!"\ -{id}: - average runtime over {n} runs: - {avg}s - geomean over {n} runs: - {geomean}s -" + if (← getBoolOption `profiler) then + opts := opts.setBool `trace.profiler true + n := 1 -- only run once, if `profiler` is set to true + else + opts := opts.setBool `trace.benchmark true + + if n = 0 then + return () + + -- Set options + modifyScope fun scope => { scope with opts } + + withBenchTraceNode m!"Running {id} benchmark" <| do + let mut totalRunTime := 0 + -- geomean = exp(log((a₁ a₂ ... aₙ)^1/n)) = + -- exp(1/n * (log a₁ + log a₂ + log aₙ)). + let mut totalRunTimeLog : Float := 0 + for i in [0:n] do + let runTime ← withBenchTraceNode m!"Run {i+1} (out of {n}):" <| do + let ((), _, runTime) ← withHeartbeatsAndMilliseconds <| + elabCommand stx + + trace[benchmark] m!"Proof took {runTime / 1000}s in total" + pure runTime + totalRunTime := totalRunTime + runTime + totalRunTimeLog := totalRunTimeLog + Float.log runTime.toFloat + + let avg := totalRunTime.toFloat / n.toFloat / 1000 + let geomean := (Float.exp (totalRunTimeLog / n.toFloat)) / 1000.0 + trace[benchmark] m!"\ + {id}: + average runtime over {n} runs: + {avg}s + geomean over {n} runs: + {geomean}s + " + -- Restore options + modifyScope fun scope => { scope with opts := originalOpts } /-- Set various options to disable linters -/ macro "disable_linters" "in" cmd:command : command => `(command| - set_option linter.constructorNameAsVariable false in - set_option linter.deprecated false in - set_option linter.missingDocs false in - set_option linter.omit false in - set_option linter.suspiciousUnexpanderPatterns false in - set_option linter.unnecessarySimpa false in - set_option linter.unusedRCasesPattern false in - set_option linter.unusedSectionVars false in - set_option linter.unusedVariables false in - $cmd +set_option linter.constructorNameAsVariable false in +set_option linter.deprecated false in +set_option linter.missingDocs false in +set_option linter.omit false in +set_option linter.suspiciousUnexpanderPatterns false in +set_option linter.unnecessarySimpa false in +set_option linter.unusedRCasesPattern false in +set_option linter.unusedSectionVars false in +set_option linter.unusedVariables false in +$cmd ) /-- The default `maxHeartbeats` setting. @@ -96,7 +141,7 @@ private def withBenchmarkAux (x : m α) (f : Nat → Nat → m Unit) : m α := if (← getBoolOption `benchmark) = false then x else - let (a, heartbeats, t) ← withHeartbeatsAndMs x + let (a, heartbeats, t) ← withHeartbeatsAndMilliseconds x f heartbeats t return a diff --git a/Benchmarks/SHA512_150_noKernel_noLint.lean b/Benchmarks/SHA512_150_noKernel_noLint.lean new file mode 100644 index 00000000..a801bd79 --- /dev/null +++ b/Benchmarks/SHA512_150_noKernel_noLint.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Alex Keizer +-/ +import Tactics.Sym +import Benchmarks.Command +import Benchmarks.SHA512 + +open Benchmarks + +disable_linters in +set_option debug.skipKernelTC true in +benchmark sha512_150_noKernel_noLint : SHA512Bench 150 := fun s0 _ h => by + intros + sym_n 150 + simp only [h, bitvec_rules] + · exact (sorry : Aligned ..) + done diff --git a/Benchmarks/SHA512_225_noKernel_noLint.lean b/Benchmarks/SHA512_225_noKernel_noLint.lean new file mode 100644 index 00000000..6bdc12b5 --- /dev/null +++ b/Benchmarks/SHA512_225_noKernel_noLint.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Alex Keizer +-/ +import Tactics.Sym +import Benchmarks.Command +import Benchmarks.SHA512 + +open Benchmarks + +disable_linters in +set_option debug.skipKernelTC true in +benchmark sha512_225_noKernel_noLint : SHA512Bench 225 := fun s0 _ h => by + intros + sym_n 225 + simp only [h, bitvec_rules] + · exact (sorry : Aligned ..) + done diff --git a/Benchmarks/SHA512_400_noKernel_noLint.lean b/Benchmarks/SHA512_400_noKernel_noLint.lean new file mode 100644 index 00000000..06f90357 --- /dev/null +++ b/Benchmarks/SHA512_400_noKernel_noLint.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Alex Keizer +-/ +import Tactics.Sym +import Benchmarks.Command +import Benchmarks.SHA512 + +open Benchmarks + +disable_linters in +set_option debug.skipKernelTC true in +benchmark sha512_400_noKernel_noLint : SHA512Bench 400 := fun s0 _ h => by + intros + sym_n 400 + simp only [h, bitvec_rules] + · exact (sorry : Aligned ..) + done diff --git a/Benchmarks/SHA512_75.lean b/Benchmarks/SHA512_75.lean new file mode 100644 index 00000000..a0ab30db --- /dev/null +++ b/Benchmarks/SHA512_75.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Alex Keizer +-/ +import Tactics.Sym +import Benchmarks.Command +import Benchmarks.SHA512 + +open Benchmarks + +benchmark sha512_75 : SHA512Bench 75 := fun s0 _ h => by + intros + sym_n 75 + simp only [h, bitvec_rules] + · exact (sorry : Aligned ..) + done diff --git a/Benchmarks/SHA512_75_noKernel_noLint.lean b/Benchmarks/SHA512_75_noKernel_noLint.lean new file mode 100644 index 00000000..454c4e51 --- /dev/null +++ b/Benchmarks/SHA512_75_noKernel_noLint.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Alex Keizer +-/ +import Tactics.Sym +import Benchmarks.Command +import Benchmarks.SHA512 + +open Benchmarks + +disable_linters in +set_option debug.skipKernelTC true in +benchmark sha512_75_noKernel_noLint : SHA512Bench 75 := fun s0 _ h => by + intros + sym_n 75 + simp only [h, bitvec_rules] + · exact (sorry : Aligned ..) + done diff --git a/Makefile b/Makefile index 00cf37c6..e3900c20 100644 --- a/Makefile +++ b/Makefile @@ -5,6 +5,8 @@ SHELL := /bin/bash LAKE = lake +LEAN = $(LAKE) env lean +GIT = git NUM_TESTS?=3 VERBOSE?=--verbose @@ -37,9 +39,22 @@ awslc_elf: cosim: time -p lake exe lnsym $(VERBOSE) --num-tests $(NUM_TESTS) +BENCHMARKS = Benchmarks/SHA512_75.lean \ + Benchmarks/SHA512_75_noKernel_noLint.lean \ + Benchmarks/SHA512_150.lean \ + Benchmarks/SHA512_150_noKernel_noLint.lean \ + Benchmarks/SHA512_225.lean \ + Benchmarks/SHA512_225_noKernel_noLint.lean \ + Benchmarks/SHA512_400.lean \ + Benchmarks/SHA512_400_noKernel_noLint.lean + .PHONY: benchmarks benchmarks: - $(LAKE) build Benchmarks + ./scripts/benchmark.sh $(BENCHMARKS) + +.PHONY: profile +profile: + ./scripts/profile.sh $(BENCHMARKS) .PHONY: clean clean_all clean: diff --git a/README.md b/README.md index 47939c18..2054fdf4 100644 --- a/README.md +++ b/README.md @@ -43,6 +43,8 @@ native-code programs of interest. `benchmarks`: run benchmarks for the symbolic simulator. +`profiler`: run a single round of each benchmark, with the profiler enabled + ### Makefile variables that can be passed in at the command line `VERBOSE`: Verbose mode; prints disassembly of the instructions being diff --git a/lakefile.lean b/lakefile.lean index 7175ad63..66000295 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -33,6 +33,7 @@ lean_lib «Doc» where -- add library configuration options here lean_lib «Benchmarks» where + leanOptions := #[⟨`weak.benchmark.runs, (0 : Nat)⟩] -- add library configuration options here @[default_target] diff --git a/scripts/benchmark.sh b/scripts/benchmark.sh new file mode 100755 index 00000000..028b2bf4 --- /dev/null +++ b/scripts/benchmark.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +LAKE=lake +BENCH="$LAKE env lean -Dweak.benchmark.runs=5" +OUT="data/benchmarks" + +timestamp=$(date +"%Y-%m-%d_%H%M%S") +rev=$(git rev-parse --short HEAD) +echo "HEAD is on $rev" +out="$OUT/${timestamp}_${rev}" +mkdir -p "$out" + +$LAKE build Benchmarks +for file in "$@"; do + echo + echo + $file + echo + base="$(basename "$file" ".lean")" + $BENCH $file | tee "$out/$base" +done diff --git a/scripts/profile.sh b/scripts/profile.sh new file mode 100755 index 00000000..ccc1433d --- /dev/null +++ b/scripts/profile.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +LAKE=lake +PROF="$LAKE env lean -Dprofiler=true" +OUT="data/profiles" + +timestamp=$(date +"%Y-%m-%d_%H%M%S") +rev=$(git rev-parse --short HEAD) +echo "HEAD is on $rev" +out="$OUT/${timestamp}_${rev}" +mkdir -p "$out" + +$LAKE build Benchmarks +for file in "$@"; do + echo + echo + $file + echo + base="$(basename "$file" ".lean")" + $PROF -Dtrace.profiler.output="$out/$base.json" "$file" | tee "$base.log" +done