feat(tests/playground): Lean variant benchmarks
This commit is contained in:
Sebastian Ullrich
parent
5302a40763
commit
c1ba216bcc
3 changed files with 40 additions and 9 deletions
|
|
@ -1,11 +1,14 @@
|
|||
## CONFIG
|
||||
|
||||
LEAN_BENCHES = binarytrees deriv expr_const_folding qsort rbmap rbmap_checkpoint_10 rbmap_shared unionfind1 unionfind2
|
||||
CROSS_BENCHES = binarytrees deriv expr_const_folding qsort rbmap rbmap_checkpoint_10 rbmap_shared
|
||||
|
||||
LEAN_CATS = .lean .no_reuse.lean .no_borrow.lean .no_st.lean
|
||||
CROSS_CATS = .lean .gc.lean .lean.perf .hs .gc.hs .hs.perf .ml .gc.ml .ml.perf .mlton .gc.mlton .mlton.perf .mlkit .gc.mlkit .mlkit.perf
|
||||
TIME_CATS = .lean .hs .ml .mlton .mlkit
|
||||
RETIRED_CATS = .gcc.lean .llvm.hs .flambda.ml
|
||||
|
||||
LEAN_FLAGS =
|
||||
LEANC_FLAGS = -O3
|
||||
GHC_FLAGS = -O3
|
||||
OCAML_FLAGS = -O3
|
||||
|
|
@ -21,27 +24,36 @@ MLKIT ?= mlkit
|
|||
|
||||
## IMPLEMENTATION
|
||||
|
||||
LEAN_INPUTS = $(foreach bench,$(LEAN_BENCHES), $(foreach cat, $(LEAN_CATS), $(bench)$(cat)))
|
||||
CROSS_INPUTS = $(foreach bench,$(CROSS_BENCHES), $(foreach cat, $(CROSS_CATS), $(bench)$(cat)))
|
||||
|
||||
.SECONDARY: $(CROSS_INPUTS:%=%.out) $(CROSS_INPUTS:%=bench/%.bench)
|
||||
.SECONDARY: $(LEAN_INPUTS:%=%.out) $(LEAN_INPUTS:%=bench/%.bench) $(CROSS_INPUTS:%=%.out) $(CROSS_INPUTS:%=bench/%.bench)
|
||||
.DELETE_ON_ERROR:
|
||||
|
||||
all: reports report_cross.csv
|
||||
all: reports report_lean.csv report_cross.csv
|
||||
|
||||
# disable some built-in rules
|
||||
%.lean:
|
||||
%.out: %
|
||||
|
||||
%.lean.cpp: %.lean
|
||||
$(LEAN_BIN)/lean --cpp=$@ $<
|
||||
$(LEAN_BIN)/lean --cpp=$@ $(LEAN_FLAGS) $<
|
||||
%.lean.out: %.lean.cpp
|
||||
$(LEAN_BIN)/leanc $(LEANC_FLAGS) -o $@ $<
|
||||
frontend%lean.out:
|
||||
ln -f $(LEAN_BIN)/lean
|
||||
# Binaries x.lean.out and x.gcc.lean.out etc. are produced by the
|
||||
# same rules and x.lean source file by copying the latter to
|
||||
# x.gcc.lean. This also avoids conflicts between intermediate
|
||||
# files of the two binaries.
|
||||
%.gcc.lean.out: LEAN_BIN = $(LEAN_GCC_BIN)
|
||||
%.gcc.lean: %.lean; ln -f $< $@
|
||||
%.no_reuse.lean.out: LEAN_BIN = $(LEAN_NO_REUSE_BIN)
|
||||
%.no_reuse.lean: %.lean; ln -f $< $@
|
||||
%.no_borrow.lean.out: LEAN_BIN = $(LEAN_NO_BORROW_BIN)
|
||||
%.no_borrow.lean: %.lean; ln -f $< $@
|
||||
%.no_st.lean.out: LEAN_BIN = $(LEAN_NO_ST_BIN)
|
||||
%.no_st.lean: %.lean; ln -f $< $@
|
||||
|
||||
%.hs.out: %.hs
|
||||
$(GHC) $(GHC_FLAGS) -rtsopts $< -o $@
|
||||
|
|
@ -76,6 +88,8 @@ bench:
|
|||
bench/%.bench: %.out | bench
|
||||
ulimit -s unlimited && $(TEMCI) short exec -d $< "./$< $(BENCH_PARAMS)" --out $@
|
||||
|
||||
bench/frontend.%.bench: BENCH_PARAMS = --new-frontend ../../library/init/core.lean
|
||||
|
||||
bench/binarytrees.%.bench: BENCH_PARAMS = 21
|
||||
|
||||
bench/qsort.%.bench: BENCH_PARAMS = 250
|
||||
|
|
@ -88,6 +102,9 @@ bench/rbmap_shared.%.bench: BENCH_PARAMS = 500000 1
|
|||
rbmap_checkpoint_10.%.out: rbmap_checkpoint.%.out; ln -f $< $@
|
||||
bench/rbmap_checkpoint_10.%.bench: BENCH_PARAMS = 2000000 10
|
||||
|
||||
bench/unionfind1.%.bench: BENCH_PARAMS = 3000000
|
||||
bench/unionfind2.%.bench: BENCH_PARAMS = 3000000
|
||||
|
||||
bench/%gc.lean.bench: %lean.out | bench
|
||||
ulimit -s unlimited && $(TEMCI) short exec\
|
||||
-d $< "perf record -o $@.tmp ./$< $(BENCH_PARAMS) >/dev/null && perf report -i $@.tmp -t ';' --stdio -S 'lean::del,lean::dealloc' | ./lean-gc.py"\
|
||||
|
|
@ -127,6 +144,7 @@ bench/binarytrees%mlton.perf.bench: ; touch $@
|
|||
bench/binarytrees%mlkit.bench: ; touch $@
|
||||
bench/binarytrees%mlkit.perf.bench: ; touch $@
|
||||
|
||||
bench_lean: $(LEAN_INPUTS:%=bench/%.bench)
|
||||
bench_cross: $(CROSS_INPUTS:%=bench/%.bench)
|
||||
|
||||
report:
|
||||
|
|
@ -147,6 +165,9 @@ reports: $(foreach bench, $(CROSS_BENCHES), report/$(bench)) report/index.html
|
|||
# yes.
|
||||
space = $() $()
|
||||
|
||||
report_lean.csv: $(LEAN_INPUTS:%=bench/%.bench) report.py temci.yaml
|
||||
BENCHES=$(subst $(space),:,$(LEAN_BENCHES)) CATS=$(subst $(space),:,$(LEAN_CATS)) ./report.py > $@
|
||||
|
||||
report_cross.csv: $(CROSS_INPUTS:%=bench/%.bench) report.py temci.yaml
|
||||
BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@
|
||||
|
||||
|
|
|
|||
|
|
@ -1,12 +1,11 @@
|
|||
{ pkgs ? import ./nixpkgs.nix }:
|
||||
|
||||
let
|
||||
lean = { cmakeFlags ? "", stdenv ? pkgs.llvmPackages_7.stdenv }:
|
||||
lean = { stdenv ? pkgs.llvmPackages_7.stdenv }:
|
||||
(pkgs.callPackage ../../default.nix { inherit stdenv; }).overrideAttrs (attrs: {
|
||||
inherit cmakeFlags;
|
||||
# pin Lean commit to avoid rebuilds
|
||||
# 2019-05-24
|
||||
src = builtins.fetchGit { url = ../../.; rev = "074002eb847b6f4fbaf2484c928c86baadf66a42"; };
|
||||
# 2019-05-27
|
||||
src = builtins.fetchGit { url = ../../.; rev = "0e8abd81bba1b9c06ea7eab23001bbf08ff267dc"; };
|
||||
});
|
||||
# for binarytrees.hs
|
||||
ghcPackages = p: [ p.parallel ];
|
||||
|
|
@ -39,6 +38,15 @@ in pkgs.stdenv.mkDerivation rec {
|
|||
src = pkgs.lib.sourceFilesBySuffices ./. ["Makefile" "leanpkg.path" "temci.yaml" ".py" ".lean" ".hs" ".ml"];
|
||||
LEAN_BIN = "${lean {}}/bin";
|
||||
LEAN_GCC_BIN = "${lean { stdenv = pkgs.gcc9Stdenv; }}/bin";
|
||||
LEAN_NO_REUSE_BIN = "${(lean {}).overrideAttrs (attrs: { prePatch = ''
|
||||
substituteInPlace library/init/lean/compiler/ir/default.lean --replace "decls.map Decl.insertResetReuse" "decls"
|
||||
''; })}/bin";
|
||||
LEAN_NO_BORROW_BIN = "${(lean {}).overrideAttrs (attrs: { prePatch = ''
|
||||
substituteInPlace library/init/lean/compiler/ir/default.lean --replace "decls.map Decl.inferBorrow" "decls"
|
||||
''; })}/bin";
|
||||
LEAN_NO_ST_BIN = "${(lean {}).overrideAttrs (attrs: { prePatch = ''
|
||||
substituteInPlace src/runtime/object.h --replace "c_init_mem_kind = object_memory_kind::STHeap" "c_init_mem_kind = object_memory_kind::MTHeap"
|
||||
''; })}/bin";
|
||||
GHC = "${ghc}/bin/ghc";
|
||||
OCAML = "${ocaml}/bin/ocamlopt.opt";
|
||||
OCAML_FLAMBDA = "${ocamlFlambda}/bin/ocamlopt.opt";
|
||||
|
|
|
|||
|
|
@ -31,8 +31,7 @@ def pp(bench, cat, prop, norm):
|
|||
norm = norm if prop == 'etime' else 1
|
||||
mean_by_cat[cat].append(s.mean() / norm)
|
||||
stddev_by_cat[cat].append(s.std_dev() / norm)
|
||||
return number.fnumber(s.mean() / norm, abs_deviation=s.std_dev() / norm,
|
||||
min_decimal_places = 0 if cat in ['del', 'gc'] else None)
|
||||
return number.fnumber(s.mean() / norm, abs_deviation=s.std_dev() / norm)
|
||||
|
||||
def gmean(cat):
|
||||
mean = st.gmean(mean_by_cat[cat])
|
||||
|
|
@ -41,6 +40,9 @@ def gmean(cat):
|
|||
|
||||
CATBAG = {
|
||||
'.lean': ("Lean [s]", "etime"),
|
||||
'.no_reuse.lean': ("-reuse", "etime"),
|
||||
'.no_borrow.lean': ("-borrow", "etime"),
|
||||
'.no_st.lean': ("-ST", "etime"),
|
||||
'.gcc.lean': ("Lean+GCC9", "etime"),
|
||||
'.gc.lean': ("del [%]", "gc"),
|
||||
'.lean.perf': ("cache misses (CM) [1M/s]", "cache-misses"),
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue