search

sosy-lab / benchexec

BenchExec: A Framework for Reliable Benchmarking and Resource Measurement
Apache License 2.0
234 stars 201 forks source link

Use PID cgroup controller to limit number of tasks #235

Open PhilippWendler opened 7 years ago

PhilippWendler commented 7 years ago

In order to prevent (accidental) fork bombs and exhaustion of the number of available PIDs, BenchExec should use the pid cgroup controller (if available) and set a limit of concurrent tasks (threads and processes) per run. In theory, we could make the limit configurable, but as this is mostly to prevent crashing the system, I think it enough to just hard-code it to a high value like 10000.

PhilippWendler commented 6 years ago

Such a problem has happened in SV-COMP'19, so we should implement this.

The problem was that there was a limit of about 10000 PIDs for a user, and a run triggered this, leaving BenchExec and other runs no chance to create further threads/processes. So in order for us to always be able to fork, we need to limit the runs.

PhilippWendler commented 6 years ago

As workaround, one can use --set-cgroup-value pids.max=5000.