diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 673e6797f..52eb630af 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -5,8 +5,8 @@ #include "storm/utility/file.h" #include "storm/utility/storm-version.h" #include "storm/utility/macros.h" - #include "storm/utility/initialize.h" +#include "storm/utility/SignalHandler.h" #include "storm/utility/Stopwatch.h" #include diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 5845d5c31..6db536f2d 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -5,7 +5,7 @@ #include "storm-counterexamples/api/counterexamples.h" #include "storm-parsers/api/storm-parsers.h" -#include "storm/utility/resources.h" +#include "storm/utility/SignalHandler.h" #include "storm/utility/file.h" #include "storm/utility/storm-version.h" #include "storm/utility/macros.h" diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 3931279c1..35645d02e 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -21,6 +21,7 @@ #include "storm/utility/vector.h" #include "storm/utility/graph.h" #include "storm/utility/NumberTraits.h" +#include "storm/utility/SignalHandler.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" @@ -29,8 +30,6 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LpSolver.h" -#include "storm/utility/resources.h" - #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/InvalidOperationException.h" diff --git a/src/storm/utility/SignalHandler.cpp b/src/storm/utility/SignalHandler.cpp new file mode 100644 index 000000000..13cdcae08 --- /dev/null +++ b/src/storm/utility/SignalHandler.cpp @@ -0,0 +1,94 @@ +#include "SignalHandler.h" + +#include +#include + +namespace storm { + namespace utility { + namespace resources { + + // Maximal waiting time after abort signal before terminating + const int maxWaitTime = 3; + + SignalInformation::SignalInformation() : terminate(false), lastSignal(0) { + } + + SignalInformation::~SignalInformation() { + // Intentionally left empty. + } + + SignalInformation& SignalInformation::infos() { + static SignalInformation signalInfo; + return signalInfo; + } + + /*! + * Signal handler for aborts, etc. + * After the first signal the handler waits a number of seconds to let the program print preliminary results + * which were computed up this point. If the waiting time is exceeded or if a second signal was raised + * in the mean time, the program immediately terminates. + * + * @param signal Exit code of signal. + */ + void signalHandler(int signal) { + if (!isTerminate()) { + // First time we get an abort signal + // We give the program a number of seconds to print results obtained so far before termination + std::cerr << "ERROR: The program received signal " << signal << " and will be aborted in " << maxWaitTime << "s." << std::endl; + SignalInformation::infos().setTerminate(true); + // Remember original signal such that the program returns the correct original signal + SignalInformation::infos().setErrorCode(signal); + // Trigger a new signal after waitTime + setTimeoutAlarm(maxWaitTime); + } else { + // Second time we get a signal + // We now definitely have to terminate as fast as possible + if (SignalInformation::infos().getErrorCode() == SIGXCPU) { + std::cerr << "TIMEOUT." << std::endl; + } else if (SignalInformation::infos().getErrorCode() == ENOMEM) { + std::cerr << "OUT OF MEMORY." << std::endl; + } else if (SignalInformation::infos().getErrorCode() == SIGABRT || SignalInformation::infos().getErrorCode() == SIGINT) { + std::cerr << "ABORT." << std::endl; + } else { + std::cerr << "Received signal " << signal << std::endl; + } + quickest_exit(SignalInformation::infos().getErrorCode()); + } + } + + void installSignalHandler() { + // We use the newer sigaction instead of signal + struct sigaction sa; + sa.sa_handler = signalHandler; + sigemptyset(&sa.sa_mask); + sa.sa_flags = SA_RESTART; + + // CPU Limit + if (sigaction(SIGXCPU, &sa, nullptr) == -1) { + std::cerr << "FATAL: Installing a signal handler failed." << std::endl; + } + // Memory out + if (sigaction(ENOMEM, &sa, nullptr) == -1) { + std::cerr << "FATAL: Installing a signal handler failed." << std::endl; + } + if (sigaction(SIGSEGV, &sa, nullptr) == -1) { + std::cerr << "FATAL: Installing a signal handler failed." << std::endl; + } + if (sigaction(SIGABRT, &sa, nullptr) == -1) { + std::cerr << "FATAL: Installing a signal handler failed." << std::endl; + } + if (sigaction(SIGINT, &sa, nullptr) == -1) { + std::cerr << "FATAL: Installing a signal handler failed." << std::endl; + } + if (sigaction(SIGTERM, &sa, nullptr) == -1) { + std::cerr << "FATAL: Installing a signal handler failed." << std::endl; + } + if (sigaction(SIGALRM, &sa, nullptr) == -1) { + std::cerr << "FATAL: Installing a signal handler failed." << std::endl; + } + } + + + } + } +} diff --git a/src/storm/utility/SignalHandler.h b/src/storm/utility/SignalHandler.h new file mode 100644 index 000000000..070509583 --- /dev/null +++ b/src/storm/utility/SignalHandler.h @@ -0,0 +1,121 @@ +#pragma once + +#include + +#include "storm-config.h" +#include "storm/utility/OsDetection.h" + +namespace storm { + namespace utility { + namespace resources { + + /*! + * Exit without cleanup. + * @param errorCode Error code to return. + */ + inline void quickest_exit(int errorCode) { +#if defined LINUX + std::quick_exit(errorCode); +#elif defined MACOS + std::_Exit(errorCode); +#else + std::abort(); +#endif + } + + /*! + * Set timeout by raising an alarm after timeout seconds. + * @param timeout Timeout in seconds. + */ + inline void setTimeoutAlarm(uint_fast64_t timeout) { + alarm(timeout); + } + + + class SignalInformation { + public: + + // Explicitly delete copy constructor + SignalInformation(SignalInformation const&) = delete; + + // Explicitly delete copy constructor + void operator=(SignalInformation const&) = delete; + + /*! + * Retrieves the only existing instance of the signal information. + * + * @return The only existing instance of the signal information. + */ + static SignalInformation& infos(); + + /*! + * Check whether the program should terminate (due to some abort signal). + * + * @return True iff program should terminate. + */ + inline bool isTerminate() const { + return terminate; + } + + /*! + * Set whether the program should terminate. + * + * @param terminate True iff program should terminate. + */ + inline void setTerminate(bool terminate) { + this->terminate = terminate; + } + + /*! Get the error code. + * Default is 0. If a signal was handled, the corresponding signal code is returned. + * + * @return Error code. + */ + inline int getErrorCode() const { + return lastSignal; + } + + /*! Set the error code. + * + * @param errorCode Error code. + */ + inline void setErrorCode(int errorCode) { + lastSignal = errorCode; + } + + private: + /*! + * Constructs new signal information. This constructor is private to forbid instantiation of this class. The only + * way to create a new instance is by calling the static infos() method. + */ + SignalInformation(); + + /*! + * This destructor is private, since we need to forbid explicit destruction of the signal information. + */ + virtual ~SignalInformation(); + + + // Flag whether the program should terminate + bool terminate; + // Store last signal code + int lastSignal; + }; + + /*! + * Check whether the program should terminate (due to some abort signal). + * + * @return True iff program should terminate. + */ + inline bool isTerminate() { + return SignalInformation::infos().isTerminate(); + } + + /*! + * Register some signal handlers to detect and correctly handle abortion (due to timeout for example). + */ + void installSignalHandler(); + + } + } +} \ No newline at end of file diff --git a/src/storm/utility/resources.h b/src/storm/utility/resources.h index 3b9138150..eb84d73c0 100644 --- a/src/storm/utility/resources.h +++ b/src/storm/utility/resources.h @@ -1,8 +1,6 @@ #ifndef STORM_UTILITY_RESOURCES_H_ #define STORM_UTILITY_RESOURCES_H_ -#include -#include #include #include #include @@ -15,30 +13,6 @@ namespace storm { namespace utility { namespace resources { - // Maximal waiting time after abort signal before terminating - static const int maxWaitTime = 3; - - // Flag whether the program should terminate - static bool terminate = false; - // Store last signal code - static int lastSignal = 0; - - /*! - * Check whether the program should terminate (due to some abort signal). - * @return True iff program should terminate. - */ - inline bool isTerminate() { - return terminate; - } - - /*! Get the error code. - * Default is 0. If a signal was handled, the corresponding signal code is returned. - * @return Error code. - */ - inline int getErrorCode() { - return lastSignal; - } - /*! * Get CPU limit. * @return CPU limit in seconds. @@ -99,96 +73,6 @@ namespace storm { #endif } - /*! - * Exit without cleanup. - * @param errorCode Error code to return. - */ - inline void quickest_exit(int errorCode) { -#if defined LINUX - std::quick_exit(errorCode); -#elif defined MACOS - std::_Exit(errorCode); -#else - std::abort(); -#endif - } - - /*! - * Set timeout by raising an alarm after timeout seconds. - * @param timeout Timeout in seconds. - */ - inline void setTimeoutAlarm(uint_fast64_t timeout) { - alarm(timeout); - } - - /*! - * Signal handler for aborts, etc. - * After the first signal the handler waits a number of seconds to let the program print preliminary results - * which were computed up this point. If the waiting time is exceeded or if a second signal was raised - * in the mean time, the program immediately terminates. - * @param signal Exit code of signal. - */ - inline void signalHandler(int signal) { - if (!isTerminate()) { - // First time we get an abort signal - // We give the program a number of seconds to print results obtained so far before termination - std::cerr << "ERROR: The program received signal " << signal << " and will be aborted in " << maxWaitTime << "s." << std::endl; - terminate = true; - // Remember original signal such that the program returns the correct original signal - lastSignal = signal; - // Trigger a new signal after waitTime - setTimeoutAlarm(maxWaitTime); - } else { - // Second time we get a signal - // We now definitely have to terminate as fast as possible - if (getErrorCode() == SIGXCPU) { - std::cerr << "TIMEOUT." << std::endl; - } else if (getErrorCode() == ENOMEM) { - std::cerr << "OUT OF MEMORY." << std::endl; - } else if (getErrorCode() == SIGABRT || getErrorCode() == SIGINT) { - std::cerr << "ABORT." << std::endl; - } else { - std::cerr << "Received signal " << signal << std::endl; - } - quickest_exit(getErrorCode()); - } - } - - /*! - * Register some signal handlers to detect and correctly handle abortion (due to timeout for example). - */ - inline void installSignalHandler() { - // We use the newer sigaction instead of signal - struct sigaction sa; - sa.sa_handler = signalHandler; - sigemptyset(&sa.sa_mask); - sa.sa_flags = SA_RESTART; - - // CPU Limit - if (sigaction(SIGXCPU, &sa, nullptr) == -1) { - std::cerr << "FATAL: Installing a signal handler failed." << std::endl; - } - // Memory out - if (sigaction(ENOMEM, &sa, nullptr) == -1) { - std::cerr << "FATAL: Installing a signal handler failed." << std::endl; - } - if (sigaction(SIGSEGV, &sa, nullptr) == -1) { - std::cerr << "FATAL: Installing a signal handler failed." << std::endl; - } - if (sigaction(SIGABRT, &sa, nullptr) == -1) { - std::cerr << "FATAL: Installing a signal handler failed." << std::endl; - } - if (sigaction(SIGINT, &sa, nullptr) == -1) { - std::cerr << "FATAL: Installing a signal handler failed." << std::endl; - } - if (sigaction(SIGTERM, &sa, nullptr) == -1) { - std::cerr << "FATAL: Installing a signal handler failed." << std::endl; - } - if (sigaction(SIGALRM, &sa, nullptr) == -1) { - std::cerr << "FATAL: Installing a signal handler failed." << std::endl; - } - } - } } }