diff --git a/1-runs/1-SKELETON/run-lean-stage-bench-worker.sh b/1-runs/1-SKELETON/run-lean-stage-bench-worker.sh
deleted file mode 100644
index b66be76b84bc..000000000000
--- a/1-runs/1-SKELETON/run-lean-stage-bench-worker.sh
+++ /dev/null
@@ -1,248 +0,0 @@
-#!/usr/bin/env bash
-set -o xtrace
-set -e
-
-# HERE BE DRAGONS!
-# ~~~~~~~~~~~~~~~~~
-# Manually changed things:
-# Need to set options "hardcoded" in stage0 CmakeLists, because
-# for whatever reason, it does not carry over options:
-# So for now, I manually set PROFILE_PATH=/tmp/profile.csv and RUNTIME_STATS=ON.
-# This should be improved in the next iteration of this benchmark script.
-# # Furthermore, the Lean build system is even more schizo: It seems to want these options
-# # set in `src/CMakeLists.txt`.
-# # In an abundance of caution, I also set them in `stage0/src/CMakeLists.txt`. I am
-# # not sure this is necessary, but it's totally opaque to me how options get forwarded.
-
-COMMIT_TO_BENCH="2024-04-01---22-10-tcg40"
-
-if [[  $PWD  != *$COMMIT_TO_BENCH* ]]; then
-  echo "The commit to bench '${COMMIT_TO_BENCH}' is not contained in PWD '${PWD}'."
-  read -p "Do you want to proceed? (y/n)" -n 1 -r
-  echo    # Move to a new line
-  if [[ $REPLY =~ ^[Yy]$ ]]; then
-    echo "Proceeding to run..."
-  else
-    echo "Run aborted."
-    exit 1
-  fi
-fi
-
-# --------
-
-EXPERIMENTDIR=$(pwd)
-echo "pwd: $EXPERIMENTDIR"
-DATE=$(date)
-echo "date: $DATE"
-MACHINE=$(uname -a)
-echo "machine: $MACHINE"
-echo "git status: $(git status --short)"
-echo "git commit: $(git rev-parse HEAD)"
-ROOT=$(git rev-parse --show-toplevel)
-echo "root folder: $ROOT"
-echo "out folder: $OUTFOLDER"
-
-if [ "$(uname -s)" = "Darwin" ]; then
-    TIME="gtime"
-else
-    TIME="command time"
-fi
-echo "time: $TIME"
-$TIME -v echo "time"
-
-COMMITS=("$COMMIT_TO_BENCH" "2024-borrowing-benching-baseline" )
-KINDS=("reuse" "noreuse")
-
-
-ntfysh() {
-  curl -d "$1" ntfy.sh/xISSztEV8EoOchM2
-}
-
-clone_baseline() {
-  ntfysh "started cloning baseline"
-  mkdir -p "$EXPERIMENTDIR/builds/"
-
-  if [ ! -d "${EXPERIMENTDIR}/builds/baseline-src-code" ]; then
-    git clone git@github.com:opencompl/lean4.git \
-      --depth 1 \
-      --branch 2024-borrowing-benching-baseline \
-      "$EXPERIMENTDIR/builds/baseline-src-code"
-  fi
-  ntfysh "done cloning baseline"
-}
-
-
-clone_repo() {
-  local kind="$1"
-  ntfysh "started cloning repo $kind"
-
-  mkdir -p "$EXPERIMENTDIR/builds/"
-  if [ ! -d "${EXPERIMENTDIR}/builds/${kind}" ]; then
-    git clone git@github.com:opencompl/lean4.git  \
-      --depth 1 \
-      --branch "${COMMITS[i]}" "$EXPERIMENTDIR/builds/${kind}" \
-      --reference /anfs/bigdisc/sb2743/24-borrowing/lean4.reference
-  fi
-  ntfysh "done cloning repo $kind"
-}
-
-build_stage0() {
-  local kind="$1"
-  ntfysh "starting stage0 $kind"
-
-  if [ ! -f "${EXPERIMENTDIR}/builds/${kind}/build/release/stage0/bin/lean" ]; then
-    mkdir -p "$EXPERIMENTDIR/builds/${kind}/build/release/"
-    cd "$EXPERIMENTDIR/builds/${kind}/build/release/"
-    # output log name from stage3 build.
-
-    cmake ../../ \
-      -DCCACHE=OFF \
-      -DRUNTIME_STATS=ON \
-      -DCMAKE_BUILD_TYPE=Release \
-      -DLEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH="$EXPERIMENTDIR/builds/${kind}/build/release/profile.csv"
-    make update-stage0 -j20
-    rm -rf ../../src/; cp -r "$EXPERIMENTDIR/builds/baseline-src-code/src" ../../
-    cd ../../; rm -rf build; mkdir -p build/release; cd build/release
-    git checkout -- ../../src/runtime ../../src/include/lean/lean.h ../../src/library/compiler/ir_interpreter.h
-    # TODO: replace LEAN_PROFILER_... with /tmp/profile.csv (hardcoded).
-    cmake ../../ \
-      -DCCACHE=OFF \
-      -DRUNTIME_STATS=ON \
-      -DCMAKE_BUILD_TYPE=Release \
-      -DLEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH="/tmp/profile.csv"
-  fi
-  ntfysh "done stage0 $kind"
-}
-
-build_stage1() {
-  ntfysh "starting stage1 $kind"
-  local kind="$1"
-  if [ ! -f "${EXPERIMENTDIR}/builds/${kind}/build/release/stage1/bin/lean" ]; then
-    cd "$EXPERIMENTDIR/builds/${kind}/build/release/"
-    make -j20 stage1
-  fi
-  ntfysh "done stage1 $kind"
-}
-
-build_stage2() {
-  ntfysh "starting stage2 $kind"
-  local kind="$1"
-  if [ ! -f "${EXPERIMENTDIR}/builds/${kind}/build/release/stage2/bin/lean" ]; then
-    cd "$EXPERIMENTDIR/builds/${kind}/build/release/"
-    make -j20 stage2
-  fi
-  ntfysh "done stage2 $kind"
-}
-
-build_stage3() {
-  ntfysh "starting stage3 $kind"
-  local kind="$1"
-  mkdir -p "$EXPERIMENTDIR/outputs"
-  if [ ! -f "${EXPERIMENTDIR}/outputs/${kind}.stage3-compile-profile.csv" ]; then
-    cd "$EXPERIMENTDIR/builds/${kind}/build/release/"
-    make -j40 stage2 # just to check that stage2 is completed.
-    rm "/tmp/profile.csv" || true
-    $TIME -v make -j4 stage3 2>&1 | tee "$EXPERIMENTDIR/outputs/time-${kind}-stage3.txt"
-    cp "/tmp/profile.csv" "$EXPERIMENTDIR/outputs/${kind}.stage3-compile-profile.csv"
-  fi
-  ntfysh "done stage3 $kind"
-}
-
-build_stage1_stdlib() {
-  ntfysh "starting stage1 stdlib $kind"
-  local kind="$1"
-  mkdir -p "$EXPERIMENTDIR/outputs"
-
-  if [ ! -f "${EXPERIMENTDIR}/outputs/${kind}-stdlib-compile-profile.csv" ]; then
-    cd "$EXPERIMENTDIR/builds/${kind}"
-    rm -rf build/release || true
-    mkdir -p build/release
-    cd build/release
-    cmake ../../ -DCCACHE=OFF -DRUNTIME_STATS=ON -DCMAKE_BUILD_TYPE=Release -DLEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH="/tmp/profile.csv"
-    make -j40 stage1 # build stage1
-    touch ../../src/Init/Prelude.lean # touch stdlib
-    make -j40 stage0 # rebuild stage0
-
-    rm "/tmp/profile.csv" || true
-    mkdir -p "$EXPERIMENTDIR/outputs/"
-    $TIME -v make -j4 stage1 2>&1 | tee "$EXPERIMENTDIR/outputs/time-${kind}-stdlib.txt" # bench build stage1
-    cp "/tmp/profile.csv" "$EXPERIMENTDIR/outputs/${kind}-stdlib-compile-profile.csv" # save script.
-  fi
-  ntfysh "done stage1 stdlib $kind"
-}
-
-
-clone_baseline
-
-for i in {0..1}; do
-  clone_repo "${KINDS[i]}"
-done;
-
-
-# for i in {0..1}; do
-#   build_stage0 "${KINDS[i]}"
-# done;
-#
-# for i in {0..1}; do
-#   build_stage1 "${KINDS[i]}"
-# done;
-#
-# for i in {0..1}; do
-#   build_stage2 "${KINDS[i]}"
-# done;
-#
-# for i in {0..1}; do
-#   build_stage3 "${KINDS[i]}"
-# done;
-
-
-for i in {0..1}; do
-  build_stage1_stdlib "${KINDS[i]}"
-done;
-
-
-
-
-
-
-
-
-#   echo "@@@ ${KINDS[i]} BUILD @@@"
-#   curl -d "Started[Stage3-Bench-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)."  ntfy.sh/xISSztEV8EoOchM2
-#   mkdir -p "$EXPERIMENTDIR/builds/"
-#   if [ ! -d "${EXPERIMENTDIR}/builds/${KINDS[i]}" ]; then
-#     git clone git@github.com:opencompl/lean4.git  \
-#       --depth 1 \
-#       --branch "${COMMITS[i]}" "$EXPERIMENTDIR/builds/${KINDS[i]}" \
-#       --reference /anfs/bigdisc/sb2743/24-borrowing/lean4.reference
-#   fi
-#
-#   CSVNAME="${KINDS[i]}.stage3.csv"
-#
-#   if [ ! -f "${EXPERIMENTDIR}/builds/${KINDS[i]}/build/release/stage2/bin/lean" ]; then
-#     mkdir -p "$EXPERIMENTDIR/builds/${KINDS[i]}/build/release/"
-#     cd "$EXPERIMENTDIR/builds/${KINDS[i]}/build/release/"
-#     # output log name from stage3 build.
-#
-#     cmake ../../ \
-#       -DCCACHE=OFF \
-#       -DRUNTIME_STATS=ON \
-#       -DCMAKE_BUILD_TYPE=Release \
-#       -DLEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH="$EXPERIMENTDIR/$CSVNAME"
-#     make update-stage0
-#     rm -rf ../../src/; cp -r "$EXPERIMENTDIR/builds/baseline-src-code/src" ../../
-#     git checkout -- ../../src/runtime ../../src/include/lean/lean.h ../../src/library/compiler/ir_interpreter.h
-#     make -j10 stage2
-#   fi
-#
-#   if [ ! -f "${EXPERIMENTDIR}/outputs/${KINDS[i]}.stage3.compile.csv" ]; then
-#     $TIME -v make -j10 stage3 2>&1 | tee "$EXPERIMENTDIR/time-${KINDS[i]}-stage3.txt"
-#     mv "${EXPERIMENTDIR}/$CSVNAME" "$EXPERIMENTDIR/outputs/${KINDS[i]}.stage3-compile.csv"
-#   fi
-#   curl -d "Done[STAGE3-BENCH-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)."  ntfy.sh/xISSztEV8EoOchM2
-# done;
-#
-#   # if [ ! -f "${EXPERIMENTDIR}/outputs/ctest-${KINDS[i]}-stage3.txt ]; then
-#   #   (cd $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/stage3 && (ctest -E handleLocking -j32 --output-on-failure 2>&1 | tee "$EXPERIMENTDIR/ctest-${KINDS[i]}-stage3.txt")) || true
-#   #   mv
-#   # fi
diff --git a/1-runs/1-SKELETON/run-lean-stage-bench-wrapper.sh b/1-runs/1-SKELETON/run-lean-stage-bench-wrapper.sh
deleted file mode 100755
index 1649ba0d8833..000000000000
--- a/1-runs/1-SKELETON/run-lean-stage-bench-wrapper.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-bash run-lean-stage-bench-worker.sh 2>&1 | tee log.txt
-
diff --git a/1-runs/1-SKELETON/speedcenter-worker.sh b/1-runs/1-SKELETON/speedcenter-worker.sh
index 083b830c08c1..ec3e9f5deec6 100644
--- a/1-runs/1-SKELETON/speedcenter-worker.sh
+++ b/1-runs/1-SKELETON/speedcenter-worker.sh
@@ -111,14 +111,15 @@ run_temci_for_kind() {
     elan toolchain link "$LEAN_TOOLCHAIN" "$EXPERIMENTDIR/builds-speedcenter/$kind/build/release/stage2"
     cd "$EXPERIMENTDIR/builds-speedcenter/$kind/tests/bench/" || exit 1
     elan override set "$LEAN_TOOLCHAIN" # set override for temci
-    temci exec --config speedcenter.yaml --out "$outfile_temp" --included_blocks suite # run temci
+    # taskset is preserved across child PIDs: https://stackoverflow.com/a/42941343
+    taskset -c0  temci exec --config speedcenter.yaml --out "$outfile_temp" --included_blocks suite # run temci
     mkdir -p "$EXPERIMENTDIR/outputs/"
     mv "$outfile_temp" "$outfile"
   fi
   local temci_report_outfile="$EXPERIMENTDIR/outputs/temci-report.txt"
   if [ ! -f "${temci_report_outfile}" ]; then
-    temci report "$EXPERIMENTDIR/outputs${KINDS[0]}.speedcenter.bench.yaml" \
-      "$EXPERIMENTDIR/outputs${KINDS[1]}.speedcenter.bench.yaml" > "$temci_report_outfile"
+    temci report "$EXPERIMENTDIR/outputs/${KINDS[0]}.speedcenter.bench.yaml" \
+      "$EXPERIMENTDIR/outputs/${KINDS[1]}.speedcenter.bench.yaml" > "$temci_report_outfile"
   fi
 }
 
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
new file mode 100644
index 000000000000..afff3011ab6d
--- /dev/null
+++ b/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-worker.sh
@@ -0,0 +1,137 @@
+#!/usr/bin/env bash
+set -o xtrace
+
+COMMIT_TO_BENCH=6639fae
+
+# --------
+COMMIT_PRETTY_NAME=$(git name-rev --name-only $COMMIT_TO_BENCH)
+
+EXPERIMENTDIR=$(pwd)
+echo "pwd: $EXPERIMENTDIR"
+DATE=$(date)
+echo "date: $DATE"
+MACHINE=$(uname -a)
+echo "machine: $MACHINE"
+echo "git status: $(git status --short)"
+echo "git commit: $(git rev-parse HEAD)"
+ROOT=$(git rev-parse --show-toplevel)
+echo "root folder: $ROOT"
+echo "out folder: $OUTFOLDER"
+
+if [ "$(uname -s)" = "Darwin" ]; then
+    TIME="gtime"
+else
+    TIME="command time"
+fi
+echo "time: $TIME"
+$TIME -v echo "time"
+
+COMMITS=("$COMMIT_TO_BENCH" "2024-borrowing-benchmarking-baseline-v4")
+KINDS=("reuse" "noreuse")
+
+run_benchmark_for_kind() {
+  # argument: kind
+  local kind="$1"
+  local BENCHMARKS=(
+    "rbmap_checkpoint.lean" "2000000 1"
+    "binarytrees.lean" "21"
+    "const_fold.lean" "21"
+    "deriv.lean" "10"
+    "liasolver.lean" ex-50-50-1.leq
+    # "parser.lean"
+    "qsort.lean" "400"
+    #"rbmap_checkpoint.lean" "2000000 1"
+    "rbmap_fbip.lean" "2000000"
+    "rbmap.lean" "2000000"
+    "unionfind.lean" "3000000")
+  local nruns=5
+  local outfile="$EXPERIMENTDIR/outputs/benchmarks-allocator-log-$kind.csv"
+  local outfile_temp="$outfile.temp"
+  rm "$outfile_temp" || true
+  if [ ! -f "${outfile}" ]; then
+    # link lean tooolchain
+    # # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/elan.20toolchain.20link.3A.20three.20hyphens.20becomes.20colon.3F/near/430447189
+    # # Lean toolchain does not like having three dash, so for now, just name it based on KINDS.
+    LEAN_TOOLCHAIN="$kind"
+
+    # TODO: elan does not like '---' in folder name?
+    elan toolchain link "$LEAN_TOOLCHAIN" "$EXPERIMENTDIR/builds-speedcenter/$kind/build/release/stage2"
+    cd "$EXPERIMENTDIR/builds-speedcenter/$kind/tests/bench/" || exit 1
+    elan override set "$LEAN_TOOLCHAIN" # set override for temci
+    mkdir -p "$EXPERIMENTDIR/outputs/"
+    for ((ix=0; ix<${#BENCHMARKS[@]}; ix+=2)); do
+      benchmark=${BENCHMARKS[ix]}
+      benchmark_input=${BENCHMARKS[ix+1]}
+      ./compile.sh "${benchmark}"
+      for _irun in $(seq 1 $nruns); do
+        RESEARCH_LEAN_RUNTIME_ALLOCATOR_LOG=./log.txt ./"${benchmark}.out" "${benchmark_input}"
+        while read -r line; do echo "$benchmark,$line"; done < log.txt >> "$outfile_temp"
+      done;
+    done;
+    mv "$outfile_temp" "$outfile"
+  fi
+}
+
+run_build_for_kind() {
+  local kind="$1"
+  mkdir -p "${EXPERIMENTDIR}/builds-speedcenter"
+  if [ ! -d "${EXPERIMENTDIR}/builds-speedcenter/${KINDS[i]}" ]; then
+    git clone --depth 1 https://github.com/opencompl/lean4.git --branch "${COMMITS[i]}" "$EXPERIMENTDIR/builds-speedcenter/${KINDS[i]}"
+  fi
+  # build
+  mkdir -p "$EXPERIMENTDIR/builds-speedcenter/$kind/build/release/"
+  cd "$EXPERIMENTDIR/builds-speedcenter/$kind/build/release/" || exit 1
+  # build stage2, with ccache, since we are only interested in benching the microbenchmarks
+  if [ ! -f "${EXPERIMENTDIR}/builds-speedcenter/$kind/build/release/stage2/bin/lean" ]; then
+    cmake ../../ -DCCACHE=ON -DRUNTIME_STATS=ON -DCMAKE_BUILD_TYPE=Release
+    make -j4 stage2
+  fi
+}
+
+run_ctest_for_kind() {
+  # run ctest to make sure our toolchain is legit.
+  local kind="$1"
+  mkdir -p "$EXPERIMENTDIR/outputs/"
+  cd "$EXPERIMENTDIR/builds-speedcenter/$kind/build/release/stage2" && \
+    (ctest -E handleLocking -j32 --output-on-failure 2>&1 | tee "$EXPERIMENTDIR/outputs/ctest-speedcenter-$kind-stage2.txt")
+}
+
+run_temci_for_kind() {
+  local kind="$1"
+  local outfile="$EXPERIMENTDIR/outputs/${KINDS[i]}.speedcenter.bench.yaml"
+  local outfile_temp="$outfile.temp"
+  rm "$outfile_temp" || true
+  if [ ! -f "${outfile}" ]; then
+    # link lean tooolchain
+    # # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/elan.20toolchain.20link.3A.20three.20hyphens.20becomes.20colon.3F/near/430447189
+    # # Lean toolchain does not like having three dash, so for now, just name it based on KINDS.
+    LEAN_TOOLCHAIN="$kind"
+
+    # TODO: elan does not like '---' in folder name?
+    elan toolchain link "$LEAN_TOOLCHAIN" "$EXPERIMENTDIR/builds-speedcenter/$kind/build/release/stage2"
+    cd "$EXPERIMENTDIR/builds-speedcenter/$kind/tests/bench/" || exit 1
+    elan override set "$LEAN_TOOLCHAIN" # set override for temci
+    # taskset is preserved across child PIDs: https://stackoverflow.com/a/42941343
+    taskset -c0  temci exec --config speedcenter.yaml --out "$outfile_temp" --included_blocks suite # run temci
+    mkdir -p "$EXPERIMENTDIR/outputs/"
+    mv "$outfile_temp" "$outfile"
+  fi
+  local temci_report_outfile="$EXPERIMENTDIR/outputs/temci-report.txt"
+  if [ ! -f "${temci_report_outfile}" ]; then
+    temci report "$EXPERIMENTDIR/outputs/${KINDS[0]}.speedcenter.bench.yaml" \
+      "$EXPERIMENTDIR/outputs/${KINDS[1]}.speedcenter.bench.yaml" > "$temci_report_outfile"
+  fi
+}
+
+run() {
+  for i in {0..1}; do
+    # curl -d "Start[MICROBENCHMARK-LOG-${KINDS[i]}]. run:$COMMIT_PRETTY_NAME. 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
+  done;
+}
+
+run 
diff --git a/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-wrapper.sh b/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-wrapper.sh
new file mode 100755
index 000000000000..01fd135e6ad4
--- /dev/null
+++ b/1-runs/run-2024-05-06--13-24-grosser-7950x3d/speedcenter-wrapper.sh
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+bash ./speedcenter-worker.sh 2>&1 | tee log.txt
+