Feature Request - Allow Memory Oversubscription

[sosy-lab]

Feature Request - Allow Memory Oversubscription

[MontyCarter]

By the way, I tried starting two calls to benchexec, each with 8 concurrent benchmarks and 15GB memory, but it seems like it puts 1 execution from each call to benchexec into each cgroup. (That is, 8 cgroup containers, each with 2 jobs - one from each call to benchexec).

I'm guessing this is because the cgroups are not uniquely named between calls to benchexec (for example, both calls to benchexec use 8 cgroups, named like "benchgroup1, benchgroup2, ..., benchgroup8", and so they end up going in the same container)?

If this is the case, then using unique cgroup names between benchexec calls would provide the functionality I'm looking for, as opposed to creating an explicit switch to allow oversubscription.

[PhilippWendler]

BenchExec does create unique cgroup names and would never put different runs into the same cgroup. If you can reproduce other behavior, please file a separate bug.

For the original proposal, I think it is technically possible to implement with cgroups. I am not convinced on whether it makes sense, though, if we really abort completely on OOM. This would mean that basically the whole benchmark was wasted.

Another strategy we have implemented in a different system is to start each run with half of its memory limit first, and if it hits the limit, restart this single run with its full limit. This could also be done in BenchExec and has the advantage that it produces exactly the same results as starting all runs with the full limit, but it would significantly complicate the resource assignment and task scheduling in BenchExec.

I won't have time for this year's SV-Comp to implement any of these possibilities.

Note that for your machine, also your number of cores only allows to have 8 parallel runs if you want to use the SV-Comp resource settings (4 cores plus hyper-threading). So if you want more parallel runs, you need to reduce the number of cores, so you could also consider simply reducing the memory limit (and maybe manually execute the OOM results again, or just ignore them).

Running two BenchExec instances in parallel would mean that there is absolutely no possibility to prevent severely skewed results if you do overbooking. The kernel could start swapping any of the runs, or (if you have not enough swap) even start killing runs before they reach their memory limit.