From 1f41b912064e49979bfefa5874ea53cb25934a06 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 20 Jan 2023 12:45:37 +0100 Subject: [PATCH] test: update Lean variant benchmarks --- tests/bench/Makefile | 12 ++++---- tests/bench/disable-st.patch | 32 ------------------- tests/bench/flake.lock | 25 +++++++++++---- tests/bench/flake.nix | 60 ++++++++++++++++++++++++++---------- tests/bench/parser.lean | 8 +++++ tests/bench/report.py | 21 +++++++++---- 6 files changed, 91 insertions(+), 67 deletions(-) delete mode 100644 tests/bench/disable-st.patch create mode 100644 tests/bench/parser.lean diff --git a/tests/bench/Makefile b/tests/bench/Makefile index f2f0a6bcf1..45ce06d7f3 100644 --- a/tests/bench/Makefile +++ b/tests/bench/Makefile @@ -103,7 +103,7 @@ bench: bench/%.bench: %.out | bench ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS) -d $< "./$< $(BENCH_PARAMS)" --out $@ -bench/parser.%.bench: BENCH_PARAMS = $(PARSER_TEST_FILE) 100 +bench/parser.%.bench: BENCH_PARAMS = $(PARSER_TEST_FILE) 10 bench/binarytrees.%.bench: BENCH_PARAMS = 21 bench/binarytrees.ml.bench: BENCH_PARAMS = $$(nproc) 21 @@ -130,7 +130,7 @@ bench/unionfind.%.bench: BENCH_PARAMS = 3000000 bench/%gc.lean.bench: %lean.out | bench ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS)\ - -d $< "perf record -o $@.tmp ./$< $(BENCH_PARAMS) >/dev/null && perf report -i $@.tmp -t ';' --stdio -S 'lean_dec_ref_cold,lean_del_core,lean_free_small' | ./lean-gc.py"\ + -d $< "perf record -o $@.tmp ./$< $(BENCH_PARAMS) >/dev/null && perf report -i $@.tmp -t ';' --stdio -S 'lean_inc_ref_cold,lean_inc_ref_n_cold,lean_dec_ref_cold,lean_del_core,lean_free_small' | ./lean-gc.py"\ --runner output --out $@ bench/%gc.hs.bench: %hs.out | bench @@ -201,12 +201,12 @@ report: report/index.html # yes. space = $() $() -report_lean.csv: bench_lean - BENCHES=$(subst $(space),:,$(LEAN_BENCHES)) CATS=$(subst $(space),:,$(LEAN_CATS)) ./report.py > $@ +report_lean.csv report_lean_rbmap.csv: bench_lean + BENCHES=$(subst $(space),:,$(LEAN_BENCHES)) CATS=$(subst $(space),:,$(LEAN_CATS)) ./report.py report_lean column -s';' -t < $@ -report_cross.csv: bench_cross - BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py > $@ +report_cross.csv report_cross_rbmap.csv: bench_cross + BENCHES=$(subst $(space),:,$(CROSS_BENCHES)) CATS=$(subst $(space),:,$(CROSS_CATS)) ./report.py report_cross column -s';' -t < $@ TO_TEX = 's/-/---/g;s/%/\\%/g;s/\.$$//g;s/(\([0-9]\)\([0-9]\))/\\ensuremath{\\tilde{\1}\\tilde{\2}}/g;s/(\([0-9]\))/\\ensuremath{\\tilde{\1}}/g;s/;/ \& /g;s/$$/\\\\/' diff --git a/tests/bench/disable-st.patch b/tests/bench/disable-st.patch deleted file mode 100644 index f0e46b26e9..0000000000 --- a/tests/bench/disable-st.patch +++ /dev/null @@ -1,32 +0,0 @@ -From bebbd732ac64eefe841ec2da25a67c756dfa0f61 Mon Sep 17 00:00:00 2001 -From: Sebastian Ullrich -Date: Mon, 11 Nov 2019 18:15:21 +0100 -Subject: [PATCH] disable ST objects - ---- - src/include/lean/lean.h | 6 +++--- - 1 file changed, 3 insertions(+), 3 deletions(-) - -diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h -index 6b37fd91a..c53137860 100644 ---- a/src/include/lean/lean.h -+++ b/src/include/lean/lean.h -@@ -567,13 +567,13 @@ void lean_mark_persistent(lean_object * o); - - static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) { - #if defined(LEAN_COMPRESSED_OBJECT_HEADER) -- o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | (1ull << LEAN_ST_BIT) | 1; -+ o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | (1ull << LEAN_MT_BIT) | 1; - #elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) -- o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_ST_MEM_KIND << 40) | 1; -+ o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_MT_MEM_KIND << 40) | 1; - #else - o->m_rc = 1; - o->m_tag = tag; -- o->m_mem_kind = LEAN_ST_MEM_KIND; -+ o->m_mem_kind = LEAN_MT_MEM_KIND; - o->m_other = other; - #endif - } --- -2.23.0 diff --git a/tests/bench/flake.lock b/tests/bench/flake.lock index cb6d87b019..3513604b7e 100644 --- a/tests/bench/flake.lock +++ b/tests/bench/flake.lock @@ -1,5 +1,17 @@ { "nodes": { + "disable-st": { + "flake": false, + "locked": { + "narHash": "sha256-8Wlf9O+YRInYJdN9ydBGh5vaYAqESpZ4Kn0BvxivYog=", + "type": "file", + "url": "https://github.com/Kha/lean4/commit/no-st.patch" + }, + "original": { + "type": "file", + "url": "https://github.com/Kha/lean4/commit/no-st.patch" + } + }, "flake-utils": { "locked": { "lastModified": 1656928814, @@ -38,14 +50,14 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 0, - "narHash": "sha256-BfyPrBC8uxFmK08pnWd6+fSOl8MAct4mpi0rTypoyrU=", - "path": "/nix/store/y2cgjkc355yma96gjrai3lhbi18klgwx-source", - "type": "path" + "lastModified": 1674199151, + "narHash": "sha256-IASus2xsMhew5BIm54h1DOL57t/VS0/OszWUWTRfU9A=", + "type": "git", + "url": "file:../.." }, "original": { - "path": "/nix/store/y2cgjkc355yma96gjrai3lhbi18klgwx-source", - "type": "path" + "type": "git", + "url": "file:../.." } }, "lean4-mode": { @@ -182,6 +194,7 @@ }, "root": { "inputs": { + "disable-st": "disable-st", "flake-utils": [ "lean", "flake-utils" diff --git a/tests/bench/flake.nix b/tests/bench/flake.nix index 5c75033a6f..4bda95a7f2 100644 --- a/tests/bench/flake.nix +++ b/tests/bench/flake.nix @@ -1,9 +1,11 @@ { - inputs.lean.url = "../.."; + inputs.lean.url = "git+file:../.."; inputs.flake-utils.url = github:numtide/flake-utils; inputs.flake-utils.follows = "lean/flake-utils"; inputs.temci.url = github:Kha/temci; inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable; + inputs.disable-st.url = https://github.com/Kha/lean4/commit/no-st.patch; + inputs.disable-st.flake = false; outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system: { packages = rec { leanPkgs = inputs.lean.packages.${system}; @@ -40,22 +42,6 @@ src = ./.; LEAN_BIN = "${leanPkgs.lean-all}/bin"; #LEAN_GCC_BIN = "${lean { stdenv = pkgs.gcc9Stdenv; }}/bin"; - #LEAN_NO_REUSE_BIN = "${lean.overrideAttrs (attrs: { - # prePatch = '' - #substituteInPlace src/Lean/Compiler/IR.lean --replace "decls.map Decl.insertResetReuse" "decls" - # ''; - # buildFlags = [ "stage1.5" ]; - # installFlags = [ "-C stage1.5" ]; - #})}/bin"; - #LEAN_NO_BORROW_BIN = "${lean.overrideAttrs (attrs: { - # prePatch = '' - #substituteInPlace src/Lean/Compiler/IR.lean --replace "inferBorrow" "pure" - # ''; - # buildFlags = [ "stage1.5" ]; - # installFlags = [ "-C stage1.5" ]; - #})}/bin"; - #LEAN_NO_ST_BIN = "${lean.overrideAttrs (attrs: { patches = [ ./disable-st.patch ]; })}/bin"; - PARSER_TEST_FILE = ../../src/Init/Core.lean; GHC = "${ghc}/bin/ghc"; OCAML = "${ocaml}/bin/ocamlopt.opt"; #OCAML_FLAMBDA = "${ocamlFlambda}/bin/ocamlopt.opt"; @@ -80,5 +66,45 @@ cp -r report *.csv $out ''; }; + + lean-variants = pkgs.stdenv.mkDerivation rec { + name = "lean_bench"; + src = ./.; + LEAN_BIN = "${leanPkgs.lean-all}/bin"; + LEAN_NO_REUSE_BIN = "${(leanPkgs.override (args: { + src = pkgs.runCommand "lean-no-reuse-src" {} '' + cp -r ${args.src} $out + substituteInPlace $out/src/Lean/Compiler/IR.lean --replace "decls.map Decl.insertResetReuse" "decls" + ''; + })).stage2.lean-all}/bin"; + LEAN_NO_BORROW_BIN = "${(leanPkgs.override (args: { + src = pkgs.runCommand "lean-no-borrow-src" {} '' + cp -r ${args.src} $out + substituteInPlace $out/src/Lean/Compiler/IR.lean --replace "inferBorrow" "pure" + ''; + })).stage2.lean-all}/bin"; + LEAN_NO_ST_BIN = "${(leanPkgs.override (args: { + src = pkgs.runCommand "lean-no-st-src" {} '' + cp -r ${args.src} $out + chmod -R u+w $out + cd $out + patch -p1 < ${inputs.disable-st} + ''; + })).lean-all}/bin"; + PARSER_TEST_FILE = ../../src/Init/Prelude.lean; + buildInputs = with pkgs; [ + ((builtins.elemAt temci.nativeBuildInputs 0).withPackages (ps: [ temci ps.numpy ps.pyyaml ])) + temci + pkgs.linuxPackages.perf time unixtools.column + ]; + patchPhase = '' + patchShebangs . + ''; + makeFlags = [ "report_lean.csv" ]; + installPhase = '' + mkdir $out + cp -r report *.csv $out + ''; + }; };}); } diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean new file mode 100644 index 0000000000..de4a6ea7f5 --- /dev/null +++ b/tests/bench/parser.lean @@ -0,0 +1,8 @@ +import Lean.Parser.Module + +def main : List String → IO Unit +| [fname, n] => do + let env ← Lean.mkEmptyEnvironment + for _ in [0:n.toNat!] do + discard $ Lean.Parser.testParseFile env fname +| _ => throw $ IO.userError "give file" diff --git a/tests/bench/report.py b/tests/bench/report.py index 068a47a338..08897a7ba3 100755 --- a/tests/bench/report.py +++ b/tests/bench/report.py @@ -20,7 +20,10 @@ def single(bench, cat, prop): runs = yaml.load(f, Loader=yaml.CLoader) stats_helper = rundata.RunDataStatsHelper.init_from_dicts(runs) stat = stats.TestedPairsAndSingles(stats_helper.valid_runs()) - return stat.singles[0].properties[prop] + if stat.singles: + return stat.singles[0].properties[prop] + else: + raise Exception(f"failed to parse {f}") mean_by_cat = collections.defaultdict(list) stddev_by_cat = collections.defaultdict(list) @@ -71,10 +74,16 @@ CATBAG = { benches = os.environ['BENCHES'].split(':') cats = os.environ['CATS'].split(':') -print(";".join(["Benchmark"] + [f'{CATBAG[cat][0]};{CATBAG[cat][0]} std' for cat in cats])) -for bench in benches: - norm = single('rbmap' if bench.startswith('rbmap') else bench, '.lean', 'etime').mean() - print(";".join([bench] + [pp(bench, cat, CATBAG[cat][1], norm) for cat in cats])) +# create one file without rbmap_ benchmarks, one without only rbmap and normed by rbmap_1 +for sfx in ['', '_rbmap']: + f = open(sys.argv[1] + sfx + '.csv', 'w') + print(";".join(["Benchmark"] + [f'{CATBAG[cat][0]};{CATBAG[cat][0]} std' for cat in cats]), file=f) -print(";".join(["geom. mean"] + [mean(cat, CATBAG[cat][1]) for cat in cats])) + for bench in benches: + if sfx == '' and bench.startswith('rbmap_') or sfx == '_rbmap' and not bench.startswith('rbmap'): + continue + norm = single('rbmap_1' if bench.startswith('rbmap') and sfx == '_rbmap' else bench, '.lean', 'etime').mean() + print(";".join([bench] + [pp(bench, cat, CATBAG[cat][1], norm) for cat in cats]), file=f) + + print(";".join(["geom. mean"] + [mean(cat, CATBAG[cat][1]) for cat in cats]), file=f)