diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/util/resource_manager.h | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/util/resource_manager.h')
-rw-r--r-- | src/util/resource_manager.h | 158 |
1 files changed, 158 insertions, 0 deletions
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 <cstddef> +#include <sys/time.h> + +#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 */ |