From 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Mon, 17 Nov 2014 15:26:42 -0500 Subject: Resource-limiting work. Signed-off-by: Morgan Deters --- src/util/Makefile.am | 6 +- src/util/resource_manager.cpp | 285 ++++++++++++++++++++++++++++++++++ src/util/resource_manager.h | 158 +++++++++++++++++++ src/util/resource_manager.i | 5 + src/util/unsafe_interrupt_exception.h | 43 +++++ src/util/unsafe_interrupt_exception.i | 7 + 6 files changed, 503 insertions(+), 1 deletion(-) create mode 100644 src/util/resource_manager.cpp create mode 100644 src/util/resource_manager.h create mode 100644 src/util/resource_manager.i create mode 100644 src/util/unsafe_interrupt_exception.h create mode 100644 src/util/unsafe_interrupt_exception.i (limited to 'src/util') diff --git a/src/util/Makefile.am b/src/util/Makefile.am index fc9192dd9..a6543391d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -99,7 +99,10 @@ libutil_la_SOURCES = \ didyoumean.h \ didyoumean.cpp \ unsat_core.h \ - unsat_core.cpp + unsat_core.cpp \ + resource_manager.h \ + resource_manager.cpp \ + unsafe_interrupt_exception.h libstatistics_la_SOURCES = \ statistics_registry.h \ @@ -158,6 +161,7 @@ EXTRA_DIST = \ uninterpreted_constant.i \ chain.i \ regexp.i \ + resource_manager.i \ proof.i \ unsat_core.i diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp new file mode 100644 index 000000000..2aca55616 --- /dev/null +++ b/src/util/resource_manager.cpp @@ -0,0 +1,285 @@ +/********************* */ +/*! \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 "util/resource_manager.h" +#include "util/output.h" +#include "smt/smt_engine_scope.h" +#include "smt/options.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace std; + +void Timer::set(unsigned long 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(). */ +unsigned long 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; +} + +unsigned long 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" <= d_cpu_limit) { + Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl; + return true; + } + return false; +} + +const unsigned long 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) +{} + + +void ResourceManager::setResourceLimit(unsigned long 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(unsigned long 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 + } + +} + +unsigned long ResourceManager::getResourceUsage() const { + return d_cumulativeResourceUsed; +} + +unsigned long ResourceManager::getTimeUsage() const { + if (d_timeBudgetCumulative) { + return d_cumulativeTimer.elapsed(); + } + return d_cumulativeTimeUsed; +} + +unsigned long ResourceManager::getResourceRemaining() const { + if (d_thisCallResourceBudget <= d_thisCallResourceUsed) + return 0; + return d_thisCallResourceBudget - d_thisCallResourceUsed; +} + +unsigned long ResourceManager::getTimeRemaining() const { + unsigned long time_passed = d_cumulativeTimer.elapsed(); + if (time_passed >= d_thisCallTimeBudget) + return 0; + return d_thisCallTimeBudget - time_passed; +} + +void ResourceManager::spendResource() throw (UnsafeInterruptException) { + ++d_spendResourceCalls; + if (!d_on) return; + + Debug("limit") << "ResourceManager::spendResource()" << std::endl; + ++d_cumulativeResourceUsed; + ++d_thisCallResourceUsed; + 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 (smt::smtEngineInScope()) { + theory::Rewriter::clearCaches(); + } + if (d_isHardLimit) { + throw UnsafeInterruptException(); + } + + // interrupt it next time resources are checked + if (smt::smtEngineInScope()) { + smt::currentSmtEngine()->interrupt(); + } + } +} + +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() { + unsigned long 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; +} diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h new file mode 100644 index 000000000..a16f60910 --- /dev/null +++ b/src/util/resource_manager.h @@ -0,0 +1,158 @@ +/********************* */ +/*! \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 +#include + +#include "util/exception.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 { + + unsigned long 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. */ + unsigned long elapsedCPU() const; + /** Return the milliseconds elapsed since last set() wall time. */ + unsigned long 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(unsigned long millis, bool wall_time = true); + /** Return the milliseconds elapsed since last set() wall/cpu time + depending on d_wall_time*/ + unsigned long 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. */ + unsigned long d_timeBudgetCumulative; + /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ + unsigned long d_timeBudgetPerCall; + /** A user-imposed cumulative resource budget. 0 = no limit. */ + unsigned long d_resourceBudgetCumulative; + /** A user-imposed per-call resource budget. 0 = no limit. */ + unsigned long d_resourceBudgetPerCall; + + /** The number of milliseconds used. */ + unsigned long d_cumulativeTimeUsed; + /** The amount of resource used. */ + unsigned long d_cumulativeResourceUsed; + + /** The ammount of resource used during this call. */ + unsigned long d_thisCallResourceUsed; + + /** + * The ammount of resource budget for this call (min between per call + * budget and left-over cumulative budget. + */ + unsigned long d_thisCallTimeBudget; + unsigned long d_thisCallResourceBudget; + + bool d_isHardLimit; + bool d_on; + bool d_cpuTime; + unsigned long d_spendResourceCalls; + + /** Counter indicating how often to check resource manager in loops */ + static const unsigned long s_resourceCount; + +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()); } + + unsigned long getResourceUsage() const; + unsigned long getTimeUsage() const; + unsigned long getResourceRemaining() const; + unsigned long getTimeRemaining() const; + + unsigned long getResourceBudgetForThisCall() { + return d_thisCallResourceBudget; + } + + void spendResource() throw(UnsafeInterruptException); + + void setHardLimit(bool value); + void setResourceLimit(unsigned long units, bool cumulative = false); + void setTimeLimit(unsigned long 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 unsigned long getFrequencyCount() { return s_resourceCount; } + +};/* 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" diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h new file mode 100644 index 000000000..e19fc37ce --- /dev/null +++ b/src/util/unsafe_interrupt_exception.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file modal_exception.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 An exception that is thrown when the solver is out of time/resources + ** and is interrupted in an unsafe state + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H +#define __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC UnsafeInterruptException : public CVC4::Exception { +public: + UnsafeInterruptException() : + Exception("Interrupted in unsafe state due to " + "time/resource limit.") { + } + + UnsafeInterruptException(const std::string& msg) : + Exception(msg) { + } + + UnsafeInterruptException(const char* msg) : + Exception(msg) { + } +};/* class UnsafeInterruptException */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */ diff --git a/src/util/unsafe_interrupt_exception.i b/src/util/unsafe_interrupt_exception.i new file mode 100644 index 000000000..94a552877 --- /dev/null +++ b/src/util/unsafe_interrupt_exception.i @@ -0,0 +1,7 @@ +%{ +#include "util/unsafe_interrupt_exception.h" +%} + +%ignore CVC4::UnsafeInterruptException::UnsafeInterruptException(const char*); + +%include "util/unsafe_interrupt_exception.h" -- cgit v1.2.3