diff options
author | Tim King <taking@google.com> | 2016-01-08 18:19:30 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-08 18:19:30 -0800 |
commit | 3a973bd4fb586707a20d5e73146b79ff9fd6a77a (patch) | |
tree | 506d13a137c620751d350bf03ed2c888656e9918 /src/util | |
parent | f4ef7af0a2295691f281ee1604dfeb4082fe229c (diff) |
Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/resource_manager.cpp | 292 | ||||
-rw-r--r-- | src/util/resource_manager.h | 174 | ||||
-rw-r--r-- | src/util/resource_manager.i | 5 |
4 files changed, 474 insertions, 0 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e1c593243..e95faea56 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -43,6 +43,8 @@ libutil_la_SOURCES = \ proof.h \ regexp.cpp \ regexp.h \ + resource_manager.cpp \ + resource_manager.h \ result.cpp \ result.h \ sexpr.cpp \ @@ -97,6 +99,7 @@ EXTRA_DIST = \ rational_gmp_imp.cpp \ rational_gmp_imp.h \ regexp.i \ + resource_manager.i \ result.i \ sexpr.i \ statistics.i \ diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp new file mode 100644 index 000000000..d426ab03e --- /dev/null +++ b/src/util/resource_manager.cpp @@ -0,0 +1,292 @@ +/********************* */ +/*! \file resource_manager.cpp +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): none +** This file is part of the CVC4 project. +** Copyright (c) 2009-2014 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Manages and updates various resource and time limits. +** +** Manages and updates various resource and time limits. +**/ +#include "util/resource_manager.h" + +#include "base/cvc4_assert.h" +#include "base/output.h" + +using namespace std; + +namespace CVC4 { + +void Timer::set(uint64_t millis, bool wallTime) { + 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) + d_wall_time = wallTime; + if (d_wall_time) { + // 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) { + ++d_wall_limit.tv_sec; + d_wall_limit.tv_usec -= 1000000; + } + Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + } else { + // CPU time + d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001); + d_cpu_limit = d_cpu_start_time + d_ms; + } +} + +/** Return the milliseconds elapsed since last set(). */ +uint64_t Timer::elapsedWall() const { + Assert (d_wall_time); + 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; +} + +uint64_t Timer::elapsedCPU() const { + Assert (!d_wall_time); + clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time; + Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <<std::endl; + return elapsed; +} + +uint64_t Timer::elapsed() const { + if (d_wall_time) + return elapsedWall(); + return elapsedCPU(); +} + +bool Timer::expired() const { + if (!on()) return false; + + if (d_wall_time) { + 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; + } + + // cpu time + double current = ((double)clock())/(CLOCKS_PER_SEC*0.001); + Debug("limit") << "Timer::expired(): current cpu time is " << current << std::endl; + Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit << std::endl; + if (current >= d_cpu_limit) { + Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl; + return true; + } + return false; +} + +const uint64_t ResourceManager::s_resourceCount = 1000; + +ResourceManager::ResourceManager() + : d_cumulativeTimer() + , d_perCallTimer() + , d_timeBudgetCumulative(0) + , d_timeBudgetPerCall(0) + , d_resourceBudgetCumulative(0) + , d_resourceBudgetPerCall(0) + , d_cumulativeTimeUsed(0) + , d_cumulativeResourceUsed(0) + , d_thisCallResourceUsed(0) + , d_thisCallTimeBudget(0) + , d_thisCallResourceBudget(0) + , d_isHardLimit() + , d_on(false) + , d_cpuTime(false) + , d_spendResourceCalls(0) + , d_hardListeners() + , d_softListeners() +{} + + +void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl; + d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); + d_thisCallResourceBudget = d_resourceBudgetCumulative; + } else { + Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl; + d_resourceBudgetPerCall = units; + } +} + +void ResourceManager::setTimeLimit(uint64_t millis, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl; + d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); + d_cumulativeTimer.set(millis, !d_cpuTime); + } else { + Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl; + d_timeBudgetPerCall = millis; + // perCall timer will be set in beginCall + } + +} + +const uint64_t& ResourceManager::getResourceUsage() const { + return d_cumulativeResourceUsed; +} + +uint64_t ResourceManager::getTimeUsage() const { + if (d_timeBudgetCumulative) { + return d_cumulativeTimer.elapsed(); + } + return d_cumulativeTimeUsed; +} + +uint64_t ResourceManager::getResourceRemaining() const { + if (d_thisCallResourceBudget <= d_thisCallResourceUsed) + return 0; + return d_thisCallResourceBudget - d_thisCallResourceUsed; +} + +uint64_t ResourceManager::getTimeRemaining() const { + uint64_t time_passed = d_cumulativeTimer.elapsed(); + if (time_passed >= d_thisCallTimeBudget) + return 0; + return d_thisCallTimeBudget - time_passed; +} + +void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) { + ++d_spendResourceCalls; + d_cumulativeResourceUsed += ammount; + if (!d_on) return; + + Debug("limit") << "ResourceManager::spendResource()" << std::endl; + d_thisCallResourceUsed += ammount; + if(out()) { + Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; + Trace("limit") << " on call " << d_spendResourceCalls << std::endl; + if (outOfTime()) { + Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl; + } + + if (d_isHardLimit) { + d_hardListeners.notify(); + throw UnsafeInterruptException(); + } else { + d_softListeners.notify(); + } + + } +} + +void ResourceManager::beginCall() { + + d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime); + d_thisCallResourceUsed = 0; + if (!d_on) return; + + if (cumulativeLimitOn()) { + if (d_resourceBudgetCumulative) { + d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 : + d_resourceBudgetCumulative - d_cumulativeResourceUsed; + } + + if (d_timeBudgetCumulative) { + + AlwaysAssert(d_cumulativeTimer.on()); + // timer was on since the option was set + d_cumulativeTimeUsed = d_cumulativeTimer.elapsed(); + d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 : + d_timeBudgetCumulative - d_cumulativeTimeUsed; + d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime); + } + // 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; + } + + if (perCallLimitOn()) { + // 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) { + d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall; + } + } +} + +void ResourceManager::endCall() { + uint64_t usedInCall = d_perCallTimer.elapsed(); + d_perCallTimer.set(0); + d_cumulativeTimeUsed += usedInCall; +} + +bool ResourceManager::cumulativeLimitOn() const { + return d_timeBudgetCumulative || d_resourceBudgetCumulative; +} + +bool ResourceManager::perCallLimitOn() const { + return d_timeBudgetPerCall || d_resourceBudgetPerCall; +} + +bool ResourceManager::outOfResources() const { + // resource limiting not enabled + if (d_resourceBudgetPerCall == 0 && + d_resourceBudgetCumulative == 0) + return false; + + return getResourceRemaining() == 0; +} + +bool ResourceManager::outOfTime() const { + if (d_timeBudgetPerCall == 0 && + d_timeBudgetCumulative == 0) + return false; + + return d_cumulativeTimer.expired() || d_perCallTimer.expired(); +} + +void ResourceManager::useCPUTime(bool cpu) { + Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n"; + d_cpuTime = cpu; +} + +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* ResourceManager::getHardListeners() { + return &d_hardListeners; +} + +ListenerCollection* ResourceManager::getSoftListeners() { + return &d_softListeners; +} + +} /* namespace CVC4 */ diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h new file mode 100644 index 000000000..2c54011a5 --- /dev/null +++ b/src/util/resource_manager.h @@ -0,0 +1,174 @@ +/********************* */ +/*! \file resource_manager.h +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): none +** This file is part of the CVC4 project. +** Copyright (c) 2009-2014 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Manages and updates various resource and time limits +** +** Manages and updates various resource and time limits. +**/ + +#include "cvc4_public.h" + +#ifndef __CVC4__RESOURCE_MANAGER_H +#define __CVC4__RESOURCE_MANAGER_H + +#include <cstddef> +#include <sys/time.h> + +#include "base/exception.h" +#include "base/listener.h" +#include "util/unsafe_interrupt_exception.h" + +namespace CVC4 { + +/** + * A helper class to keep track of a time budget and signal + * the PropEngine when the budget expires. + */ +class CVC4_PUBLIC Timer { + + uint64_t d_ms; + timeval d_wall_limit; + clock_t d_cpu_start_time; + clock_t d_cpu_limit; + + bool d_wall_time; + + /** Return the milliseconds elapsed since last set() cpu time. */ + uint64_t elapsedCPU() const; + /** Return the milliseconds elapsed since last set() wall time. */ + uint64_t elapsedWall() const; + +public: + + /** Construct a Timer. */ + Timer() + : d_ms(0) + , d_cpu_start_time(0) + , d_cpu_limit(0) + , d_wall_time(true) + {} + + /** Is the timer currently active? */ + bool on() const { + return d_ms != 0; + } + + /** Set a millisecond timer (0==off). */ + void set(uint64_t millis, bool wall_time = true); + /** Return the milliseconds elapsed since last set() wall/cpu time + depending on d_wall_time*/ + uint64_t elapsed() const; + bool expired() const; + +};/* class Timer */ + + +class CVC4_PUBLIC ResourceManager { + + Timer d_cumulativeTimer; + Timer d_perCallTimer; + + /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */ + uint64_t d_timeBudgetCumulative; + /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ + uint64_t d_timeBudgetPerCall; + /** A user-imposed cumulative resource budget. 0 = no limit. */ + uint64_t d_resourceBudgetCumulative; + /** A user-imposed per-call resource budget. 0 = no limit. */ + uint64_t d_resourceBudgetPerCall; + + /** The number of milliseconds used. */ + uint64_t d_cumulativeTimeUsed; + /** The amount of resource used. */ + uint64_t d_cumulativeResourceUsed; + + /** The ammount of resource used during this call. */ + uint64_t d_thisCallResourceUsed; + + /** + * The ammount of 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; + bool d_on; + bool d_cpuTime; + 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; + +public: + + ResourceManager(); + + bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); } + bool cumulativeLimitOn() const; + bool perCallLimitOn() const; + + bool outOfResources() const; + bool outOfTime() const; + 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; + uint64_t getTimeUsage() const; + uint64_t getResourceRemaining() const; + uint64_t getTimeRemaining() const; + + uint64_t getResourceBudgetForThisCall() { + return d_thisCallResourceBudget; + } + + void spendResource(unsigned ammount) throw(UnsafeInterruptException); + + void setHardLimit(bool value); + void setResourceLimit(uint64_t units, bool cumulative = false); + void setTimeLimit(uint64_t millis, bool cumulative = false); + void useCPUTime(bool cpu); + + void enable(bool on); + + /** + * Resets perCall limits to mark the start of a new call, + * updates budget for current call and starts the timer + */ + void beginCall(); + + /** + * Marks the end of a SmtEngine check call, stops the per + * call timer, updates cumulative time used. + */ + void endCall(); + + static uint64_t getFrequencyCount() { return s_resourceCount; } + + /** Collection of listeners that are notified on a hard resource out. */ + ListenerCollection* getHardListeners(); + + /** Collection of listeners that are notified on a soft resource out. */ + ListenerCollection* getSoftListeners(); +};/* class ResourceManager */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__RESOURCE_MANAGER_H */ diff --git a/src/util/resource_manager.i b/src/util/resource_manager.i new file mode 100644 index 000000000..0f55c2bce --- /dev/null +++ b/src/util/resource_manager.i @@ -0,0 +1,5 @@ +%{ +#include "util/resource_manager.h" +%} + +%include "util/resource_manager.h" |