Reimplement time limit mechanism for windows (#6049)

As noted in #5034, --tlimit is not working properly on windows. It turns out that the timer mechanism provided by the windows API are not suitable for our use case. Thus, this PR implements a generic std::thread-based timer mechanism which is used whenever the POSIX timers (setitimer) are not available. It also adds some documentation on the timer options and the reasons we ended up with this.
Fixes #5034.

3 files changed, 82 insertions, 32 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 7228bc167..311b81708 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -98,7 +98,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   // Parse the options
   vector<string> filenames = Options::parseOptions(&opts, argc, argv);
 
-  install_time_limit(opts);
+  auto limit = install_time_limit(opts);
 
   string progNameStr = opts.getBinaryName();
   progName = &progNameStr;
diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index be506a518..b709da165 100644
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -12,15 +12,45 @@
  ** \brief Implementation of time limits.
  **
  ** Implementation of time limits that are imposed by the --tlimit option.
+ **
+ ** There are various strategies to implement time limits, with different
+ ** advantages and disadvantages:
+ **
+ ** std::thread: we can spawn a new thread which waits for the time limit.
+ ** Unless we use std::jthread (from C++20), std::thread is not interruptible
+ ** and thus we need a synchronization mechanism so that the main thread can
+ ** communicate to the timer thread that it wants to finish. Apparently, this
+ ** is the only platform independent way.
+ **
+ ** POSIX setitimer: a very simple way that instructs the kernel to send a
+ ** signal after some time. If available, this is what we want!
+ **
+ ** Win32 CreateWaitableTimer: unfortunately, this mechanism only calls the
+ ** completion routine (the callback) when the main thread "enters an
+ ** alertable wait state", i.e. it sleeps. We don't want our main thread to
+ ** sleep, thus this approach is not appropriate.
+ **
+ ** Win32 SetTimer: while we can specify a callback function, we still need
+ ** to process the windows event queue for the callback to be called. (see
+ ** https://stackoverflow.com/a/15406527/2375725). We don't want our main
+ ** thread to continuously monitor the event queue.
+ **
+ **
+ ** We thus use the setitimer variant whenever possible, and the std::thread
+ ** variant otherwise.
  **/
 
 #include "time_limit.h"
 
-#if defined(__MINGW32__) || defined(__MINGW64__)
-#include <windows.h>
-#else
+#include "cvc4autoconfig.h"
+
+#if HAVE_SETITIMER
 #include <signal.h>
 #include <sys/time.h>
+#else
+#include <atomic>
+#include <chrono>
+#include <thread>
 #endif
 
 #include <cerrno>
@@ -31,43 +61,31 @@
 namespace CVC4 {
 namespace main {
 
-#if defined(__MINGW32__) || defined(__MINGW64__)
-void CALLBACK win_timeout_handler(LPVOID lpArg,
-                                  DWORD dwTimerLowValue,
-                                  DWORD dwTimerHighValue)
+#if HAVE_SETITIMER
+TimeLimit::~TimeLimit() {}
+
+void posix_timeout_handler(int sig, siginfo_t* info, void*)
 {
   signal_handlers::timeout_handler();
 }
 #else
-void posix_timeout_handler(int sig, siginfo_t* info, void*)
+std::atomic<bool> abort_timer_flag;
+
+TimeLimit::~TimeLimit()
 {
-  signal_handlers::timeout_handler();
+  abort_timer_flag.store(true);
 }
 #endif
 
-void install_time_limit(const Options& opts)
+TimeLimit install_time_limit(const Options& opts)
 {
   unsigned long ms = opts.getCumulativeTimeLimit();
   // Skip if no time limit shall be set.
-  if (ms == 0) return;
-
-#if defined(__MINGW32__) || defined(__MINGW64__)
-  HANDLE hTimer = CreateWaitableTimer(nullptr, true, TEXT("CVC4::Timeout"));
-  if (hTimer == nullptr)
-  {
-    throw Exception(std::string("CreateWaitableTimer() failure: ")
-                    + std::to_string(GetLastError()));
+  if (ms == 0) {
+    return TimeLimit();
   }
-  LARGE_INTEGER liDueTime;
-  liDueTime.LowPart = (DWORD)(ms & 0xFFFFFFFF);
-  liDueTime.HighPart = 0;
-  if (!SetWaitableTimer(
-          hTimer, &liDueTime, 0, win_timeout_handler, nullptr, false))
-  {
-    throw Exception(std::string("SetWaitableTimer() failure: ")
-                    + std::to_string(GetLastError()));
-  }
-#else
+
+#if HAVE_SETITIMER
   // Install a signal handler for SIGALRM
   struct sigaction sact;
   sact.sa_sigaction = posix_timeout_handler;
@@ -93,7 +111,25 @@ void install_time_limit(const Options& opts)
   {
     throw Exception(std::string("timer_settime() failure: ") + strerror(errno));
   }
+#else
+  abort_timer_flag.store(false);
+  std::thread t([ms]()
+  {
+    // when to stop
+    auto limit = std::chrono::system_clock::now() + std::chrono::milliseconds(ms);
+    while (limit > std::chrono::system_clock::now())
+    {
+      // check if the main thread is done
+      if (abort_timer_flag.load()) return;
+      std::this_thread::sleep_for(std::chrono::milliseconds(100));
+    }
+    // trigger the timeout handler
+    signal_handlers::timeout_handler();
+  });
+  // detach the thread
+  t.detach();
 #endif
+  return TimeLimit();
 }
 
 }  // namespace main
diff --git a/src/main/time_limit.h b/src/main/time_limit.h
index 22aaff8cd..d137158d0 100644
--- a/src/main/time_limit.h
+++ b/src/main/time_limit.h
@@ -23,14 +23,28 @@ namespace CVC4 {
 namespace main {
 
 /**
+ * This class makes sure that the main thread signals back to the time
+ * limit mechanism when it wants to terminate. This is necessary if we
+ * use our custom std::thread-based timers. Following RAII, we signal
+ * this using a destructor so that we can never forget to abort the time
+ * limit thread.
+ */
+struct TimeLimit
+{
+    ~TimeLimit();
+};
+
+/**
  * Installs an overall wall-clock time limit for the solver binary.
  * It retrieves the time limit and creates a POSIX timer (via setitimer()).
  * This timer signals its expiration with an SIGALRM that is handled by
  * timeout_handler() in signal_handler.cpp.
- * For windows, we use a timer (via SetWaitableTimer()) that uses
- * timeout_handler() as callback function.
+ * If the POSIX timers are not available (e.g., we are running on windows)
+ * we implement our own timer based on std::thread. In this case, the main
+ * thread needs to communicate back to the timer thread when it wants to
+ * terminate, which is done via the TimeLimit object.
  */
-void install_time_limit(const Options& opts);
+TimeLimit install_time_limit(const Options& opts);
 
 }  // namespace main
 }  // namespace CVC4