search

c-cube / frog-utils

[frozen] Scheduling and running jobs on a shared computer, then analyse their output
BSD 2-Clause "Simplified" License
5 stars 0 forks source link

System timeout and memory management #29

Closed rafoo closed 7 years ago

rafoo commented 8 years ago

In frogtptp, the $timeout and $memory variables are currently handled by the provers but not all of them feature options for timeout and memory management and the one who do might behave differently (for example: are these options only used for proof search by itself or also for problem preprocessing?).

For fair comparison of tools, it would be better to wrap the prover call with the system commands (timeout and ulimit).

c-cube commented 8 years ago

Yeah, this is annoying. I had issues with ulimit and its behavior w.r.t. memory, but this needs to be fixed.

Gbury commented 8 years ago

So, on that subject, the following issue might be related: https://github.com/Gbury/ocaml-cgroups/issues/1 Indeed, the best way to manage memory for processes (and sub-processes), is to use cgroups (at least under Linux, for windows I am clueless, but I don't think it matters for our use case here), which are being reworked (or have been reworked recently ?). The new way of interacting with cgroups would be to use the new and shiny systemd API (exposed through dbus), what do you think about it ?

c-cube commented 7 years ago

Doesn't seem like we have a good solution other than the current ulimit one, closing this for now. We should re-open if there is a magical new solution that appears on linux, with acceptable bindings.