diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 3c456b1bd..391392b31 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -213,9 +213,11 @@ namespace storm { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); // If we were given a time or memory limit, we put it in place now. - // FIXME: insert actual option. - if (false) { - + if (settings.isTimeoutSet()) { + storm::utility::resources::setCPULimit(settings.getTimeoutInSeconds()); + } + if (settings.isMemoutSet()) { + storm::utility::resources::setMemoryLimit(settings.getMemoutInMegabytes()); } // If we have to build the model from a symbolic representation, we need to parse the representation first. diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index ee76dff86..fe61401c2 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -43,7 +43,9 @@ namespace storm { const std::string GeneralSettings::dontFixDeadlockOptionName = "no-fixdl"; const std::string GeneralSettings::dontFixDeadlockOptionShortName = "ndl"; const std::string GeneralSettings::timeoutOptionName = "timeout"; - const std::string GeneralSettings::timeoutOptionShortName = "t"; + const std::string GeneralSettings::timeoutOptionShortName = "to"; + const std::string GeneralSettings::memoutOptionName = "memout"; + const std::string GeneralSettings::memoutOptionShortName = "mo"; const std::string GeneralSettings::eqSolverOptionName = "eqsolver"; const std::string GeneralSettings::lpSolverOptionName = "lpsolver"; const std::string GeneralSettings::smtSolverOptionName = "smtsolver"; @@ -106,7 +108,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout. Note that this is measures in CPU time, not in wallclock time.").setDefaultValueUnsignedInteger(0).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, memoutOptionName, false, "If given, the computation will abort if the given memory is exceeded.").setShortName(memoutOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("memory", "The amount of megabytes available.").setDefaultValueUnsignedInteger(0).build()).build()); std::vector ddLibraries = {"cudd", "sylvan"}; this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.") @@ -251,6 +255,14 @@ namespace storm { uint_fast64_t GeneralSettings::getTimeoutInSeconds() const { return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger(); } + + bool GeneralSettings::isMemoutSet() const { + return this->getOption(memoutOptionName).getHasOptionBeenSet(); + } + + uint_fast64_t GeneralSettings::getMemoutInMegabytes() const { + return this->getOption(memoutOptionName).getArgumentByName("memory").getValueAsUnsignedInteger(); + } storm::solver::EquationSolverType GeneralSettings::getEquationSolver() const { std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 6dd9326e5..1302bcc97 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -259,6 +259,20 @@ namespace storm { */ uint_fast64_t getTimeoutInSeconds() const; + /*! + * Retrieves whether the memout option was set. + * + * @return True if the memout option was set. + */ + bool isMemoutSet() const; + + /*! + * Retrieves the amount of megabytes available. + * + * @return The avail memory given in megabytes. + */ + uint_fast64_t getMemoutInMegabytes() const; + /*! * Retrieves the selected equation solver. * @@ -408,6 +422,8 @@ namespace storm { static const std::string dontFixDeadlockOptionShortName; static const std::string timeoutOptionName; static const std::string timeoutOptionShortName; + static const std::string memoutOptionName; + static const std::string memoutOptionShortName; static const std::string eqSolverOptionName; static const std::string lpSolverOptionName; static const std::string smtSolverOptionName; diff --git a/src/utility/OsDetection.h b/src/utility/OsDetection.h index d91d5595e..83d1f00bd 100644 --- a/src/utility/OsDetection.h +++ b/src/utility/OsDetection.h @@ -13,6 +13,7 @@ # define GetCurrentDir getcwd #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__ # define MACOSX +# define MACOS # define NOEXCEPT noexcept # define _DARWIN_USE_64_BIT_INODE # include diff --git a/src/utility/resources.h b/src/utility/resources.h index 0b9dd80ad..4dfc4a4d5 100644 --- a/src/utility/resources.h +++ b/src/utility/resources.h @@ -11,6 +11,8 @@ #include "src/utility/OsDetection.h" +#include "src/utility/macros.h" + namespace storm { namespace utility { namespace resources { @@ -19,40 +21,49 @@ namespace storm { static const int STORM_EXIT_TIMEOUT = -2; static const int STORM_EXIT_MEMOUT = -3; - inline void setCPULimit(std::size_t seconds) { + inline std::size_t getCPULimit() { rlimit rl; getrlimit(RLIMIT_CPU, &rl); - rl.rlim_cur = seconds; - setrlimit(RLIMIT_CPU, &rl); + return rl.rlim_cur; } - - inline std::size_t getCPULimit() { + + inline void setCPULimit(std::size_t seconds) { rlimit rl; getrlimit(RLIMIT_CPU, &rl); - return rl.rlim_cur; + rl.rlim_cur = seconds; + setrlimit(RLIMIT_CPU, &rl); } inline std::size_t usedCPU() { return std::size_t(clock()) / CLOCKS_PER_SEC; } - inline void setMemoryLimit(std::size_t megabytes) { + inline std::size_t getMemoryLimit() { +#if defined LINUX rlimit rl; getrlimit(RLIMIT_AS, &rl); - rl.rlim_cur = megabytes * 1024 * 1024; - setrlimit(RLIMIT_AS, &rl); + return rl.rlim_cur; +#else + STORM_LOG_WARN("Retrieving the memory limit is not supported for your operating system."); + return 0; +#endif } - inline std::size_t getMemoryLimit() { + inline void setMemoryLimit(std::size_t megabytes) { +#if defined LINUX rlimit rl; getrlimit(RLIMIT_AS, &rl); - return rl.rlim_cur; + rl.rlim_cur = megabytes * 1024 * 1024; + setrlimit(RLIMIT_AS, &rl); +#else + STORM_LOG_WARN("Setting a memory limit is not supported for your operating system."); +#endif } - inline void quick_exit_if_available(int errorCode) { -#ifdef LINUX + inline void quickest_exit(int errorCode) { +#if defined LINUX std::quick_exit(errorCode); -#elseif MACOS +#elif defined MACOS std::_Exit(errorCode); #else std::abort(); @@ -62,13 +73,13 @@ namespace storm { inline void signalHandler(int signal) { if (signal == SIGXCPU) { std::cerr << "Timeout." << std::endl; - quick_exit_if_available(STORM_EXIT_TIMEOUT); + quickest_exit(STORM_EXIT_TIMEOUT); } else if (signal == ENOMEM) { std::cerr << "Out of memory" << std::endl; - quick_exit_if_available(STORM_EXIT_MEMOUT); + quickest_exit(STORM_EXIT_MEMOUT); } else { std::cerr << "Unknown abort in resource limitation module." << std::endl; - quick_exit_if_available(STORM_EXIT_GENERALERROR); + quickest_exit(STORM_EXIT_GENERALERROR); } }