1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
/********************* */
/*! \file resource_manager.h
** \verbatim
** Top contributors (to current version):
** Liana Hadarean, Tim King, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#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 {
public:
/** Construct a Timer. */
Timer()
: d_ms(0),
d_cpu_start_time(0),
d_cpu_limit(0),
d_wall_time(true)
{
d_wall_limit.tv_sec = 0;
d_wall_limit.tv_usec = 0;
}
/** 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;
private:
/** 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;
uint64_t d_ms;
clock_t d_cpu_start_time;
clock_t d_cpu_limit;
bool d_wall_time;
timeval d_wall_limit;
};/* 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 amount of resource 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.
*/
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;
/**
* ResourceManagers cannot be copied as they are given an explicit
* list of Listeners to respond to.
*/
ResourceManager(const ResourceManager&) CVC4_UNDEFINED;
/**
* ResourceManagers cannot be assigned as they are given an explicit
* list of Listeners to respond to.
*/
ResourceManager& operator=(const ResourceManager&) CVC4_UNDEFINED;
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;
}
// Throws an UnsafeInterruptException if there are no remaining resources.
void spendResource(unsigned amount);
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; }
/**
* Registers a listener that is notified on a hard 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);
};/* class ResourceManager */
}/* CVC4 namespace */
#endif /* __CVC4__RESOURCE_MANAGER_H */
|
