From 0ec86ecdd25053acd26d2338b466017cb002d0ba Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 10 May 2024 17:05:23 +0100 Subject: [PATCH] feat: run temci with perf --- .../speedcenter-worker.sh | 10 +- .../speedcenter.exec.velcom.yaml | 318 ++++++++++++++++++ 2 files changed, 322 insertions(+), 6 deletions(-) create mode 100644 1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter.exec.velcom.yaml diff --git a/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-worker.sh b/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-worker.sh index afff3011ab6d..4b43805a359b 100644 --- a/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-worker.sh +++ b/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-worker.sh @@ -1,10 +1,8 @@ #!/usr/bin/env bash set -o xtrace -COMMIT_TO_BENCH=6639fae +TAG_TO_BENCH=run-2024-05-06--13-24-grosser-7950x3d -# -------- -COMMIT_PRETTY_NAME=$(git name-rev --name-only $COMMIT_TO_BENCH) EXPERIMENTDIR=$(pwd) echo "pwd: $EXPERIMENTDIR" @@ -26,7 +24,7 @@ fi echo "time: $TIME" $TIME -v echo "time" -COMMITS=("$COMMIT_TO_BENCH" "2024-borrowing-benchmarking-baseline-v4") +COMMITS=("$TAG_TO_BENCH" "2024-borrowing-benchmarking-baseline-v6") KINDS=("reuse" "noreuse") run_benchmark_for_kind() { @@ -125,12 +123,12 @@ run_temci_for_kind() { run() { for i in {0..1}; do - # curl -d "Start[MICROBENCHMARK-LOG-${KINDS[i]}]. run:$COMMIT_PRETTY_NAME. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 + curl -d "Start[MICROBENCHMARK-LOG-${KINDS[i]}]. run:$TAG_TO_BENCH. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 mkdir -p builds-speedcenter run_build_for_kind "${KINDS[i]}" run_benchmark_for_kind "${KINDS[i]}" run_temci_for_kind "${KINDS[i]}" - # curl -d "Done[MICROBENCHMARK-LOG-${KINDS[i]}]. run:$COMMIT_PRETTY_NAME. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 + curl -d "Done[MICROBENCHMARK-LOG-${KINDS[i]}]. run:$TAG_TO_BENCH. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 done; } diff --git a/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter.exec.velcom.yaml b/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter.exec.velcom.yaml new file mode 100644 index 000000000000..5a13b4fb402e --- /dev/null +++ b/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter.exec.velcom.yaml @@ -0,0 +1,318 @@ +- attributes: + description: stdlib + tags: [slow] + time: &time + # runner: time + # alternative config: use `perf stat` for extended properties + runner: perf_stat + perf_stat: + properties: ['wall-clock', 'task-clock', 'instructions', 'branches', 'branch-misses'] + # rusage_properties: ['maxrss'] + run_config: + <<: *time + cmd: | + bash -c 'set -eo pipefail; touch ../../src/Init/Prelude.lean; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=9999" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) 2>&1 | ./accumulate_profile.py' + max_runs: 2 + parse_output: true + # initialize stage2 cmake + warmup + build_config: + cmd: | + bash -c 'make -C ${BUILD:-../../build/release} stage2 -j$(nproc)' +- attributes: + description: stdlib size + tags: [deterministic, fast] + run_config: + cwd: ../../ + cmd: | + bash -c " + set -euxo pipefail && + echo -n 'lines: ' && + find src -name '*.lean' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 + echo -n 'bytes .olean: ' && + find ${BUILD:-build/release}/stage2/lib/lean -name '*.olean' -print0 | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 + echo -n 'lines C: ' && + find ${BUILD:-build/release}/stage2/lib/temp -name '*.c' -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 + echo -n 'lines C++: ' && + find src \( -name '*.h' -o -name '*.cpp' \) -print0 | wc -l --files0-from=- | tail -1 | cut -d' ' -f 1 && + echo -n 'max dynamic symbols: ' && + find ${BUILD:-build/release}/stage2/lib/lean -name '*.so' -exec bash -c 'nm --dynamic --defined-only {} | wc -l' \; | sort | head -n1 + " + max_runs: 1 + runner: output +- attributes: + description: libleanshared.so + tags: [deterministic, fast] + run_config: + cmd: | + set -eu + echo -n 'binary size: ' + wc -c ${BUILD:-../../build/release}/stage2/lib/lean/libleanshared.so | cut -d' ' -f 1 + max_runs: 1 + runner: output +- attributes: + description: import Lean + tags: [fast] + run_config: + <<: *time + cmd: lean ../../src/Lean.lean +- attributes: + description: tests/compiler + tags: [deterministic, slow] + run_config: + cwd: ../compiler/ + cmd: | + set -eu + printf 'sum binary sizes: ' + for f in *.lean; do ../bench/compile.sh $f; printf '%s\0' "$f.out"; done | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1 + max_runs: 1 + runner: output +- attributes: + description: tests/bench/ interpreted + tags: [slow] + run_config: + <<: *time + cmd: | + bash -c ' + set -euxo pipefail + ulimit -s unlimited + for f in *.args; do + lean --run ${f%.args} $(cat $f) + done + ' + max_runs: 5 +- attributes: + description: binarytrees + tags: [fast, suite] + run_config: + <<: *time + cmd: ./binarytrees.lean.out 21 + build_config: + cmd: ./compile.sh binarytrees.lean +- attributes: + description: binarytrees.st + tags: [fast, suite] + run_config: + <<: *time + cmd: ./binarytrees.st.lean.out 21 + build_config: + cmd: ./compile.sh binarytrees.st.lean +- attributes: + description: const_fold + tags: [fast, suite] + run_config: + <<: *time + cmd: bash -c "ulimit -s unlimited && ./const_fold.lean.out 23" + build_config: + cmd: ./compile.sh const_fold.lean +- attributes: + description: deriv + tags: [fast, suite] + run_config: + <<: *time + cmd: ./deriv.lean.out 10 + build_config: + cmd: ./compile.sh deriv.lean +- attributes: + description: lake build clean + tags: [slow] + run_config: + <<: *time + cmd: | + bash -c " + set -ex + ulimit -s unlimited + cd inundation + lake -flakefile-clean.lean clean + lake -flakefile-clean.lean build + " + build_config: + cmd: | + bash -c " + set -ex + ulimit -s unlimited + cd inundation + cp lakefile.lean lakefile-clean.lean + lake -flakefile-clean.lean -Ktest=Clean run mkBuild + lake -flakefile-clean.lean build + " +- attributes: + description: lake build no-op + tags: [fast] + run_config: + <<: *time + cmd: | + bash -c " + set -ex + ulimit -s unlimited + lake -dinundation -flakefile-nop.lean build + " + build_config: + cmd: | + bash -c " + set -ex + ulimit -s unlimited + cd inundation + cp lakefile.lean lakefile-nop.lean + lake -flakefile-nop.lean -Ktest=Nop run mkBuild + lake -flakefile-nop.lean build + " +- attributes: + description: lake config elab + tags: [fast] + run_config: + <<: *time + cmd: | + bash -c " + set -ex + ulimit -s unlimited + lake -dinundation -flakefile-rc.lean -R run nop + " + build_config: + cmd: cp inundation/lakefile.lean inundation/lakefile-rc.lean +- attributes: + description: lake config import + tags: [fast] + run_config: + <<: *time + cmd: | + bash -c " + set -ex + ulimit -s unlimited + lake -dinundation run nop + " + build_config: + cmd: | + bash -c " + set -ex + ulimit -s unlimited + lake -dinundation run nop + " +- attributes: + description: lake config tree + tags: [fast] + run_config: + <<: *time + cmd: | + bash -c " + set -ex + ulimit -s unlimited + lake -dinundation/test/tree run nop + " + build_config: + cmd: | + lake -dinundation run mkTree + lake -dinundation/test/tree update +- attributes: + description: lake env + tags: [fast] + run_config: + <<: *time + cmd: | + bash -c " + set -ex + ulimit -s unlimited + lake -dinundation env true + " + build_config: + cmd: lake -dinundation env true +- attributes: + description: lake startup + tags: [fast] + run_config: + <<: *time + cmd: | + bash -c " + set -ex + ulimit -s unlimited + lake self-check + " +- attributes: + description: language server startup + tags: [fast] + run_config: + <<: *time + cmd: lean -Dlinter.all=false --run server_startup.lean +- attributes: + description: liasolver + tags: [fast, suite] + run_config: + <<: *time + cmd: ./liasolver.lean.out ex-50-50-1.leq + build_config: + cmd: ./compile.sh liasolver.lean +- attributes: + description: parser + tags: [fast, suite] + run_config: + <<: *time + cmd: ./parser.lean.out ../../src/Init/Prelude.lean 50 + build_config: + cmd: ./compile.sh parser.lean +- attributes: + description: qsort + tags: [fast, suite] + run_config: + <<: *time + cmd: ./qsort.lean.out 400 + build_config: + cmd: ./compile.sh qsort.lean +- attributes: + description: rbmap + tags: [fast, suite] + run_config: + <<: *time + cmd: ./rbmap.lean.out 2000000 + build_config: + cmd: ./compile.sh rbmap.lean +- attributes: + description: rbmap_1 + tags: [fast, suite] + run_config: + <<: *time + cmd: ./rbmap_checkpoint.lean.out 2000000 1 + build_config: + cmd: ./compile.sh rbmap_checkpoint.lean +- attributes: + description: rbmap_10 + tags: [fast, suite] + run_config: + <<: *time + cmd: ./rbmap_checkpoint.lean.out 2000000 10 + build_config: + cmd: ./compile.sh rbmap_checkpoint.lean +- attributes: + description: rbmap_fbip + tags: [fast, suite] + run_config: + <<: *time + cmd: ./rbmap_fbip.lean.out 2000000 + build_config: + cmd: ./compile.sh rbmap_fbip.lean +- attributes: + description: rbmap_library + tags: [fast, suite] + run_config: + <<: *time + cmd: ./rbmap_library.lean.out 2000000 + build_config: + cmd: ./compile.sh rbmap_library.lean +- attributes: + description: reduceMatch + tags: [fast, suite] + run_config: + <<: *time + cmd: lean reduceMatch.lean +- attributes: + description: unionfind + tags: [fast, suite] + run_config: + <<: *time + cmd: ./unionfind.lean.out 3000000 + build_config: + cmd: ./compile.sh unionfind.lean +- attributes: + description: workspaceSymbols + tags: [fast, suite] + run_config: + <<: *time + cmd: lean workspaceSymbols.lean