fa40491c78
This PR adds a comparison between `MetaM` and `SymM` for a benchmark was
proposed during the Lean@Google Hackathon.
### Benchmark description
In this benchmark, we define the semantics of a very simple imperative
language using an inductive predicate
```
Exec prog events mem lctx post
```
The predicate holds if, when executing the program `prog` with an
initial list of events `events`, memory `mem`, and local context `lctx`,
the postcondition `post` holds.
We then consider the following program:
```
input b
a := b
a := a + a
a := a - b
...
a := a + a
a := a - b
```
That is, after reading an input value `b`, the program repeatedly
updates the variable `a` by doubling it and then subtracting `b`.
We prove that, for any initial memory `m` and local context `l`, and
starting from the empty list of events, the following postcondition
holds:
```
fun t' m' l' =>
m' = m ∧ -- memory did not change
∃ v : Word,
t' = [IOEvent.IN v] ∧ -- exactly one input event
l'.get "a" = some v -- `a` contains the input value
```
In other words, executing the program produces exactly one input event,
leaves the memory unchanged, and ensures that the final value of `a` is
equal to the input value.
### Symbolic simulation benchmark (problem size `n`, with `2·n + 2`
instructions)
| Problem size (n) | MetaM time (ms) | MetaM kernel (ms) | SymM time
(ms) | SymM kernel (ms) | Total speedup |
|------------------|------------------|-------------------|----------------|------------------|---------------|
| 10 | 94.83 | 6.60 | 7.04 | 6.18 | ~13.5× |
| 20 | 218.92 | 13.33 | 14.15 | 13.02 | ~15.5× |
| 30 | 375.10 | 22.95 | 26.51 | 19.81 | ~14.2× |
| 40 | 563.82 | 34.99 | 40.42 | 29.55 | ~14.0× |
| 50 | 815.89 | 53.78 | 60.84 | 42.25 | ~13.4× |
| 60 | 1081.09 | 73.46 | 80.99 | 53.52 | ~13.3× |
| 70 | 1400.80 | 102.70 | 106.02 | 68.61 | ~13.2× |
| 80 | 1772.19 | 126.65 | 134.23 | 87.64 | ~13.2× |
| 90 | 2203.41 | 161.68 | 168.26 | 115.52 | ~13.1× |
| 100 | 2474.09 | 191.23 | 209.13 | 143.86 | ~11.8× |
<img width="580" height="455" alt="image"
src="https://github.com/user-attachments/assets/bc7058fa-e71a-4c2c-be28-860f39166965"
/>
### Symbolic simulation with extra simplification (SymM)
Problem size `n` corresponds to a program with `2·n + 2` instructions.
| n | Total time (ms) | Kernel time (ms) | Non-kernel time (ms) |
|-----|------------------|------------------|----------------------|
| 10 | 6.33 | 3.97 | 2.36 |
| 20 | 10.30 | 5.59 | 4.71 |
| 30 | 13.72 | 7.38 | 6.34 |
| 40 | 17.85 | 8.84 | 9.01 |
| 50 | 21.90 | 10.63 | 11.27 |
| 60 | 27.00 | 12.56 | 14.44 |
| 70 | 32.02 | 14.04 | 17.98 |
| 80 | 37.25 | 15.76 | 21.49 |
| 90 | 42.55 | 17.95 | 24.60 |
| 100 | 49.30 | 20.03 | 29.27 |
| 200 | 125.56 | 38.21 | 87.36 |
| 300 | 293.58 | 66.79 | 226.79 |
| 400 | 361.87 | 78.96 | 282.91 |
| 500 | 518.51 | 102.51 | 416.00 |
| 600 | 716.63 | 122.81 | 593.82 |
|
||
|---|---|---|
| .. | ||
| inundation | ||
| mergeSort | ||
| qsort | ||
| sym | ||
| .gitignore | ||
| accumulate_profile.py | ||
| arith_eval.ml | ||
| big_beq.lean | ||
| big_beq_rec.lean | ||
| big_deceq.lean | ||
| big_deceq_rec.lean | ||
| big_do.lean | ||
| big_match.lean | ||
| big_match_nat.lean | ||
| big_match_nat_split.lean | ||
| big_match_partial.lean | ||
| big_omega.lean | ||
| big_struct.lean | ||
| big_struct_dep.lean | ||
| binarytrees.ghc-6.hs | ||
| binarytrees.lean | ||
| binarytrees.lean.args | ||
| binarytrees.lean.expected.out | ||
| binarytrees.ocaml-2.ml | ||
| binarytrees.st.hs | ||
| binarytrees.st.lean | ||
| binarytrees.st.mlton-2.sml | ||
| binarytrees.st.sml | ||
| binarytrees.st.swift | ||
| binarytrees.swift | ||
| binarytrees5.ml | ||
| binarytrees5_multicore.ml | ||
| bv_decide_inequality.lean | ||
| bv_decide_large_aig.lean | ||
| bv_decide_mod.lean | ||
| bv_decide_mul.lean | ||
| bv_decide_realworld.lean | ||
| bv_decide_rewriter.lean | ||
| channel.lean | ||
| charactersIn.lean | ||
| compile.sh | ||
| const_fold.hs | ||
| const_fold.lean | ||
| const_fold.lean.args | ||
| const_fold.lean.expected.out | ||
| const_fold.ml | ||
| const_fold.sml | ||
| const_fold.swift | ||
| cross.yaml | ||
| dag_hassorry_issue.lean | ||
| dag_hassorry_issue.lean.args | ||
| dag_hassorry_issue.lean.expected.out | ||
| deriv.hs | ||
| deriv.lean | ||
| deriv.lean.args | ||
| deriv.lean.expected.out | ||
| deriv.ml | ||
| deriv.sml | ||
| deriv.swift | ||
| ex-50-50-1.leq | ||
| flake.lock | ||
| flake.nix | ||
| full-stdlib.exec.yaml | ||
| ghc-gc.py | ||
| hashmap.lean | ||
| identifier_completion.lean | ||
| identifier_completion_didOpen.log | ||
| identifier_completion_initialization.log | ||
| identifier_completion_runner.lean | ||
| ilean_roundtrip.lean | ||
| iterators.lean | ||
| lean-gc.py | ||
| liasolver.lean | ||
| liasolver.lean.args | ||
| liasolver.lean.expected.out | ||
| Makefile | ||
| mlkit-gc.py | ||
| mut_rec_wf.lean | ||
| nat_repr.lean | ||
| nat_repr.lean.args | ||
| nat_repr.lean.expected.out | ||
| ocaml-gc.py | ||
| omega_stress.lean | ||
| parser.lean | ||
| perf.py | ||
| phashmap.lean | ||
| qsort.hs | ||
| qsort.lean | ||
| qsort.lean.args | ||
| qsort.lean.expected.out | ||
| qsort.ml | ||
| qsort.sml | ||
| qsort.swift | ||
| rbmap.hs | ||
| rbmap.lean | ||
| rbmap.lean.args | ||
| rbmap.lean.expected.out | ||
| rbmap.ml | ||
| rbmap.sml | ||
| rbmap.swift | ||
| rbmap2.lean | ||
| rbmap3.lean | ||
| rbmap500k.lean | ||
| rbmap_checkpoint.hs | ||
| rbmap_checkpoint.lean | ||
| rbmap_checkpoint.lean.args | ||
| rbmap_checkpoint.lean.expected.out | ||
| rbmap_checkpoint.ml | ||
| rbmap_checkpoint.sml | ||
| rbmap_checkpoint.swift | ||
| rbmap_checkpoint2.lean | ||
| rbmap_checkpoint2.sml | ||
| rbmap_checkpoint_cpp_lean3.cpp | ||
| rbmap_checkpoint_cpp_std.cpp | ||
| rbmap_cpp_lean3.cpp | ||
| rbmap_cpp_std.cpp | ||
| rbmap_fbip.lean | ||
| rbmap_library.lean | ||
| README.md | ||
| reduceMatch.lean | ||
| report.py | ||
| riscv-ast.lean | ||
| run.sh | ||
| server_startup.lean | ||
| server_startup.log | ||
| sigmaIterator.lean | ||
| simp_arith1.lean | ||
| simp_bubblesort_256.lean | ||
| simp_congr.lean | ||
| simp_local.lean | ||
| simp_subexpr.lean | ||
| speedcenter.exec.velcom.yaml | ||
| speedcenter.yaml | ||
| states35.lean | ||
| test_single.sh | ||
| treemap.lean | ||
| unionfind.lean | ||
| unionfind.lean.args | ||
| unionfind.lean.expected.out | ||
| unionfind_clean.lean | ||
| watchdogRss.lean | ||
| workspaceSymbols.lean | ||
| workspaceSymbolsNewRanges.lean | ||
Lean Benchmark Suites
This folder contains multiple small Lean programs for benchmarking used by two separate benchmark suites based on the temci benchmarking tool:
- The light-weight "Speedcenter" suite benchmarks the current build of Lean. It can be used for quick comparisons on the cmdline and powers the Lean Speedcenter website.
- The heavy-weight "Cross" suite benchmarks multiple Lean configurations and other functional compilers against each other and generates CSV and HTML reports from that. It was created for the paper "Counting Immutable Beans - Reference Counting Optimized for Purely Functional Programming" (IFL19).
Speedcenter Suite
Requirements:
- A local Lean build in
../../build/release. Build at least thebintarget. - temci. Using Nix, open a nix-shell in the project
root directory to add a compatible version to your PATH. Alternatively, try
pip3 install git+https://github.com/parttimenerd/temci.git.
To execute the suite and save the results in base.yaml, run (in this folder)
temci exec --config speedcenter.yaml --out base.yaml
Other interesting exec flags:
- use
--runs Nto modify the default number of 10 runs per benchmark - use
--included_blocks fastto excluded slow benchmarks like the stdlib benchmark. You can replacefastwith any benchmark name or label inspeedcenter.exec.yaml.
If you have multiple saved result files, you can compare them with
temci report --config speedcenter.yaml report1.yaml report2.yaml ...
Cross Suite
We recommend using Nix for building/obtaining all Lean variants and used compilers in a reproducible way. After installing Nix, running the benchmarks is as easy as
nix develop
make
This will record 50 runs for each benchmark configuration (this can be changed with runs in cross.yaml),
generate results in report_lean.csv and report_cross.csv, and print them to stdout in a tabulated format.
It will also generate HTML reports in report/ comparing the time-based benchmarks.
In order to reduce noise in the benchmarking data, you may instead want to try calling make inside a
temci shell:
temci short shell --sudo --preset usable --cpuset_active make
Using root powers, this will temporarily configure your machine similarly to the LLVM benchmarking recommendations and move all your other processes to a single CPU core.