Browse Source
			
			
			Moved signal handling to own file to prevent problems with global static variables being non-unique
			
			
				main
			
			
		
		Moved signal handling to own file to prevent problems with global static variables being non-unique
	
		
	
			
			
				main
			
			
		
				 6 changed files with 218 additions and 120 deletions
			
			
		- 
					2src/storm-cli-utilities/cli.cpp
 - 
					2src/storm-cli-utilities/model-handling.h
 - 
					3src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
 - 
					94src/storm/utility/SignalHandler.cpp
 - 
					121src/storm/utility/SignalHandler.h
 - 
					116src/storm/utility/resources.h
 
@ -0,0 +1,94 @@ | 
				
			|||
#include "SignalHandler.h"
 | 
				
			|||
 | 
				
			|||
#include <csignal>
 | 
				
			|||
#include <iostream>
 | 
				
			|||
 | 
				
			|||
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; | 
				
			|||
                } | 
				
			|||
            } | 
				
			|||
 | 
				
			|||
 | 
				
			|||
        } | 
				
			|||
    } | 
				
			|||
} | 
				
			|||
@ -0,0 +1,121 @@ | 
				
			|||
#pragma once | 
				
			|||
 | 
				
			|||
#include <cstdlib> | 
				
			|||
 | 
				
			|||
#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(); | 
				
			|||
 | 
				
			|||
        } | 
				
			|||
    } | 
				
			|||
} | 
				
			|||
						Write
						Preview
					
					
					Loading…
					
					Cancel
						Save
					
		Reference in new issue