diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp index dbe49fd3d3..b8e82fbc6b 100644 --- a/CASC/PortfolioMode.cpp +++ b/CASC/PortfolioMode.cpp @@ -32,7 +32,6 @@ #include "Shell/Shuffling.hpp" #include "Shell/TheoryFinder.hpp" -#include #include #include #include @@ -52,7 +51,6 @@ using namespace Lib; using namespace CASC; -using Lib::Sys::Multiprocessing; using std::cout; using std::cerr; using std::endl; @@ -412,7 +410,7 @@ std::optional PortfolioMode::runSchedule(Schedule schedule) { ALWAYS(it.hasNext()); std::string code = it.next(); - pid_t process = Multiprocessing::instance()->fork(); + pid_t process = Sys::fork(); ASS_NEQ(process, -1); if(process == 0) { @@ -423,10 +421,8 @@ std::optional PortfolioMode::runSchedule(Schedule schedule) { ALWAYS(processes.insert(process)); } - bool exited, signalled; - int code; - // sleep until process changes state - pid_t process = Multiprocessing::instance()->poll_children(exited, signalled, code); + // sleep until any child terminates + auto [ process, signalled, code ] = Sys::waitForChildTermination(-1); /* cout << "Child " << process @@ -434,30 +430,30 @@ std::optional PortfolioMode::runSchedule(Schedule schedule) { << " sig " << signalled << " code " << code << endl; */ - // child died, remove it from the pool and check if succeeded - if(exited) { + // killed by an external agency (could be e.g. a slurm cluster killing for too much memory allocated) + if (signalled) { + Shell::addCommentSignForSZS(cout); + cout<<"Child killed by signal " << code << endl; + ALWAYS(processes.remove(process)); + } else { + // child exited by itself, remove it from the pool and check if succeeded ALWAYS(processes.remove(process)); if(!code) { successful = process; break; } - } else if (signalled) { - // killed by an external agency (could be e.g. a slurm cluster killing for too much memory allocated) - Shell::addCommentSignForSZS(cout); - cout<<"Child killed by signal " << code << endl; - ALWAYS(processes.remove(process)); } } // kill all running processes first for(auto process : processes.iter()) - Multiprocessing::instance()->kill(process, SIGINT); + Sys::kill(process, SIGINT); // and also wait until the killing is really done - // WHY: because we really want to be alone when we later start priting the proof + // WHY: because we really want to be alone when we later start printing the proof // NOTE: an alternative could (maybe) be to just use a SIGKILL above instead of SIGINT for(auto process : processes.iter()) - waitpid(process, nullptr, 0); + Sys::waitForChildTermination(process); // also clean up temporary files // we don't know which processes managed to open their proof file before being killed diff --git a/Lib/Sys/Multiprocessing.cpp b/Lib/Sys/Multiprocessing.cpp index 3d04685f46..6e8de3a826 100644 --- a/Lib/Sys/Multiprocessing.cpp +++ b/Lib/Sys/Multiprocessing.cpp @@ -12,14 +12,12 @@ * Implements class Multiprocessing. */ -#include -#include -#include -#include -#include -#include +#include // errno +#include // kill +#include // fork +#include // waitpid -#include "Debug/TimeProfiling.hpp" +#include "Debug/Assertion.hpp" #include "Lib/Exception.hpp" #include "Multiprocessing.hpp" @@ -29,13 +27,7 @@ namespace Lib namespace Sys { -Multiprocessing* Multiprocessing::instance() -{ - static Multiprocessing inst; - return &inst; -} - -pid_t Multiprocessing::fork() +pid_t fork() { errno=0; pid_t res=::fork(); @@ -45,37 +37,7 @@ pid_t Multiprocessing::fork() return res; } -/** - * Wait for a first child process to terminate, return its pid and assign - * its exit status into @b resValue. If the child was terminated by a signal, - * assign into @b resValue the signal number increased by 256. - */ -pid_t Multiprocessing::waitForChildTermination(int& resValue) -{ - TIME_TRACE("waiting for child") - - int status; - pid_t childPid; - - do { - errno=0; - childPid = wait(&status); - if(childPid==-1) { - SYSTEM_FAIL("Call to wait() function failed.", errno); - } - } while(WIFSTOPPED(status)); - - if(WIFEXITED(status)) { - resValue = WEXITSTATUS(status); - } - else { - ASS(WIFSIGNALED(status)); - resValue = WTERMSIG(status)+256; - } - return childPid; -} - -void Multiprocessing::kill(pid_t child, int signal) +void kill(pid_t child, int signal) { int res = ::kill(child, signal); if(res!=0) { @@ -84,31 +46,24 @@ void Multiprocessing::kill(pid_t child, int signal) } } -void Multiprocessing::killNoCheck(pid_t child, int signal) -{ - ::kill(child, signal); -} - -pid_t Multiprocessing::poll_children(bool &exited, bool &signalled, int &code) +Headstone waitForChildTermination(pid_t query) { int status; - pid_t pid = waitpid(-1 /*wait for any child*/, &status, WUNTRACED); + pid_t pid = waitpid(query, &status, 0); if (pid == -1) { SYSTEM_FAIL("Call to waitpid() function failed.", errno); } - exited = WIFEXITED(status); - signalled = WIFSIGNALED(status); - if(exited) - { - code = WEXITSTATUS(status); - } - if(signalled) - { - code = WTERMSIG(status); - } - return pid; + // PID 0 and 1 are unlikely! + ASS_G(pid, 1) + bool exited = WIFEXITED(status), signalled = WIFSIGNALED(status); + // child should actually have changed state, + // and these are mutually-exclusive conditions + ASS_NEQ(WIFEXITED(status), WIFSIGNALED(status)) + + int code = exited ? WEXITSTATUS(status) : WTERMSIG(status); + return { pid, signalled, code }; } } diff --git a/Lib/Sys/Multiprocessing.hpp b/Lib/Sys/Multiprocessing.hpp index 34cf14a301..53564a5c43 100644 --- a/Lib/Sys/Multiprocessing.hpp +++ b/Lib/Sys/Multiprocessing.hpp @@ -19,18 +19,24 @@ namespace Lib::Sys { -class Multiprocessing { -public: - static Multiprocessing* instance(); - - pid_t waitForChildTermination(int& resValue); - pid_t fork(); - - void kill(pid_t child, int signal); - void killNoCheck(pid_t child, int signal); - pid_t poll_children(bool &exited, bool &signalled, int &code); +// records how a child process died +struct Headstone { + // child PID + pid_t pid; + // if the child was killed by a signal + bool signalled; + // exit code if child exited of its own accord, + // or the signal number used otherwise + int code; }; +// wrap the usual system calls +pid_t fork(); +void kill(pid_t child, int signal); +// wait for a child process to exit: pass -1 for any child +// wraps waitpid +Headstone waitForChildTermination(pid_t pid); + } diff --git a/Test/UnitTesting.cpp b/Test/UnitTesting.cpp index 55367d04d5..0ed16c6611 100644 --- a/Test/UnitTesting.cpp +++ b/Test/UnitTesting.cpp @@ -24,7 +24,6 @@ namespace Test { using namespace std; using namespace Lib; -using namespace Lib::Sys; TestUnit::TestUnit(std::string const& name) : _tests(), _name(name) @@ -189,8 +188,7 @@ bool TestUnit::spawnTest(TestProc proc) return true; } - auto mp = Multiprocessing::instance(); - pid_t fres = mp->fork(); + pid_t fres = Sys::fork(); if(fres == 0) { try { proc(); @@ -203,9 +201,7 @@ bool TestUnit::spawnTest(TestProc proc) } exit(0); } else { - int childRes; - Multiprocessing::instance()->waitForChildTermination(childRes); - return childRes == 0; + return Sys::waitForChildTermination(-1).code == 0; } } diff --git a/vampire.cpp b/vampire.cpp index be74bc1272..7d94bc0f37 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -570,7 +570,7 @@ void interactiveMetamode() break; } else if (line.rfind("run",0) == 0) { // the whole running happens in a child (don't modify our options, don't crash here when parsing option rubbish, etc.) - pid_t process = Lib::Sys::Multiprocessing::instance()->fork(); + pid_t process = Sys::fork(); ASS_NEQ(process, -1); if(process == 0) { UIHelper::unsetExpecting(); // probably garbage at this point