feat: run temci with perf

opencompl · May 10, 2024 · 0ec86ec · 0ec86ec
1 parent cab211b
commit 0ec86ec
Show file tree

Hide file tree

Showing 2 changed files with 322 additions and 6 deletions.
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
@@ -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
@@ -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