From: Gereon Kremer Date: Thu, 16 Jul 2020 19:57:36 +0000 (+0200) Subject: Resource manager cleanup (#4732) X-Git-Tag: cvc5-1.0.0~3097 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6187b58ed1a7d5c74fa148d663964daef8efae2d;p=cvc5.git Resource manager cleanup (#4732) This PR performs some general cleanup in and around the ResourceManager class. In detail, it does remove --hard-limit (we decided to always leave the solver in a usable state, i.e. always do a soft limit), remove --cpu-time (we decided to always use wall-clock time for time limiting) replace old gettimeofday-based Timer by new std::chrono-based WallClockTimer clean up the logic around beginCall() and endCall() --- diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 96fccdcdb..18a99ad3c 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -482,15 +482,6 @@ header = "options/smt_options.h" read_only = true help = "enable resource limiting per query" -[[option]] - name = "hardLimit" - category = "common" - long = "hard-limit" - type = "bool" - default = "false" - read_only = true - help = "the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)" - [[option]] name = "rewriteStep" category = "expert" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a3313a733..16e4e916a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -148,9 +148,9 @@ void DeleteAndClearCommandVector(std::vector& commands) { commands.clear(); } -class SoftResourceOutListener : public Listener { +class ResourceOutListener : public Listener { public: - SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} + ResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} void notify() override { SmtScope scope(d_smt); @@ -159,20 +159,7 @@ class SoftResourceOutListener : public Listener { } private: SmtEngine* d_smt; -}; /* class SoftResourceOutListener */ - - -class HardResourceOutListener : public Listener { - public: - HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} - void notify() override - { - SmtScope scope(d_smt); - theory::Rewriter::clearCaches(); - } - private: - SmtEngine* d_smt; -}; /* class HardResourceOutListener */ +}; /* class ResourceOutListener */ class BeforeSearchListener : public Listener { public: @@ -364,10 +351,7 @@ class SmtEnginePrivate : public NodeManagerListener { ResourceManager* rm = d_smt.getResourceManager(); d_listenerRegistrations->add( - rm->registerSoftListener(new SoftResourceOutListener(d_smt))); - - d_listenerRegistrations->add( - rm->registerHardListener(new HardResourceOutListener(d_smt))); + rm->registerListener(new ResourceOutListener(d_smt))); try { @@ -638,8 +622,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) new ResourceManager(*d_statisticsRegistry.get(), d_options)); d_private.reset(new smt::SmtEnginePrivate(*this)); d_stats.reset(new SmtEngineStatistics()); - d_stats->d_resourceUnitsUsed.setData(d_resourceManager->getResourceUsage()); - + // The ProofManager is constructed before any other proof objects such as // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are // initialized in TheoryEngine and PropEngine respectively. @@ -663,7 +646,6 @@ void SmtEngine::finishInit() // of SMT-LIB 2.6 standard. // Inialize the resource manager based on the options. - d_resourceManager->setHardLimit(options::hardLimit()); if (options::perCallResourceLimit() != 0) { d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false); @@ -1371,16 +1353,15 @@ Result SmtEngine::check() { Trace("smt") << "SmtEngine::check()" << endl; - d_resourceManager->beginCall(); - // Only way we can be out of resource is if cumulative budget is on - if (d_resourceManager->cumulativeLimitOn() && d_resourceManager->out()) + if (d_resourceManager->out()) { Result::UnknownExplanation why = d_resourceManager->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename); } + d_resourceManager->beginCall(); // Make sure the prop layer has all of the assertions Trace("smt") << "SmtEngine::check(): processing assertions" << endl; diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index 964237499..9b25580d2 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -32,8 +32,7 @@ SmtEngineStatistics::SmtEngineStatistics() d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), - d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0), - d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed") + d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) { smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); smtStatisticsRegistry()->registerStat(&d_numConstantProps); @@ -48,7 +47,6 @@ SmtEngineStatistics::SmtEngineStatistics() smtStatisticsRegistry()->registerStat(&d_pushPopTime); smtStatisticsRegistry()->registerStat(&d_processAssertionsTime); smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse); - smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed); } SmtEngineStatistics::~SmtEngineStatistics() @@ -66,7 +64,6 @@ SmtEngineStatistics::~SmtEngineStatistics() smtStatisticsRegistry()->unregisterStat(&d_pushPopTime); smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime); smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse); - smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed); } } // namespace smt diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index 3ea46eaa4..3463a0371 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -53,8 +53,6 @@ struct SmtEngineStatistics /** Has something simplified to false? */ IntStat d_simplifiedToFalse; - /** Number of resource units spent. */ - ReferenceStat d_resourceUnitsUsed; }; /* struct SmtEngineStatistics */ } // namespace smt diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 7080d5040..ac1d57324 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -25,66 +25,47 @@ using namespace std; namespace CVC4 { -void Timer::set(uint64_t millis) +bool WallClockTimer::on() const { - d_ms = millis; - Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; - // keep track of when it was set, even if it's disabled (i.e. == 0) - // Wall time - gettimeofday(&d_wall_limit, NULL); - Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," - << d_wall_limit.tv_usec << std::endl; - d_wall_limit.tv_sec += millis / 1000; - d_wall_limit.tv_usec += (millis % 1000) * 1000; - if (d_wall_limit.tv_usec > 1000000) + // default-constructed time points are at the respective epoch + return d_limit.time_since_epoch().count() != 0; +} +void WallClockTimer::set(uint64_t millis) +{ + if (millis == 0) + { + // reset / deactivate + d_start = time_point(); + d_limit = time_point(); + } + else { - ++d_wall_limit.tv_sec; - d_wall_limit.tv_usec -= 1000000; + // set to now() + millis + d_start = clock::now(); + d_limit = d_start + std::chrono::milliseconds(millis); } - Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," - << d_wall_limit.tv_usec << std::endl; } - -/** Return the milliseconds elapsed since last set(). */ -uint64_t Timer::elapsed() const +uint64_t WallClockTimer::elapsed() const { - timeval tv; - gettimeofday(&tv, NULL); - Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," - << tv.tv_usec << std::endl; - tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000; - tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000; - Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec - << "," << tv.tv_usec << std::endl; - return tv.tv_sec * 1000 + tv.tv_usec / 1000; + if (!on()) return 0; + // now() - d_start casted to milliseconds + return std::chrono::duration_cast(clock::now() + - d_start) + .count(); } - -bool Timer::expired() const +bool WallClockTimer::expired() const { + // whether d_limit is in the past if (!on()) return false; - - timeval tv; - gettimeofday(&tv, NULL); - Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec - << "," << tv.tv_usec << std::endl; - Debug("limit") << "Timer::expired(): limit wall time is " - << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec - << std::endl; - if (d_wall_limit.tv_sec < tv.tv_sec - || (d_wall_limit.tv_sec == tv.tv_sec - && d_wall_limit.tv_usec <= tv.tv_usec)) - { - Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl; - return true; - } - Debug("limit") << "Timer::expired(): within limit" << std::endl; - return false; + return d_limit <= clock::now(); } /*---------------------------------------------------------------------------*/ struct ResourceManager::Statistics { + ReferenceStat d_resourceUnitsUsed; + IntStat d_spendResourceCalls; IntStat d_numBitblastStep; IntStat d_numBvEagerAssertStep; IntStat d_numBvPropagationStep; @@ -107,7 +88,9 @@ struct ResourceManager::Statistics }; ResourceManager::Statistics::Statistics(StatisticsRegistry& stats) - : d_numBitblastStep("resource::BitblastStep", 0), + : d_resourceUnitsUsed("resource::resourceUnitsUsed"), + d_spendResourceCalls("resource::spendResourceCalls", 0), + d_numBitblastStep("resource::BitblastStep", 0), d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0), d_numBvPropagationStep("resource::BvPropagationStep", 0), d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0), @@ -123,6 +106,8 @@ ResourceManager::Statistics::Statistics(StatisticsRegistry& stats) d_numTheoryCheckStep("resource::TheoryCheckStep", 0), d_statisticsRegistry(stats) { + d_statisticsRegistry.registerStat(&d_resourceUnitsUsed); + d_statisticsRegistry.registerStat(&d_spendResourceCalls); d_statisticsRegistry.registerStat(&d_numBitblastStep); d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep); d_statisticsRegistry.registerStat(&d_numBvPropagationStep); @@ -141,6 +126,8 @@ ResourceManager::Statistics::Statistics(StatisticsRegistry& stats) ResourceManager::Statistics::~Statistics() { + d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed); + d_statisticsRegistry.unregisterStat(&d_spendResourceCalls); d_statisticsRegistry.unregisterStat(&d_numBitblastStep); d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep); d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep); @@ -169,17 +156,14 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) d_cumulativeTimeUsed(0), d_cumulativeResourceUsed(0), d_thisCallResourceUsed(0), - d_thisCallTimeBudget(0), d_thisCallResourceBudget(0), - d_isHardLimit(), d_on(false), - d_spendResourceCalls(0), - d_hardListeners(), - d_softListeners(), + d_listeners(), d_statistics(new ResourceManager::Statistics(stats)), d_options(options) { + d_statistics->d_resourceUnitsUsed.setData(d_cumulativeResourceUsed); } ResourceManager::~ResourceManager() {} @@ -212,7 +196,7 @@ void ResourceManager::setTimeLimit(uint64_t millis) // perCall timer will be set in beginCall } -const uint64_t& ResourceManager::getResourceUsage() const +uint64_t ResourceManager::getResourceUsage() const { return d_cumulativeResourceUsed; } @@ -227,7 +211,7 @@ uint64_t ResourceManager::getResourceRemaining() const void ResourceManager::spendResource(unsigned amount) { - ++d_spendResourceCalls; + ++d_statistics->d_spendResourceCalls; d_cumulativeResourceUsed += amount; if (!d_on) return; @@ -236,22 +220,14 @@ void ResourceManager::spendResource(unsigned amount) if (out()) { Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; - Trace("limit") << " on call " << d_spendResourceCalls << std::endl; + Trace("limit") << " on call " << d_statistics->d_spendResourceCalls.getData() << std::endl; if (outOfTime()) { Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_perCallTimer.elapsed() << std::endl; } - if (d_isHardLimit) - { - d_hardListeners.notify(); - throw UnsafeInterruptException(); - } - else - { - d_softListeners.notify(); - } + d_listeners.notify(); } } @@ -327,38 +303,18 @@ void ResourceManager::beginCall() d_thisCallResourceUsed = 0; if (!d_on) return; - if (cumulativeLimitOn()) + if (d_resourceBudgetCumulative > 0) { - if (d_resourceBudgetCumulative) - { - d_thisCallResourceBudget = - d_resourceBudgetCumulative <= d_cumulativeResourceUsed - ? 0 - : d_resourceBudgetCumulative - d_cumulativeResourceUsed; - } - // we are out of resources so we shouldn't update the - // budget for this call to the per call budget - if (d_thisCallTimeBudget == 0 || d_thisCallResourceUsed == 0) return; + // Compute remaining cumulative resource budget + d_thisCallResourceBudget = + d_resourceBudgetCumulative - d_cumulativeResourceUsed; } - - if (perCallLimitOn()) + if (d_resourceBudgetPerCall > 0) { - // take min of what's left and per-call budget - if (d_resourceBudgetPerCall) - { - d_thisCallResourceBudget = - d_thisCallResourceBudget < d_resourceBudgetPerCall - && d_thisCallResourceBudget != 0 - ? d_thisCallResourceBudget - : d_resourceBudgetPerCall; - } - - if (d_timeBudgetPerCall) + // Check if per-call resource budget is even smaller + if (d_resourceBudgetPerCall < d_thisCallResourceBudget) { - d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall - && d_thisCallTimeBudget != 0 - ? d_thisCallTimeBudget - : d_timeBudgetPerCall; + d_thisCallResourceBudget = d_resourceBudgetPerCall; } } } @@ -367,56 +323,56 @@ void ResourceManager::endCall() { d_cumulativeTimeUsed += d_perCallTimer.elapsed(); d_perCallTimer.set(0); + d_thisCallResourceUsed = 0; } bool ResourceManager::cumulativeLimitOn() const { - return d_resourceBudgetCumulative; + return d_resourceBudgetCumulative > 0; } bool ResourceManager::perCallLimitOn() const { - return d_timeBudgetPerCall || d_resourceBudgetPerCall; + return (d_timeBudgetPerCall > 0) || (d_resourceBudgetPerCall > 0); } bool ResourceManager::outOfResources() const { - // resource limiting not enabled - if (d_resourceBudgetPerCall == 0 && d_resourceBudgetCumulative == 0) - return false; - - return getResourceRemaining() == 0; + if (d_resourceBudgetPerCall > 0) + { + // Check if per-call resources are exhausted + if (d_thisCallResourceUsed >= d_resourceBudgetPerCall) + { + return true; + } + } + if (d_resourceBudgetCumulative > 0) + { + // Check if cumulative resources are exhausted + if (d_cumulativeResourceUsed >= d_resourceBudgetCumulative) + { + return true; + } + } + return false; } bool ResourceManager::outOfTime() const { if (d_timeBudgetPerCall == 0) return false; - return d_perCallTimer.expired(); } -void ResourceManager::setHardLimit(bool value) -{ - Trace("limit") << "ResourceManager::setHardLimit(" << value << ")\n"; - d_isHardLimit = value; -} - void ResourceManager::enable(bool on) { Trace("limit") << "ResourceManager::enable(" << on << ")\n"; d_on = on; } -ListenerCollection::Registration* ResourceManager::registerHardListener( - Listener* listener) -{ - return d_hardListeners.registerListener(listener); -} - -ListenerCollection::Registration* ResourceManager::registerSoftListener( +ListenerCollection::Registration* ResourceManager::registerListener( Listener* listener) { - return d_softListeners.registerListener(listener); + return d_listeners.registerListener(listener); } } /* namespace CVC4 */ diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 822f17713..57a227d7b 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -23,6 +23,7 @@ #include +#include #include #include @@ -36,36 +37,48 @@ namespace CVC4 { class StatisticsRegistry; /** - * A helper class to keep track of a time budget and signal - * the PropEngine when the budget expires. + * This class implements a easy to use wall clock timer based on std::chrono. */ -class CVC4_PUBLIC Timer +class CVC4_PUBLIC WallClockTimer { - public: - /** Construct a Timer. */ - Timer() : d_ms(0) - { - d_wall_limit.tv_sec = 0; - d_wall_limit.tv_usec = 0; - } - - /** Is the timer currently active? */ - bool on() const { return d_ms != 0; } + /** + * The underlying clock that is used. + * std::chrono::system_clock represents wall clock time. + */ + using clock = std::chrono::system_clock; + /** A time point of the clock we use. */ + using time_point = std::chrono::time_point; - /** Set a millisecond timer (0==off). */ + public: + /** Checks whether this timer is active. */ + bool on() const; + /** + * Activates this timer with a timeout in milliseconds. + * If millis is zero, the timer is deactivated. + */ void set(uint64_t millis); - /** Return the milliseconds elapsed since last set() wall time. */ + /** Returns the number of elapsed milliseconds since the last call to set(). + */ uint64_t elapsed() const; + /** Checks whether the current timeout has expired. */ bool expired() const; private: - uint64_t d_ms; - timeval d_wall_limit; -}; /* class Timer */ + /** The start of this timer. */ + time_point d_start; + /** The point in time when this timer expires. */ + time_point d_limit; +}; +/** + * This class manages resource limits (cumulative or per call) and (per call) + * time limits. The available resources are listed in ResourceManager::Resource + * and their individual costs are configured via command line options. + */ class CVC4_PUBLIC ResourceManager { public: + /** Types of resources. */ enum class Resource { BitblastStep, @@ -84,32 +97,54 @@ class CVC4_PUBLIC ResourceManager TheoryCheckStep, }; + /** Construst a resource manager. */ ResourceManager(StatisticsRegistry& statistics_registry, Options& options); + /** Default destructor. */ ~ResourceManager(); + /** Can not be copied. */ + ResourceManager(const ResourceManager&) = delete; + /** Can not be moved. */ + ResourceManager(ResourceManager&&) = delete; + /** Can not be copied. */ + ResourceManager& operator=(const ResourceManager&) = delete; + /** Can not be moved. */ + ResourceManager& operator=(ResourceManager&&) = delete; + /** Checks whether any limit is active. */ bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); } + /** Checks whether any cumulative limit is active. */ bool cumulativeLimitOn() const; + /** Checks whether any per-call limit is active. */ bool perCallLimitOn() const; + /** Checks whether resources have been exhausted. */ bool outOfResources() const; + /** Checks whether time has been exhausted. */ bool outOfTime() const; + /** Checks whether any limit has been exhausted. */ bool out() const { return d_on && (outOfResources() || outOfTime()); } - /** - * This returns a const uint64_t& to support being used as a ReferenceStat. - */ - const uint64_t& getResourceUsage() const; + /** Retrieves amount of resources used overall. */ + uint64_t getResourceUsage() const; + /** Retrieves time used over all calls. */ uint64_t getTimeUsage() const; + /** Retrieves the remaining number of cumulative resources. */ uint64_t getResourceRemaining() const; + /** Retrieves resource budget for this call. */ uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; } - // Throws an UnsafeInterruptException if there are no remaining resources. + + /** + * Spends a given resources. Throws an UnsafeInterruptException if there are + * no remaining resources. + */ void spendResource(Resource r); - void setHardLimit(bool value); + /** Sets the resource limit. */ void setResourceLimit(uint64_t units, bool cumulative = false); + /** Sets the time limit. */ void setTimeLimit(uint64_t millis); - + /** Sets whether resource limitation is enabled. */ void enable(bool on); /** @@ -127,23 +162,16 @@ class CVC4_PUBLIC ResourceManager static uint64_t getFrequencyCount() { return s_resourceCount; } /** - * Registers a listener that is notified on a hard resource out. + * Registers a listener that is notified on a resource out. * * This Registration must be destroyed by the user before this * ResourceManager. */ - ListenerCollection::Registration* registerHardListener(Listener* listener); - - /** - * Registers a listener that is notified on a soft resource out. - * - * This Registration must be destroyed by the user before this - * ResourceManager. - */ - ListenerCollection::Registration* registerSoftListener(Listener* listener); + ListenerCollection::Registration* registerListener(Listener* listener); private: - Timer d_perCallTimer; + /** The per-call wall clock timer. */ + WallClockTimer d_perCallTimer; /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ uint64_t d_timeBudgetPerCall; @@ -152,45 +180,28 @@ class CVC4_PUBLIC ResourceManager /** A user-imposed per-call resource budget. 0 = no limit. */ uint64_t d_resourceBudgetPerCall; - /** The number of milliseconds used. */ + /** The total number of milliseconds used. */ uint64_t d_cumulativeTimeUsed; - /** The amount of resource used. */ + /** The total amount of resources used. */ uint64_t d_cumulativeResourceUsed; - /** The amount of resource used during this call. */ + /** The amount of resources used during this call. */ uint64_t d_thisCallResourceUsed; /** - * The amount of resource budget for this call (min between per call - * budget and left-over cumulative budget. + * The resource budget for this call (min between per call + * budget and left-over cumulative budget.) */ - uint64_t d_thisCallTimeBudget; uint64_t d_thisCallResourceBudget; - bool d_isHardLimit; + /** A flag indicating whether resource limitation is active. */ bool d_on; - uint64_t d_spendResourceCalls; /** Counter indicating how often to check resource manager in loops */ static const uint64_t s_resourceCount; - /** Receives a notification on reaching a hard limit. */ - ListenerCollection d_hardListeners; - - /** Receives a notification on reaching a hard limit. */ - ListenerCollection d_softListeners; - - /** - * ResourceManagers cannot be copied as they are given an explicit - * list of Listeners to respond to. - */ - ResourceManager(const ResourceManager&) = delete; - - /** - * ResourceManagers cannot be assigned as they are given an explicit - * list of Listeners to respond to. - */ - ResourceManager& operator=(const ResourceManager&) = delete; + /** Receives a notification on reaching a limit. */ + ListenerCollection d_listeners; void spendResource(unsigned amount);