diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-16 11:15:19 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-16 11:15:19 +0100 |
commit | db84323caa3009cf418f959313e49f5bea5d35a6 (patch) | |
tree | cf0e4d4d37f97fdb61255853b607fa254f708080 /src/util | |
parent | a71274b992ea5ddfb930b754f1b705f417f7b4e5 (diff) |
Improve accuracy of resource limitation (#4763)
The main goal of the resource limitation mechanism (via `--rlimit`) is to have a deterministic limitation on runtime. The ultimate goal would be that the actual runtime grows linearly with the spent resources.
To achieve this, this PR does the following:
- introduce new resources spent in places that are not yet covered
- find resource weights that best approximate the runtime
It provides a contrib script `learn_resource_weights.py` that uses statistics from a given benchmark run and uses linear regression to find good resource weights. The script also evaluates this estimate and identifies outliers, benchmarks for which this approximation is particularly bad. This probably indicates that on such a benchmark, some part of the code takes a significant amount of time but is not yet represented by a resource.
Eventually, we should use the resulting resource weights as defaults for the options like `--rewrite-step`, `--theory-check-step`, etc.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/resource_manager.cpp | 45 | ||||
-rw-r--r-- | src/util/resource_manager.h | 12 |
2 files changed, 48 insertions, 9 deletions
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index f85e06b12..9afa79ef0 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -66,13 +66,18 @@ struct ResourceManager::Statistics { ReferenceStat<std::uint64_t> d_resourceUnitsUsed; IntStat d_spendResourceCalls; + IntStat d_numArithPivotStep; + IntStat d_numArithNlLemmaStep; IntStat d_numBitblastStep; IntStat d_numBvEagerAssertStep; IntStat d_numBvPropagationStep; IntStat d_numBvSatConflictsStep; + IntStat d_numBvSatPropagateStep; + IntStat d_numBvSatSimplifyStep; IntStat d_numCnfStep; IntStat d_numDecisionStep; IntStat d_numLemmaStep; + IntStat d_numNewSkolemStep; IntStat d_numParseStep; IntStat d_numPreprocessStep; IntStat d_numQuantifierStep; @@ -90,13 +95,18 @@ struct ResourceManager::Statistics ResourceManager::Statistics::Statistics(StatisticsRegistry& stats) : d_resourceUnitsUsed("resource::resourceUnitsUsed"), d_spendResourceCalls("resource::spendResourceCalls", 0), + d_numArithPivotStep("resource::ArithPivotStep", 0), + d_numArithNlLemmaStep("resource::ArithNlLemmaStep", 0), d_numBitblastStep("resource::BitblastStep", 0), d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0), d_numBvPropagationStep("resource::BvPropagationStep", 0), d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0), + d_numBvSatPropagateStep("resource::BvSatPropagateStep", 0), + d_numBvSatSimplifyStep("resource::BvSatSimplifyStep", 0), d_numCnfStep("resource::CnfStep", 0), d_numDecisionStep("resource::DecisionStep", 0), d_numLemmaStep("resource::LemmaStep", 0), + d_numNewSkolemStep("resource::NewSkolemStep", 0), d_numParseStep("resource::ParseStep", 0), d_numPreprocessStep("resource::PreprocessStep", 0), d_numQuantifierStep("resource::QuantifierStep", 0), @@ -108,13 +118,18 @@ ResourceManager::Statistics::Statistics(StatisticsRegistry& stats) { d_statisticsRegistry.registerStat(&d_resourceUnitsUsed); d_statisticsRegistry.registerStat(&d_spendResourceCalls); + d_statisticsRegistry.registerStat(&d_numArithPivotStep); + d_statisticsRegistry.registerStat(&d_numArithNlLemmaStep); d_statisticsRegistry.registerStat(&d_numBitblastStep); d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep); d_statisticsRegistry.registerStat(&d_numBvPropagationStep); d_statisticsRegistry.registerStat(&d_numBvSatConflictsStep); + d_statisticsRegistry.registerStat(&d_numBvSatPropagateStep); + d_statisticsRegistry.registerStat(&d_numBvSatSimplifyStep); d_statisticsRegistry.registerStat(&d_numCnfStep); d_statisticsRegistry.registerStat(&d_numDecisionStep); d_statisticsRegistry.registerStat(&d_numLemmaStep); + d_statisticsRegistry.registerStat(&d_numNewSkolemStep); d_statisticsRegistry.registerStat(&d_numParseStep); d_statisticsRegistry.registerStat(&d_numPreprocessStep); d_statisticsRegistry.registerStat(&d_numQuantifierStep); @@ -128,13 +143,18 @@ ResourceManager::Statistics::~Statistics() { d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed); d_statisticsRegistry.unregisterStat(&d_spendResourceCalls); + d_statisticsRegistry.unregisterStat(&d_numArithPivotStep); + d_statisticsRegistry.unregisterStat(&d_numArithNlLemmaStep); d_statisticsRegistry.unregisterStat(&d_numBitblastStep); d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep); d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep); d_statisticsRegistry.unregisterStat(&d_numBvSatConflictsStep); + d_statisticsRegistry.unregisterStat(&d_numBvSatPropagateStep); + d_statisticsRegistry.unregisterStat(&d_numBvSatSimplifyStep); d_statisticsRegistry.unregisterStat(&d_numCnfStep); d_statisticsRegistry.unregisterStat(&d_numDecisionStep); d_statisticsRegistry.unregisterStat(&d_numLemmaStep); + d_statisticsRegistry.unregisterStat(&d_numNewSkolemStep); d_statisticsRegistry.unregisterStat(&d_numParseStep); d_statisticsRegistry.unregisterStat(&d_numPreprocessStep); d_statisticsRegistry.unregisterStat(&d_numQuantifierStep); @@ -146,8 +166,6 @@ ResourceManager::Statistics::~Statistics() /*---------------------------------------------------------------------------*/ -const uint64_t ResourceManager::s_resourceCount = 1000; - ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) : d_perCallTimer(), d_timeBudgetPerCall(0), @@ -219,7 +237,8 @@ void ResourceManager::spendResource(unsigned amount) if (out()) { Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; - Trace("limit") << " on call " << d_statistics->d_spendResourceCalls.getData() << std::endl; + Trace("limit") << " on call " + << d_statistics->d_spendResourceCalls.getData() << std::endl; if (outOfTime()) { Trace("limit") << "ResourceManager::spendResource: elapsed time" @@ -238,6 +257,14 @@ void ResourceManager::spendResource(Resource r) uint32_t amount = 0; switch (r) { + case Resource::ArithPivotStep: + amount = d_options[options::arithPivotStep]; + ++d_statistics->d_numArithPivotStep; + break; + case Resource::ArithNlLemmaStep: + amount = d_options[options::arithNlLemmaStep]; + ++d_statistics->d_numArithNlLemmaStep; + break; case Resource::BitblastStep: amount = d_options[options::bitblastStep]; ++d_statistics->d_numBitblastStep; @@ -254,6 +281,14 @@ void ResourceManager::spendResource(Resource r) amount = d_options[options::bvSatConflictStep]; ++d_statistics->d_numBvSatConflictsStep; break; + case Resource::BvSatPropagateStep: + amount = d_options[options::bvSatPropagateStep]; + ++d_statistics->d_numBvSatPropagateStep; + break; + case Resource::BvSatSimplifyStep: + amount = d_options[options::bvSatSimplifyStep]; + ++d_statistics->d_numBvSatSimplifyStep; + break; case Resource::CnfStep: amount = d_options[options::cnfStep]; ++d_statistics->d_numCnfStep; @@ -266,6 +301,10 @@ void ResourceManager::spendResource(Resource r) amount = d_options[options::lemmaStep]; ++d_statistics->d_numLemmaStep; break; + case Resource::NewSkolemStep: + amount = d_options[options::newSkolemStep]; + ++d_statistics->d_numNewSkolemStep; + break; case Resource::ParseStep: amount = d_options[options::parseStep]; ++d_statistics->d_numParseStep; diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index e67598afc..f6cff2e7f 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -10,7 +10,7 @@ ** directory for licensing information.\endverbatim ** ** \brief Provides mechanisms to limit resources. - ** + ** ** This file provides the ResourceManager class. It can be used to impose ** (cumulative and per-call) resource limits on the solver, as well as per-call ** time limits. @@ -81,13 +81,18 @@ class CVC4_PUBLIC ResourceManager /** Types of resources. */ enum class Resource { + ArithPivotStep, + ArithNlLemmaStep, BitblastStep, BvEagerAssertStep, BvPropagationStep, BvSatConflictsStep, + BvSatPropagateStep, + BvSatSimplifyStep, CnfStep, DecisionStep, LemmaStep, + NewSkolemStep, ParseStep, PreprocessStep, QuantifierStep, @@ -159,8 +164,6 @@ class CVC4_PUBLIC ResourceManager */ void endCall(); - static uint64_t getFrequencyCount() { return s_resourceCount; } - /** * Registers a listener that is notified on a resource out or (per-call) * timeout. @@ -195,9 +198,6 @@ class CVC4_PUBLIC ResourceManager /** A flag indicating whether resource limitation is active. */ bool d_on; - /** Counter indicating how often to check resource manager in loops */ - static const uint64_t s_resourceCount; - /** Receives a notification on reaching a limit. */ std::vector<Listener*> d_listeners; |