cleanup Multiprocessing API

CASC/PortfolioMode.cpp

@@ -32,9 +32,7 @@
 #include "Shell/Shuffling.hpp"
 #include "Shell/TheoryFinder.hpp"
 
-#include <sys/wait.h>
 #include <limits>
-#include <unistd.h>
 #include <signal.h>
 #include <fstream>
 #include <random>
@@ -52,7 +50,6 @@
 
 using namespace Lib;
 using namespace CASC;
-using Lib::Sys::Multiprocessing;
 using std::cout;
 using std::cerr;
 using std::endl;
@@ -412,7 +409,7 @@ std::optional<fs::path> 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,41 +420,39 @@ std::optional<fs::path> 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
         << " exit " << exited
         << " 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

Lib/Sys/Multiprocessing.cpp

@@ -12,14 +12,12 @@
  * Implements class Multiprocessing.
  */
 
-#include <cerrno>
-#include <csignal>
-#include <cerrno>
-#include <unistd.h>
-#include <sys/types.h>
-#include <sys/wait.h>
+#include <cerrno> // errno
+#include <csignal> // kill
+#include <unistd.h> // fork
+#include <sys/wait.h> // 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 };
 }
 
 }

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);
+
 }
 
 

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;
   }
 }
 

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