-
Notifications
You must be signed in to change notification settings - Fork 225
Description
I just came back to a BenchExec run which seems to have crashed after a long series of "too many open files" errors from various places. Here's the dump of terminal output I still had: benchexec-too-many-open-files.log.
This was with BenchExec at 3593215. The open file limit was the Ubuntu 24.04 default 1024.
For more context: this was with --numOfThreads 14 on a bench-def consisting of all SV-COMP 2026 C rundefinitions for witness validation.
I don't know the details, but isn't the open file limit independent for each tool execution started by BenchExec? In that case, even if Goblint itself hits the limit (which doesn't seem to be the case), it shouldn't cause BenchExec to hit the limit.
I now started a new run with the limit bumped to 10000, just to see if it makes any difference. The run is still going, but there are strange errors which may be contributing to the eventual demise.
BenchExec terminal output is scattered with versions of the following messages (not together like this):
CRITICAL - Error while starting './goblint_runner.py' in '.': [Errno 32] Broken pipe.
CRITICAL - Error while starting './goblint_runner.py' in '.': [Errno 0] Child process of RunExecutor terminated with exit signal 9.
WARNING - Logfile '/mnt/goblint-svcomp/benchexec/results/292-all-validate-no-diff-box-again/goblint-validate.2025-11-13_08-04-57.logfiles/SV-COMP26_unreach-call.btor2c-lazyMod.circular_pointer_top_w64_d8_e0.yml.log' is too big (size 220417283 bytes). Removing lines.
Also, htop shows BenchExec having a lot of zombie child processes:

Maybe these zombies are using up the open file limit?