Repository navigation
Measure Linux benchmark peak RSS with GNU time - #165
Conversation
|
@sharkdp It looks like ru_maxrss includes the parent's high-water RSS from before exec, so the harness's own memory leaks into the result. Could you measure through GNU /usr/bin/time -f %M on Linux, as the macOS path does, so the checker starts from a small process? I'll rerun the experiment on the updated PR. |
There was a problem hiding this comment.
🟡 Changes recommended
The timing test does not assert peak RSS, leaving discarded values or incorrect unit conversions undetected and the memory-measurement regression unprotected.
1 open issue
What changed in this PR
This PR addresses #161 by measuring Linux type-checker peak RSS at process exit, avoiding missed memory peaks from polling.
Changes:
- Use blocking
wait4()to collect exit status and peak RSS on Linux. - Retain
/procpolling only for memory-limit enforcement. - Update the timing test to verify Linux uses a blocking wait.
| File | Description |
|---|---|
typecheck_benchmark/daily_runner.py |
Collect peak RSS with wait4() and separate memory-limit monitoring. |
tests/test_typecheck_benchmark_timing.py |
Verify blocking wait4() behavior on Linux. |
Review effort: Balanced
| if sys.platform == "linux": | ||
| with patch("os.wait4", wraps=os.wait4) as wait4: | ||
| run_process_with_timeout( | ||
| [sys.executable, "-S", "-c", "pass"], | ||
| cwd=tmp_path, timeout=30, capture_output=False, | ||
| ) | ||
| wait4.assert_called_once() | ||
| assert wait4.call_args.args[1] == 0 # Blocking wait. | ||
| return |
sharkdp
changed the title
|
Ok, updated to use GNU time. I also edited the PR description with the updated experiment. |
lolpack
left a comment
lolpack
left a comment
There was a problem hiding this comment.
The timing was largely unaffected from this change, but still worth landing for better resiliency and precision. https://github.com/lolpack/type_coverage_py/actions/runs/42083592710
The runner measures Linux peak memory with /usr/bin/time (#165). The ubuntu-latest image ships it today, but if a future image dropped it every checker would fail to launch and the whole run would crash. Installing it explicitly is a no-op while it is present.
Fixes #161.
Use GNU time on Linux to collect peak RSS when the type-checker exits (the OOM watcher still uses
/proc/<pid>/statusfor querying while the process is still running).I ran a benchmark for each type-checker on "cerify". Each cell shows min..max peak RSS in MiB for five benchmarking runs. Standalone GNU
timeis used for comparison. As we can tell from this table, the new ("After") results are closed to thetimemeasurements, especially for the fast-running type checkers. The previous implementation could miss as much as 13 MiB, or 20% of the peak RSS (see e.g. the "min" times in the Pyrefly or ty rows):/procpolling)time)time