From 4414dc58c7986cc100925f62954e09831020a724 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 25 Sep 2024 19:19:55 -0500 Subject: [PATCH] feat: benchmark setup (#183) ### Description: Add a basic benchmark setup: - `benchmark` command, which has a theorem-like syntax, but doesn't get added to the environment, and runs the proof 5 times, reporting both the individual and average runtime, - similarly, a `logHeartbeats` tactic combinator, which measures the heartbeats used by an arbitrary tactic. - Add a benchmark folder, with files for SHA512 runs with: 150, 225, and 400 steps (which are the numbers I've been reporting so far) - Adds a `make benchmark` Make-target, to build the aforementioned files. Crucially, this target is *not* part of `make all`, for all our sanity's sake (running 400 steps of SHA512 for 5 times takes a while) ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? yes ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --------- Co-authored-by: Siddharth Co-authored-by: Shilpi Goel --- .github/workflows/makefile.yml | 5 ++++ Benchmarks.lean | 8 ++++++ Benchmarks/Command.lean | 50 ++++++++++++++++++++++++++++++++++ Benchmarks/SHA512.lean | 23 ++++++++++++++++ Benchmarks/SHA512_150.lean | 15 ++++++++++ Benchmarks/SHA512_225.lean | 15 ++++++++++ Benchmarks/SHA512_400.lean | 15 ++++++++++ Makefile | 10 +++++-- README.md | 4 ++- Tactics/Sym.lean | 2 -- Tactics/SymContext.lean | 10 +++---- lakefile.lean | 3 ++ 12 files changed, 150 insertions(+), 10 deletions(-) create mode 100644 Benchmarks.lean create mode 100644 Benchmarks/Command.lean create mode 100644 Benchmarks/SHA512.lean create mode 100644 Benchmarks/SHA512_150.lean create mode 100644 Benchmarks/SHA512_225.lean create mode 100644 Benchmarks/SHA512_400.lean diff --git a/.github/workflows/makefile.yml b/.github/workflows/makefile.yml index a272a748..a9826fd6 100644 --- a/.github/workflows/makefile.yml +++ b/.github/workflows/makefile.yml @@ -42,3 +42,8 @@ jobs: if : ${{ runner.os == 'macOS' }} run: | make cosim NUM_TESTS=100 + + - name: Run LNSym Benchmarks (Ubuntu) + if : ${{ runner.os != 'macOS' }} + run: | + make benchmarks diff --git a/Benchmarks.lean b/Benchmarks.lean new file mode 100644 index 00000000..7b7fcc0a --- /dev/null +++ b/Benchmarks.lean @@ -0,0 +1,8 @@ +/- +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_150 +import Benchmarks.SHA512_225 +import Benchmarks.SHA512_400 diff --git a/Benchmarks/Command.lean b/Benchmarks/Command.lean new file mode 100644 index 00000000..7d903fc4 --- /dev/null +++ b/Benchmarks/Command.lean @@ -0,0 +1,50 @@ +/- +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 Lean + +open Lean Parser.Command Elab.Command + +elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do + let stx ← `(command| example $declSig:optDeclSig $val:declVal ) + + let n := 5 + let mut runTimes := #[] + let mut totalRunTime := 0 + for _ in [0:n] do + let start ← IO.monoMsNow + elabCommand stx + let endTime ← IO.monoMsNow + let runTime := endTime - start + runTimes := runTimes.push runTime + totalRunTime := totalRunTime + runTime + + let avg := totalRunTime.toFloat / n.toFloat / 1000 + let geomean := (totalRunTime.toFloat.pow (1.0 / n.toFloat)) / 1000.0 + logInfo m!"\ +{id}: + average runtime over {n} runs: + {avg}s + geomean over {n} runs: + {geomean}s + + indidividual runtimes: + {runTimes} +" + +/-- The default `maxHeartbeats` setting. + +NOTE: even if the actual default value changes at some point in the future, +this value should *NOT* be updated, to ensure the percentages we've reported +in previous versions remain comparable. -/ +def defaultMaxHeartbeats : Nat := 200000 + +open Elab.Tactic in +elab "logHeartbeats" tac:tactic : tactic => do + let ((), heartbeats) ← withHeartbeats <| + evalTactic tac + let percent := heartbeats / (defaultMaxHeartbeats * 10) + + logInfo m!"used {heartbeats / 1000} heartbeats ({percent}% of the default maximum)" diff --git a/Benchmarks/SHA512.lean b/Benchmarks/SHA512.lean new file mode 100644 index 00000000..1ef411bb --- /dev/null +++ b/Benchmarks/SHA512.lean @@ -0,0 +1,23 @@ +/- +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 Proofs.SHA512.SHA512StepLemmas + +/-! +### Symbolic Simulation for SHA512 +This file sets up the basic shape of a simulation of SHA512 +for a set number of instructions +-/ + +namespace Benchmarks + +def SHA512Bench (nSteps : Nat) : Prop := + ∀ (s0 sf : ArmState) + (_h_s0_pc : read_pc s0 = 0x1264c4#64) + (_h_s0_err : read_err s0 = StateError.None) + (_h_s0_sp_aligned : CheckSPAlignment s0) + (_h_s0_program : s0.program = SHA512.program) + (_h_run : sf = run nSteps s0), + r StateField.ERR sf = StateError.None diff --git a/Benchmarks/SHA512_150.lean b/Benchmarks/SHA512_150.lean new file mode 100644 index 00000000..b54d8f83 --- /dev/null +++ b/Benchmarks/SHA512_150.lean @@ -0,0 +1,15 @@ +/- +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_150_instructions : SHA512Bench 150 := fun s0 => by + intros + sym_n 150 + done diff --git a/Benchmarks/SHA512_225.lean b/Benchmarks/SHA512_225.lean new file mode 100644 index 00000000..26310030 --- /dev/null +++ b/Benchmarks/SHA512_225.lean @@ -0,0 +1,15 @@ +/- +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_225_instructions : SHA512Bench 225 := fun s0 => by + intros + sym_n 225 + done diff --git a/Benchmarks/SHA512_400.lean b/Benchmarks/SHA512_400.lean new file mode 100644 index 00000000..bd725f6f --- /dev/null +++ b/Benchmarks/SHA512_400.lean @@ -0,0 +1,15 @@ +/- +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.SHA512 +import Benchmarks.Command + +open Benchmarks + +benchmark sha512_400_instructions : SHA512Bench 400 := fun s0 => by + intros + sym_n 400 + done diff --git a/Makefile b/Makefile index 3639a262..00cf37c6 100644 --- a/Makefile +++ b/Makefile @@ -9,8 +9,10 @@ LAKE = lake NUM_TESTS?=3 VERBOSE?=--verbose -.PHONY: all +.PHONY: all all: specs correctness proofs tests cosim +# Note that we don't include benchmarks in `all`, +# to avoid slowing down CI too much .PHONY: specs time -p $(LAKE) build Specs @@ -35,8 +37,12 @@ awslc_elf: cosim: time -p lake exe lnsym $(VERBOSE) --num-tests $(NUM_TESTS) +.PHONY: benchmarks +benchmarks: + $(LAKE) build Benchmarks + .PHONY: clean clean_all -clean: +clean: $(LAKE) clean clean_all: clean diff --git a/README.md b/README.md index 37b50e73..47939c18 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ # LNSym: Native Code Symbolic Simulator in Lean -[![Makefile CI](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml/badge.svg)](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml) +[![Makefile CI](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml/badge.svg)](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml) LNSym is a symbolic simulator for Armv8 machine-code programs. @@ -41,6 +41,8 @@ native-code programs of interest. `awslc_elf`: perform ELF loading tests for AWS-LC. +`benchmarks`: run benchmarks for the symbolic simulator. + ### Makefile variables that can be passed in at the command line `VERBOSE`: Verbose mode; prints disassembly of the instructions being diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean index 1b74546a..c18286be 100644 --- a/Tactics/Sym.lean +++ b/Tactics/Sym.lean @@ -439,7 +439,6 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do let goal ← subst goal hEqId trace[Tactic.sym] "performed subsitutition in:\n{goal}" - traceHeartbeats replaceMainGoal [goal] @@ -447,7 +446,6 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do -- added while symbolically evaluating to `simp` let msg := m!"aggregating (non-)effects" withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do - traceHeartbeats "pre" let goal? ← LNSymSimp (← getMainGoal) c.aggregateSimpCtx c.aggregateSimprocs replaceMainGoal goal?.toList diff --git a/Tactics/SymContext.lean b/Tactics/SymContext.lean index e672e47f..a105f855 100644 --- a/Tactics/SymContext.lean +++ b/Tactics/SymContext.lean @@ -242,12 +242,12 @@ def inferStatePrefixAndNumber : SymM Unit := do state_prefix := (state.get? 0).getD 's' |>.toString, currentStateNumber }) else - SymM.logWarning "\ - Expected state to be a single letter followed by a number, but found: - {state} + SymM.logWarning m!"\ +Expected state to be a single letter followed by a number, but found: + {state} - Falling back to the default numbering schema, - with `s1` as the first new intermediate state" +Falling back to the default numbering scheme, \ +with `s1` as the first new intermediate state" modifyThe SymContext ({ · with state_prefix := "s", currentStateNumber := 1 }) diff --git a/lakefile.lean b/lakefile.lean index 80f20126..7175ad63 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,6 +32,9 @@ lean_lib «Tactics» where lean_lib «Doc» where -- add library configuration options here +lean_lib «Benchmarks» where + -- add library configuration options here + @[default_target] lean_exe «lnsym» where root := `Main