diff --git a/tests/playground/Makefile b/tests/playground/Makefile index e1b98ccc98..edd295622b 100644 --- a/tests/playground/Makefile +++ b/tests/playground/Makefile @@ -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 > $@ diff --git a/tests/playground/bench.nix b/tests/playground/bench.nix index 2223514398..2550d87ba4 100644 --- a/tests/playground/bench.nix +++ b/tests/playground/bench.nix @@ -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"; diff --git a/tests/playground/report.py b/tests/playground/report.py index 34692524b2..7d3c5b4ade 100755 --- a/tests/playground/report.py +++ b/tests/playground/report.py @@ -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"),