From e73c81f0241a0f46a94b548dc6c2aaba338637c1 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 5 Mar 2021 12:37:50 +0100 Subject: [PATCH] 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. --- cmake/ConfigureCVC4.cmake | 7 +++ cmake/Toolchain-mingw64.cmake | 4 +- cvc4autoconfig.h.in | 3 ++ src/main/driver_unified.cpp | 2 +- src/main/time_limit.cpp | 92 ++++++++++++++++++++++++----------- src/main/time_limit.h | 20 ++++++-- 6 files changed, 94 insertions(+), 34 deletions(-) diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake index 9c160e4fc..421fd9f4f 100644 --- a/cmake/ConfigureCVC4.cmake +++ b/cmake/ConfigureCVC4.cmake @@ -76,6 +76,13 @@ check_symbol_exists(optreset "getopt.h" HAVE_DECL_OPTRESET) check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK) check_symbol_exists(strerror_r "string.h" HAVE_STRERROR_R) check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R) +check_symbol_exists(setitimer "sys/time.h" HAVE_SETITIMER) + +# on non-POSIX systems, time limit is implemented with threads +if(NOT HAVE_SETITIMER) + find_package(Threads REQUIRED) + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${CMAKE_THREAD_LIBS_INIT}") +endif() # Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r. check_c_source_compiles( diff --git a/cmake/Toolchain-mingw64.cmake b/cmake/Toolchain-mingw64.cmake index 604de4159..dd2367c72 100644 --- a/cmake/Toolchain-mingw64.cmake +++ b/cmake/Toolchain-mingw64.cmake @@ -16,8 +16,8 @@ SET(CMAKE_SYSTEM_NAME Windows) set(TOOLCHAIN_PREFIX x86_64-w64-mingw32) -SET(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc) -SET(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++) +SET(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc-posix) +SET(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++-posix) SET(CMAKE_RC_COMPILER ${TOOLCHAIN_PREFIX}-windres) # Set target environment path diff --git a/cvc4autoconfig.h.in b/cvc4autoconfig.h.in index 3d3412d66..8af8a5b47 100644 --- a/cvc4autoconfig.h.in +++ b/cvc4autoconfig.h.in @@ -61,6 +61,9 @@ /* Define if `strtok_r' is supported by the platform. */ #cmakedefine HAVE_STRTOK_R +/* Define if `setitimer` is supported by the platform. */ +#cmakedefine01 HAVE_SETITIMER + /* Define to 1 if the header file is available. */ #cmakedefine01 HAVE_UNISTD_H 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 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 -#else +#include "cvc4autoconfig.h" + +#if HAVE_SETITIMER #include #include +#else +#include +#include +#include #endif #include @@ -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 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 @@ -22,15 +22,29 @@ 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 -- 2.30.2