cpulimit

Verification

Everything here is in the repository and wired into CI. Nothing is claimed as proved beyond what the tools actually reported, and the limits are listed next to the results.

Current status

CI status verify status The results of every run are on the Actions page; this page does not copy them. Figures below were measured on a Linux x86_64 development host unless they say otherwise.

Techniques

TechniqueCovers
Unit, CLI and integration tests (make check)controller, /proc parser, process table, list, CLI, lock, snapshot selection, 55 end-to-end checks with real processes, and 123 checks of cpulimit together with nice, ionice, taskset, chrt, env, nohup, timeout and setsid
SanitizersASan and UBSan on gcc and clang; clang's integer sanitizers
Fuzzingthe stat parser and the CLI parser against stated properties, not only "no crash" (libFuzzer in CI, a standalone driver locally)
Bounded model checkingCBMC harnesses for the controller invariants, tick conversion and the /proc parser (cbmc.yml, manual and weekly). experimental The same harnesses run as random tests on every push (make verif-sim).
Mutation testingdefects re-introduced one at a time, each of which must fail a unit test: 25 mutants, all detected locally
Coveragegcov line and branch coverage with an 85 % line gate
Stress and valgrindfork/exit churn under -i with 300 children: no leaks, flat memory, nothing left stopped
Static analysisgcc -fanalyzer (must be silent), clang-tidy, cppcheck, scan-build, CodeQL
Formatclang-format 18 checked in CI (make format-check)
PortabilityCI matrix of OS, compiler, libc and architecture; the experimental vm workflow

Measurements

Every number is in data/results.json with where and when it was measured, and the charts are drawn from that file by tools/charts.py. They are single runs on a 2-CPU virtual machine with a 10 ms clock tick: treat differences of a point or two as noise.

-4-20+2+4-2.8-2.8-l 10-1.0-1.8-l 25+3.1+2.1-l 50-0.7-0.7-l 75-0.5-0.5-l 90achieved minus requested, percentage points of one CPUupstream 0.3.2this fork
Accuracy. A one-thread busy loop under -l N, 8 s per case. The two versions are the same within noise: both overshoot near 50 % and under-deliver at 10 % and 25 %, because they share one controller. Nothing here is an improvement.
upstream 0.3.2this forksystem calls per second, one target212 calls/s88 calls/s58% lesslimiter CPU, one target0.25 % of one CPU0.12 % of one CPU52% lesslimiter CPU, -i with 200 children4.99 % of one CPU2.37 % of one CPU53% less
Overhead. The gain is in what the limiter itself costs: fewer system calls, and half the CPU with 200 children under -i. The single-target CPU figure is close to the noise floor (an earlier run measured the baseline at 0.12 %), so only the system-call and -i rows were stable across runs. Measured on 1.0.0 against upstream 0.3.2 and not repeated for later releases.
line coverage, % (bar) and branch coverage, % (tick)cli/cli.c100.0 / 98.5core/list.c100.0 / 100.0platform/snapshot.c100.0 / 97.5platform/procfs_parse.c98.7 / 98.2util/util.c97.0 / 94.2core/process_group.c96.9 / 86.5runtime/log.c92.6 / 61.1core/limiter.c88.9 / 83.3platform/iterator.c88.7 / 77.4runtime/lock.c84.5 / 67.7main.c82.5 / 74.3runtime/daemon.c72.6 / 55.3total90.1 / 80.9CI gate: 85% lines
Coverage (tools/coverage.sh (gcov), 2026-10-29, make coverage on 1.0.3 including daemon children). runtime/daemon.c and main.c are the weakest; they hold the process and signal plumbing that is hardest to drive from tests.

Bugs found by the process

  • The bounded model checker found compute_slices() computing 0 / NaN and cleaning it up afterwards (fixed in 1.0.1, the result is identical for every input).
  • Property checks found ticks_to_ms() returning a negative number for ticks = 2^63 + 1 at 1000 Hz and saturating wrongly above 1.8e16 ticks per second (neither reachable with a real clock rate).
  • The OpenBSD runs exposed that p_rtime only advances in scheduling-quantum steps and that zombies are listed; both are fixed and explained under platform notes.

Not verified

  • Nothing is "proved". One CBMC harness has finished (the field positions of a well-formed stat line, within its bounds, CI run 39890593464); the others were narrowed and have no verdict yet. The harnesses cover three pure functions, not the control loop or signal handling.
  • macOS, FreeBSD, NetBSD and Solaris/illumos code has not been run by hand; see the platform table for what CI ran.
  • musl on non-x86 runs under qemu-user, which fakes parts of /proc; some process-name tests are skipped there.
  • Real syslog delivery is not tested. No ACSL/Frama-C specification exists, and AFL++ was not run.
  • The benchmark was measured once on a shared VM, on 1.0.0.

Reproduce

make check analyze verif-sim format-check     # what a change must pass
sh tools/mutation.sh                          # mutants; every one must be killed
make coverage                                 # gcov, with the 85 % gate
make stress                                   # churn, 300 children, valgrind
make bench BASELINE=/path/to/old/cpulimit     # two binaries back to back