Skip to content

Commit 69d6d52

Browse files
authored
chore: repeat some benchmarks to avoid outliers (#14342)
At this point, only the `compile/incr_header_load` benchmark is being repeated. As more flaky benchmarks pop up, we can repeat them as well. The `repeatedly.py` script is copied and modified from mathlib's bench suite.
1 parent 804bb12 commit 69d6d52

10 files changed

Lines changed: 223 additions & 27 deletions

File tree

tests/README.md

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -249,6 +249,15 @@ These bash variables (set via `<file>.init.sh`) are used by the run script:
249249
A bash variable containing the expected exit code of the program.
250250
When set to `nonzero` instead of a numerical value, the exit code must not be 0.
251251

252+
- `TEST_REPEAT`:
253+
A number specifying how often to repeat the benchmark.
254+
The resulting measurements are averaged.
255+
Has no effect when testing.
256+
257+
- `TEST_REPEAT_DROP_HIGHEST`, `TEST_REPEAT_DROP_LOWEST`:
258+
A number specifying how many extreme measurements to drop before averaging.
259+
Only takes effect if `TEST_REPEAT` is set.
260+
252261
For performance reasons, elab tests can use prebuilt header snapshots.
253262
Building the snapshots and wiring them into the ctest suite (as the `build_lean_header_snapshots.sh` setup fixture) is gated by the `LEAN_HEADER_SNAPSHOTS` CMake option, which currently defaults to `OFF`.
254263
Use of the snapshots at runtime is further controlled by the `LEAN_HEADER_SNAPSHOTS` environment variable:
@@ -310,6 +319,15 @@ These bash variables (set via `<file>.init.sh`) are used by the run script:
310319
A bash variable containing the expected exit code of the program.
311320
When set to `nonzero` instead of a numerical value, the exit code must not be 0.
312321

322+
- `TEST_REPEAT`:
323+
A number specifying how often to repeat the benchmark.
324+
The resulting measurements are averaged.
325+
Has no effect when testing.
326+
327+
- `TEST_REPEAT_DROP_HIGHEST`, `TEST_REPEAT_DROP_LOWEST`:
328+
A number specifying how many extreme measurements to drop before averaging.
329+
Only takes effect if `TEST_REPEAT` is set.
330+
313331
## The `interactive` test pile
314332

315333
These tests are designed to test LSP server requests at a given position in the input file.

tests/bench/build/lakeprof_report_upload.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@
77

88
# Determine paths relative to the current file.
99
script_file = Path(__file__)
10-
src_dir = script_file.parent.parent.parent.parent / "src"
1110
template_file = script_file.parent / "lakeprof_report_template.html"
11+
src_dir = script_file.parent.parent.parent.parent / "src"
1212

1313

1414
def run_stdout(*command: str, cwd: Path | None = None) -> str:

tests/bench/build/lean_wrapper.py

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -35,15 +35,6 @@ def run(*command: str) -> None:
3535
sys.exit(result.returncode)
3636

3737

38-
def run_capture(*command: str) -> tuple[str, str]:
39-
result = subprocess.run(command, capture_output=True, encoding="utf-8")
40-
if result.returncode != 0:
41-
print(result.stdout, end="", file=sys.stdout)
42-
print(result.stderr, end="", file=sys.stderr)
43-
sys.exit(result.returncode)
44-
return result.stdout, result.stderr
45-
46-
4738
def get_module(setup: Path) -> str:
4839
with open(setup) as f:
4940
return json.load(f)["name"]
Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,15 @@
11
/-!
22
Bench: time `lean --incr-load=…` reusing a pre-saved snapshot whose header is `import Lean`.
33
The snapshot is pre-created by `.before.sh` so that the measurement only covers loading,
4-
not the cost of producing the snapshot.
4+
not the cost of producing the snapshot. The snapshot is read-only and left in place (rather
5+
than deleted here) so it can be reused across this benchmark's repeated invocations.
56
-/
67

78
unsafe def main : IO Unit := do
89
let src : System.FilePath := "_tmp_incr_header_load_src.lean"
910
let snap : System.FilePath := "_tmp_incr_header_load.snap"
10-
let deps := snap.addExtension "deps"
1111

1212
let _ ← IO.Process.run {
1313
cmd := "lean"
1414
args := #[s!"--incr-load={snap}", src.toString]
1515
}
16-
17-
IO.FS.removeFile src
18-
IO.FS.removeFile snap
19-
IO.FS.removeFile deps
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
TEST_REPEAT=2
2+
TEST_REPEAT_DROP_HIGHEST=1

tests/compile_bench/run_bench.sh

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,7 @@ if [[ -n $DO_COMPILE ]]; then
2525
lean --c="$1.c" -Dcompiler.postponeCompile=false "${TEST_LEAN_ARGS[@]}" "$1" || fail "Failed to compile $1 into $1.c"
2626
leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$1.out" "${TEST_LEANC_ARGS[@]}" "$1.c" || fail "Failed to compile $1.c"
2727

28-
capture_only "$1" \
29-
"$TEST_DIR/measure.py" -t "$TOPIC" -o "$1.measurements.jsonl" -a -d -- \
30-
"./$1.out" "${TEST_ARGS[@]}"
28+
capture_and_measure "$1" "$TOPIC" "./$1.out" "${TEST_ARGS[@]}"
3129
check_exit_is "${TEST_EXIT:-0}"
3230
extract_measurements "$TOPIC"
3331

@@ -45,8 +43,7 @@ if [[ -n $DO_INTERPRET ]]; then
4543

4644
TOPIC="interpreted/$(basename "$1" .lean)"
4745

48-
capture_only "$1" \
49-
"$TEST_DIR/measure.py" -t "$TOPIC" -o "$1.measurements.jsonl" -a -d -- \
46+
capture_and_measure "$1" "$TOPIC" \
5047
lean -Dlinter.all=false "${TEST_LEANI_ARGS[@]}" --run "$1" "${TEST_ARGS[@]}"
5148
check_exit_is "${TEST_EXIT:-0}"
5249
extract_measurements "$TOPIC"

tests/elab_bench/run_bench.sh

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,11 @@ run_before "$1"
33

44
TOPIC="elab/$(basename "$1" .lean)"
55

6+
rm -f "$1.measurements.jsonl"
7+
68
# `--root` to infer same private names as in the server
79
# Elab.inServer to allow for arbitrary `#eval`
8-
capture_only "$1" \
9-
"$TEST_DIR/measure.py" -t "$TOPIC" -o "$1.measurements.jsonl" -d -- \
10+
capture_and_measure "$1" "$TOPIC" \
1011
lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -DElab.inServer=true "${TEST_LEAN_ARGS[@]}" "$1"
1112
normalize_mvar_suffixes
1213
normalize_reference_urls

tests/measure.py

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77
import subprocess
88
import sys
99
import tempfile
10-
from argparse import Namespace
1110
from dataclasses import dataclass
1211
from pathlib import Path
1312
from typing import Tuple
@@ -184,8 +183,7 @@ def main(
184183
return measured.stdout, measured.stderr
185184

186185

187-
@dataclass
188-
class Args(Namespace):
186+
class Args:
189187
topic: list[str]
190188
metric: list[str]
191189
default_metrics: bool
@@ -243,7 +241,7 @@ class Args(Namespace):
243241
default=[],
244242
help="arguments to pass to the command",
245243
)
246-
args = parser.parse_args(namespace=Args)
244+
args = parser.parse_args(namespace=Args())
247245

248246
metrics = set(args.metric)
249247
if args.default_metrics:

tests/repeatedly.py

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
#!/usr/bin/env python3
2+
3+
import argparse
4+
import json
5+
import subprocess
6+
import sys
7+
from contextlib import contextmanager
8+
from dataclasses import dataclass
9+
from pathlib import Path
10+
11+
12+
@dataclass
13+
class Measurement:
14+
metric: str
15+
value: float
16+
unit: str | None
17+
18+
@classmethod
19+
def from_json_str(cls, s: str) -> "Measurement":
20+
data = json.loads(s.strip())
21+
return cls(data["metric"], data["value"], data.get("unit"))
22+
23+
def to_json_str(self) -> str:
24+
if self.unit is None:
25+
return json.dumps({"metric": self.metric, "value": self.value})
26+
return json.dumps(
27+
{"metric": self.metric, "value": self.value, "unit": self.unit}
28+
)
29+
30+
31+
@contextmanager
32+
def temporarily_move_outfile(outfile: Path):
33+
outfile_tmp = outfile.with_name(outfile.name + ".repeatedly_tmp")
34+
if outfile_tmp.exists():
35+
raise Exception(f"{outfile_tmp} already exists")
36+
37+
outfile.touch()
38+
outfile.rename(outfile_tmp)
39+
try:
40+
yield
41+
finally:
42+
outfile_tmp.rename(outfile)
43+
44+
45+
def read_measurements_from_outfile(outfile: Path) -> list[Measurement]:
46+
measurements = []
47+
with open(outfile, "r") as f:
48+
for line in f:
49+
measurements.append(Measurement.from_json_str(line))
50+
return measurements
51+
52+
53+
def write_measurements_to_outfile(
54+
outfile: Path, measurements: list[Measurement]
55+
) -> None:
56+
with open(outfile, "a") as f:
57+
for measurement in measurements:
58+
f.write(f"{measurement.to_json_str()}\n")
59+
60+
61+
def run_once(cmd: list[str], outfile: Path) -> list[Measurement]:
62+
with temporarily_move_outfile(outfile):
63+
proc = subprocess.run(cmd)
64+
if proc.returncode != 0:
65+
sys.exit(proc.returncode)
66+
67+
return read_measurements_from_outfile(outfile)
68+
69+
70+
def sum_by_metric(measurements: list[Measurement]) -> dict[str, Measurement]:
71+
totals: dict[str, Measurement] = {}
72+
for measurement in measurements:
73+
if existing := totals.get(measurement.metric):
74+
measurement.value += existing.value
75+
totals[measurement.metric] = measurement
76+
return totals
77+
78+
79+
def repeatedly(
80+
cmd: list[str],
81+
iterations: int,
82+
outfile: Path,
83+
drop_highest: int = 0,
84+
drop_lowest: int = 0,
85+
) -> list[Measurement]:
86+
by_metric: dict[str, list[Measurement]] = {}
87+
88+
for i in range(iterations):
89+
for metric, measurement in sum_by_metric(run_once(cmd, outfile)).items():
90+
by_metric.setdefault(metric, []).append(measurement)
91+
92+
if drop_highest + drop_lowest >= iterations:
93+
raise ValueError(
94+
f"drop_highest ({drop_highest}) + drop_lowest ({drop_lowest}) must be "
95+
f"less than the number of iterations ({iterations})"
96+
)
97+
98+
results = []
99+
for metric, measurements in by_metric.items():
100+
if drop_highest or drop_lowest:
101+
measurements.sort(key=lambda m: m.value)
102+
measurements = measurements[drop_lowest : len(measurements) - drop_highest]
103+
if not measurements:
104+
continue
105+
unit = measurements[0].unit
106+
value = sum(m.value for m in measurements) / len(measurements)
107+
results.append(Measurement(metric, value, unit))
108+
109+
return results
110+
111+
112+
class Args:
113+
iterations: int
114+
drop_highest: int
115+
drop_lowest: int
116+
outfile: Path
117+
cmd: str
118+
args: list[str]
119+
120+
121+
if __name__ == "__main__":
122+
parser = argparse.ArgumentParser(
123+
description="Repeatedly run a command, averaging the measurements it writes.",
124+
)
125+
parser.add_argument(
126+
"-n",
127+
"--iterations",
128+
type=int,
129+
default=5,
130+
help="number of iterations",
131+
)
132+
parser.add_argument(
133+
"-H",
134+
"--drop-highest",
135+
type=int,
136+
default=0,
137+
help="drop the n highest values of each metric before averaging",
138+
)
139+
parser.add_argument(
140+
"-L",
141+
"--drop-lowest",
142+
type=int,
143+
default=0,
144+
help="drop the n lowest values of each metric before averaging",
145+
)
146+
parser.add_argument(
147+
"-o",
148+
"--outfile",
149+
type=Path,
150+
default=Path("measurements.jsonl"),
151+
help="measurements file the command under test writes to",
152+
)
153+
parser.add_argument(
154+
"cmd",
155+
help="command to repeatedly run",
156+
)
157+
parser.add_argument(
158+
"args",
159+
nargs="*",
160+
default=[],
161+
help="arguments to pass to the command",
162+
)
163+
args = parser.parse_args(namespace=Args())
164+
165+
measurements = repeatedly(
166+
[args.cmd] + args.args,
167+
args.iterations,
168+
args.outfile,
169+
args.drop_highest,
170+
args.drop_lowest,
171+
)
172+
write_measurements_to_outfile(args.outfile, measurements)

tests/util.sh

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,27 @@ function capture_exit {
117117
check_exit_is "$EXPECTED"
118118
}
119119

120+
# Run a command wrapped with `capture_only` and `measure.py`.
121+
# Additionally wrap with `repeatedly.py` if `TEST_REPEAT` is set,
122+
# respecting `TEST_REPEAT_DROP_HIGHEST` and `TEST_REPEAT_DROP_LOWEST`.
123+
# The first argument specifies the output file path.
124+
# The second argument specifies the topic for the measurements.
125+
# The remaining arguments are the command to run.
126+
# Sets $EXIT to the exit code and $CAPTURED to the output file path.
127+
function capture_and_measure {
128+
local file="$1" topic="$2"; shift 2
129+
if [[ -n "${TEST_REPEAT:-}" ]]; then
130+
capture_only "$file" \
131+
"$TEST_DIR/repeatedly.py" -n "$TEST_REPEAT" \
132+
-H "${TEST_REPEAT_DROP_HIGHEST:-0}" -L "${TEST_REPEAT_DROP_LOWEST:-0}" \
133+
-o "$file.measurements.jsonl" -- \
134+
"$TEST_DIR/measure.py" -t "$topic" -o "$file.measurements.jsonl" -d -- "$@"
135+
else
136+
capture_only "$file" \
137+
"$TEST_DIR/measure.py" -t "$topic" -o "$file.measurements.jsonl" -a -d -- "$@"
138+
fi
139+
}
140+
120141
function source_init {
121142
if [[ -f "$1.init.sh" ]]; then
122143
source "$1.init.sh"

0 commit comments

Comments
 (0)