GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/resource_manager.cpp Lines: 176 228 77.2 %
Date: 2021-03-22 Branches: 113 294 38.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file resource_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Mathias Preiner, Liana Hadarean
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** [[ Add lengthier description here ]]
13
14
 ** \todo document this file
15
16
**/
17
#include "util/resource_manager.h"
18
19
#include <algorithm>
20
#include <ostream>
21
22
#include "base/check.h"
23
#include "base/listener.h"
24
#include "base/output.h"
25
#include "options/options.h"
26
#include "options/smt_options.h"
27
#include "util/statistics_registry.h"
28
29
using namespace std;
30
31
namespace CVC4 {
32
33
20216
bool WallClockTimer::on() const
34
{
35
  // default-constructed time points are at the respective epoch
36
20216
  return d_limit.time_since_epoch().count() != 0;
37
}
38
24832
void WallClockTimer::set(uint64_t millis)
39
{
40
24832
  if (millis == 0)
41
  {
42
    // reset / deactivate
43
24821
    d_start = time_point();
44
24821
    d_limit = time_point();
45
  }
46
  else
47
  {
48
    // set to now() + millis
49
11
    d_start = clock::now();
50
11
    d_limit = d_start + std::chrono::milliseconds(millis);
51
  }
52
24832
}
53
12399
uint64_t WallClockTimer::elapsed() const
54
{
55
12399
  if (!on()) return 0;
56
  // now() - d_start casted to milliseconds
57
44
  return std::chrono::duration_cast<std::chrono::milliseconds>(clock::now()
58
33
                                                               - d_start)
59
11
      .count();
60
}
61
7817
bool WallClockTimer::expired() const
62
{
63
  // whether d_limit is in the past
64
7817
  if (!on()) return false;
65
2831
  return d_limit <= clock::now();
66
}
67
68
/*---------------------------------------------------------------------------*/
69
70
struct ResourceManager::Statistics
71
{
72
  ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
73
  IntStat d_spendResourceCalls;
74
  IntStat d_numArithPivotStep;
75
  IntStat d_numArithNlLemmaStep;
76
  IntStat d_numBitblastStep;
77
  IntStat d_numBvEagerAssertStep;
78
  IntStat d_numBvPropagationStep;
79
  IntStat d_numBvSatConflictsStep;
80
  IntStat d_numBvSatPropagateStep;
81
  IntStat d_numBvSatSimplifyStep;
82
  IntStat d_numCnfStep;
83
  IntStat d_numDecisionStep;
84
  IntStat d_numLemmaStep;
85
  IntStat d_numNewSkolemStep;
86
  IntStat d_numParseStep;
87
  IntStat d_numPreprocessStep;
88
  IntStat d_numQuantifierStep;
89
  IntStat d_numRestartStep;
90
  IntStat d_numRewriteStep;
91
  IntStat d_numSatConflictStep;
92
  IntStat d_numTheoryCheckStep;
93
  Statistics(StatisticsRegistry& stats);
94
  ~Statistics();
95
96
 private:
97
  StatisticsRegistry& d_statisticsRegistry;
98
};
99
100
9620
ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
101
    : d_resourceUnitsUsed("resource::resourceUnitsUsed"),
102
      d_spendResourceCalls("resource::spendResourceCalls", 0),
103
      d_numArithPivotStep("resource::ArithPivotStep", 0),
104
      d_numArithNlLemmaStep("resource::ArithNlLemmaStep", 0),
105
      d_numBitblastStep("resource::BitblastStep", 0),
106
      d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
107
      d_numBvPropagationStep("resource::BvPropagationStep", 0),
108
      d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
109
      d_numBvSatPropagateStep("resource::BvSatPropagateStep", 0),
110
      d_numBvSatSimplifyStep("resource::BvSatSimplifyStep", 0),
111
      d_numCnfStep("resource::CnfStep", 0),
112
      d_numDecisionStep("resource::DecisionStep", 0),
113
      d_numLemmaStep("resource::LemmaStep", 0),
114
      d_numNewSkolemStep("resource::NewSkolemStep", 0),
115
      d_numParseStep("resource::ParseStep", 0),
116
      d_numPreprocessStep("resource::PreprocessStep", 0),
117
      d_numQuantifierStep("resource::QuantifierStep", 0),
118
      d_numRestartStep("resource::RestartStep", 0),
119
      d_numRewriteStep("resource::RewriteStep", 0),
120
      d_numSatConflictStep("resource::SatConflictStep", 0),
121
      d_numTheoryCheckStep("resource::TheoryCheckStep", 0),
122
9620
      d_statisticsRegistry(stats)
123
{
124
9620
  d_statisticsRegistry.registerStat(&d_resourceUnitsUsed);
125
9620
  d_statisticsRegistry.registerStat(&d_spendResourceCalls);
126
9620
  d_statisticsRegistry.registerStat(&d_numArithPivotStep);
127
9620
  d_statisticsRegistry.registerStat(&d_numArithNlLemmaStep);
128
9620
  d_statisticsRegistry.registerStat(&d_numBitblastStep);
129
9620
  d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
130
9620
  d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
131
9620
  d_statisticsRegistry.registerStat(&d_numBvSatConflictsStep);
132
9620
  d_statisticsRegistry.registerStat(&d_numBvSatPropagateStep);
133
9620
  d_statisticsRegistry.registerStat(&d_numBvSatSimplifyStep);
134
9620
  d_statisticsRegistry.registerStat(&d_numCnfStep);
135
9620
  d_statisticsRegistry.registerStat(&d_numDecisionStep);
136
9620
  d_statisticsRegistry.registerStat(&d_numLemmaStep);
137
9620
  d_statisticsRegistry.registerStat(&d_numNewSkolemStep);
138
9620
  d_statisticsRegistry.registerStat(&d_numParseStep);
139
9620
  d_statisticsRegistry.registerStat(&d_numPreprocessStep);
140
9620
  d_statisticsRegistry.registerStat(&d_numQuantifierStep);
141
9620
  d_statisticsRegistry.registerStat(&d_numRestartStep);
142
9620
  d_statisticsRegistry.registerStat(&d_numRewriteStep);
143
9620
  d_statisticsRegistry.registerStat(&d_numSatConflictStep);
144
9620
  d_statisticsRegistry.registerStat(&d_numTheoryCheckStep);
145
9620
}
146
147
19198
ResourceManager::Statistics::~Statistics()
148
{
149
9599
  d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
150
9599
  d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
151
9599
  d_statisticsRegistry.unregisterStat(&d_numArithPivotStep);
152
9599
  d_statisticsRegistry.unregisterStat(&d_numArithNlLemmaStep);
153
9599
  d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
154
9599
  d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
155
9599
  d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
156
9599
  d_statisticsRegistry.unregisterStat(&d_numBvSatConflictsStep);
157
9599
  d_statisticsRegistry.unregisterStat(&d_numBvSatPropagateStep);
158
9599
  d_statisticsRegistry.unregisterStat(&d_numBvSatSimplifyStep);
159
9599
  d_statisticsRegistry.unregisterStat(&d_numCnfStep);
160
9599
  d_statisticsRegistry.unregisterStat(&d_numDecisionStep);
161
9599
  d_statisticsRegistry.unregisterStat(&d_numLemmaStep);
162
9599
  d_statisticsRegistry.unregisterStat(&d_numNewSkolemStep);
163
9599
  d_statisticsRegistry.unregisterStat(&d_numParseStep);
164
9599
  d_statisticsRegistry.unregisterStat(&d_numPreprocessStep);
165
9599
  d_statisticsRegistry.unregisterStat(&d_numQuantifierStep);
166
9599
  d_statisticsRegistry.unregisterStat(&d_numRestartStep);
167
9599
  d_statisticsRegistry.unregisterStat(&d_numRewriteStep);
168
9599
  d_statisticsRegistry.unregisterStat(&d_numSatConflictStep);
169
9599
  d_statisticsRegistry.unregisterStat(&d_numTheoryCheckStep);
170
9599
}
171
172
/*---------------------------------------------------------------------------*/
173
174
9620
ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
175
    : d_perCallTimer(),
176
      d_timeBudgetPerCall(0),
177
      d_resourceBudgetCumulative(0),
178
      d_resourceBudgetPerCall(0),
179
      d_cumulativeTimeUsed(0),
180
      d_cumulativeResourceUsed(0),
181
      d_thisCallResourceUsed(0),
182
      d_thisCallResourceBudget(0),
183
      d_on(false),
184
9620
      d_statistics(new ResourceManager::Statistics(stats)),
185
19240
      d_options(options)
186
187
{
188
9620
  d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);
189
9620
}
190
191
9599
ResourceManager::~ResourceManager() {}
192
193
void ResourceManager::setResourceLimit(uint64_t units, bool cumulative)
194
{
195
  d_on = true;
196
  if (cumulative)
197
  {
198
    Trace("limit") << "ResourceManager: setting cumulative resource limit to "
199
                   << units << endl;
200
    d_resourceBudgetCumulative =
201
        (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
202
    d_thisCallResourceBudget = d_resourceBudgetCumulative;
203
  }
204
  else
205
  {
206
    Trace("limit") << "ResourceManager: setting per-call resource limit to "
207
                   << units << endl;
208
    d_resourceBudgetPerCall = units;
209
  }
210
}
211
212
7
void ResourceManager::setTimeLimit(uint64_t millis)
213
{
214
7
  d_on = true;
215
14
  Trace("limit") << "ResourceManager: setting per-call time limit to " << millis
216
7
                 << " ms" << endl;
217
7
  d_timeBudgetPerCall = millis;
218
  // perCall timer will be set in beginCall
219
7
}
220
221
12399
uint64_t ResourceManager::getResourceUsage() const
222
{
223
12399
  return d_cumulativeResourceUsed;
224
}
225
226
12399
uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
227
228
uint64_t ResourceManager::getResourceRemaining() const
229
{
230
  if (d_resourceBudgetCumulative <= d_cumulativeResourceUsed) return 0;
231
  return d_resourceBudgetCumulative - d_cumulativeResourceUsed;
232
}
233
234
114510498
void ResourceManager::spendResource(unsigned amount)
235
{
236
114510498
  ++d_statistics->d_spendResourceCalls;
237
114510498
  d_cumulativeResourceUsed += amount;
238
114510498
  if (!d_on) return;
239
240
7806
  Debug("limit") << "ResourceManager::spendResource()" << std::endl;
241
7806
  d_thisCallResourceUsed += amount;
242
7806
  if (out())
243
  {
244
    Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
245
    Trace("limit") << "          on call "
246
                   << d_statistics->d_spendResourceCalls.get() << std::endl;
247
    if (outOfTime())
248
    {
249
      Trace("limit") << "ResourceManager::spendResource: elapsed time"
250
                     << d_perCallTimer.elapsed() << std::endl;
251
    }
252
253
    for (Listener* l : d_listeners)
254
    {
255
      l->notify();
256
    }
257
  }
258
}
259
260
114510498
void ResourceManager::spendResource(Resource r)
261
{
262
114510498
  uint32_t amount = 0;
263
114510498
  switch (r)
264
  {
265
198166
    case Resource::ArithPivotStep:
266
396332
      amount = d_options[options::arithPivotStep];
267
198166
      ++d_statistics->d_numArithPivotStep;
268
198166
      break;
269
    case Resource::ArithNlLemmaStep:
270
      amount = d_options[options::arithNlLemmaStep];
271
      ++d_statistics->d_numArithNlLemmaStep;
272
      break;
273
91896
    case Resource::BitblastStep:
274
183792
      amount = d_options[options::bitblastStep];
275
91896
      ++d_statistics->d_numBitblastStep;
276
91896
      break;
277
588
    case Resource::BvEagerAssertStep:
278
1176
      amount = d_options[options::bvEagerAssertStep];
279
588
      ++d_statistics->d_numBvEagerAssertStep;
280
588
      break;
281
171639
    case Resource::BvPropagationStep:
282
343278
      amount = d_options[options::bvPropagationStep];
283
171639
      ++d_statistics->d_numBvPropagationStep;
284
171639
      break;
285
10409693
    case Resource::BvSatConflictsStep:
286
20819386
      amount = d_options[options::bvSatConflictStep];
287
10409693
      ++d_statistics->d_numBvSatConflictsStep;
288
10409693
      break;
289
10602716
    case Resource::BvSatPropagateStep:
290
21205432
      amount = d_options[options::bvSatPropagateStep];
291
10602716
      ++d_statistics->d_numBvSatPropagateStep;
292
10602716
      break;
293
1610
    case Resource::BvSatSimplifyStep:
294
3220
      amount = d_options[options::bvSatSimplifyStep];
295
1610
      ++d_statistics->d_numBvSatSimplifyStep;
296
1610
      break;
297
1096585
    case Resource::CnfStep:
298
2193170
      amount = d_options[options::cnfStep];
299
1096585
      ++d_statistics->d_numCnfStep;
300
1096585
      break;
301
2510897
    case Resource::DecisionStep:
302
5021794
      amount = d_options[options::decisionStep];
303
2510897
      ++d_statistics->d_numDecisionStep;
304
2510897
      break;
305
259634
    case Resource::LemmaStep:
306
519268
      amount = d_options[options::lemmaStep];
307
259634
      ++d_statistics->d_numLemmaStep;
308
259634
      break;
309
    case Resource::NewSkolemStep:
310
      amount = d_options[options::newSkolemStep];
311
      ++d_statistics->d_numNewSkolemStep;
312
      break;
313
    case Resource::ParseStep:
314
      amount = d_options[options::parseStep];
315
      ++d_statistics->d_numParseStep;
316
      break;
317
8599577
    case Resource::PreprocessStep:
318
17199154
      amount = d_options[options::preprocessStep];
319
8599577
      ++d_statistics->d_numPreprocessStep;
320
8599577
      break;
321
219589
    case Resource::QuantifierStep:
322
439178
      amount = d_options[options::quantifierStep];
323
219589
      ++d_statistics->d_numQuantifierStep;
324
219589
      break;
325
2312
    case Resource::RestartStep:
326
4624
      amount = d_options[options::restartStep];
327
2312
      ++d_statistics->d_numRestartStep;
328
2312
      break;
329
72457108
    case Resource::RewriteStep:
330
144914216
      amount = d_options[options::rewriteStep];
331
72457108
      ++d_statistics->d_numRewriteStep;
332
72457108
      break;
333
2580075
    case Resource::SatConflictStep:
334
5160150
      amount = d_options[options::satConflictStep];
335
2580075
      ++d_statistics->d_numSatConflictStep;
336
2580075
      break;
337
5308413
    case Resource::TheoryCheckStep:
338
10616826
      amount = d_options[options::theoryCheckStep];
339
5308413
      ++d_statistics->d_numTheoryCheckStep;
340
5308413
      break;
341
    default: Unreachable() << "Invalid resource " << std::endl;
342
  }
343
114510498
  spendResource(amount);
344
114510498
}
345
346
12433
void ResourceManager::beginCall()
347
{
348
12433
  d_perCallTimer.set(d_timeBudgetPerCall);
349
12433
  d_thisCallResourceUsed = 0;
350
12433
  if (!d_on) return;
351
352
11
  if (d_resourceBudgetCumulative > 0)
353
  {
354
    // Compute remaining cumulative resource budget
355
    d_thisCallResourceBudget =
356
        d_resourceBudgetCumulative - d_cumulativeResourceUsed;
357
  }
358
11
  if (d_resourceBudgetPerCall > 0)
359
  {
360
    // Check if per-call resource budget is even smaller
361
    if (d_resourceBudgetPerCall < d_thisCallResourceBudget)
362
    {
363
      d_thisCallResourceBudget = d_resourceBudgetPerCall;
364
    }
365
  }
366
}
367
368
12399
void ResourceManager::endCall()
369
{
370
12399
  d_cumulativeTimeUsed += d_perCallTimer.elapsed();
371
12399
  d_perCallTimer.set(0);
372
12399
  d_thisCallResourceUsed = 0;
373
12399
}
374
375
bool ResourceManager::cumulativeLimitOn() const
376
{
377
  return d_resourceBudgetCumulative > 0;
378
}
379
380
bool ResourceManager::perCallLimitOn() const
381
{
382
  return (d_timeBudgetPerCall > 0) || (d_resourceBudgetPerCall > 0);
383
}
384
385
7817
bool ResourceManager::outOfResources() const
386
{
387
7817
  if (d_resourceBudgetPerCall > 0)
388
  {
389
    // Check if per-call resources are exhausted
390
    if (d_thisCallResourceUsed >= d_resourceBudgetPerCall)
391
    {
392
      return true;
393
    }
394
  }
395
7817
  if (d_resourceBudgetCumulative > 0)
396
  {
397
    // Check if cumulative resources are exhausted
398
    if (d_cumulativeResourceUsed >= d_resourceBudgetCumulative)
399
    {
400
      return true;
401
    }
402
  }
403
7817
  return false;
404
}
405
406
7817
bool ResourceManager::outOfTime() const
407
{
408
7817
  if (d_timeBudgetPerCall == 0) return false;
409
7817
  return d_perCallTimer.expired();
410
}
411
412
void ResourceManager::enable(bool on)
413
{
414
  Trace("limit") << "ResourceManager::enable(" << on << ")\n";
415
  d_on = on;
416
}
417
418
9619
void ResourceManager::registerListener(Listener* listener)
419
{
420
9619
  return d_listeners.push_back(listener);
421
}
422
423
26676
} /* namespace CVC4 */