diff --git a/Lib/Timer.cpp b/Lib/Timer.cpp index 254bfbb25..1a59fcc07 100644 --- a/Lib/Timer.cpp +++ b/Lib/Timer.cpp @@ -12,6 +12,7 @@ * Implements class Timer. */ +#include #include #include #include @@ -43,6 +44,8 @@ const long long MEGA = 1 << 20; // static data for measuring instructions static int PERF_FD = -1; // the file descriptor we later read the info from static long long LAST_INSTRUCTION_COUNT_READ = -1; +// the instruction limit timer_thread enforces, see Timer::setInstructionLimit +static std::atomic INSTRUCTION_BUDGET{0}; namespace Lib { namespace Timer { // The same event, mmap'd so that the main thread can read the counter with rdpmc @@ -134,20 +137,22 @@ static std::recursive_mutex EXIT_LOCK; static std::chrono::time_point START_TIME; +// The thread is detached and can outlive env.options during global cleanup, +// so it must not read env.options: reinitialise passes in the limits instead. // TODO could maybe be more efficient if we special-case the no-instruction-limit case: // then, we could simply sleep until the time limit -[[noreturn]] void timer_thread() +[[noreturn]] void timer_thread(unsigned timeLimit, unsigned simulatedInstrLimit) { - unsigned limit = env.options->timeLimitInDeciseconds(); while(true) { - if(limit && Timer::elapsedDeciseconds() >= limit) { + if(timeLimit && Timer::elapsedDeciseconds() >= timeLimit) { limitReached(TIME_LIMIT); } #if VAMPIRE_PERF_EXISTS - if(env.options->instructionLimit() || env.options->simulatedInstructionLimit()) { + unsigned instrLimit = INSTRUCTION_BUDGET.load(std::memory_order_relaxed); + if(instrLimit || simulatedInstrLimit) { Timer::updateInstructionCount(); - if (env.options->instructionLimit() && LAST_INSTRUCTION_COUNT_READ >= MEGA*(long long)env.options->instructionLimit()) { + if (instrLimit && LAST_INSTRUCTION_COUNT_READ >= MEGA*(long long)instrLimit) { limitReached(INSTRUCTION_LIMIT); } } @@ -162,7 +167,7 @@ static std::chrono::time_point START_TIME; namespace Lib { namespace Timer { -void reinitialise(bool tryInitInstructionLimiting) { +void reinitialise(bool tryInitInstructionLimiting, bool enforceInstructionLimit) { // might (probably have) locked this in the parent process, release it for the child // // I am not sure of the semantics of placement-new for std::recursive_mutex, @@ -227,7 +232,18 @@ void reinitialise(bool tryInitInstructionLimiting) { Shell::TimeTrace::instance().rebaseInstructionCounters(); #endif - std::thread(timer_thread).detach(); + unsigned simulatedInstrLimit = 0; +#if VAMPIRE_PERF_EXISTS + setInstructionLimit(enforceInstructionLimit ? env.options->instructionLimit() : 0); + simulatedInstrLimit = env.options->simulatedInstructionLimit(); +#endif + std::thread(timer_thread, env.options->timeLimitInDeciseconds(), simulatedInstrLimit).detach(); +} + +void setInstructionLimit(unsigned limit) { +#if VAMPIRE_PERF_EXISTS + INSTRUCTION_BUDGET.store(limit, std::memory_order_relaxed); +#endif } void disableLimitEnforcement() { diff --git a/Lib/Timer.hpp b/Lib/Timer.hpp index 515a4d145..1cfeb0a27 100644 --- a/Lib/Timer.hpp +++ b/Lib/Timer.hpp @@ -26,7 +26,8 @@ namespace Timer { // 2. elapsed time (instructions) data should be live // // should be called exactly once per process as it internally spawns a std::thread - void reinitialise(bool tryInitInstructionLimiting=true); + // (with enforceInstructionLimit=false, no instruction limit until setInstructionLimit) + void reinitialise(bool tryInitInstructionLimiting=true, bool enforceInstructionLimit=true); // disables exit on resource out: call when a proof has been found! // permanently disabled per-process @@ -45,6 +46,8 @@ namespace Timer { // instruction limiting stuff below - no-op if !VAMPIRE_PERF_EXISTS // whether instruction limiting succeeded bool instructionLimitingInPlace(); + // change the enforced instruction limit (in millions, 0 for none) + void setInstructionLimit(unsigned limit); // elapsed instructions long elapsedMegaInstructions(); diff --git a/UnitTests/tTimer.cpp b/UnitTests/tTimer.cpp new file mode 100644 index 000000000..f7a8987fd --- /dev/null +++ b/UnitTests/tTimer.cpp @@ -0,0 +1,59 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include +#include +#include + +#include "Lib/Environment.hpp" +#include "Lib/Sys/Multiprocessing.hpp" +#include "Lib/Timer.hpp" +#include "Shell/Options.hpp" +#include "Test/UnitTesting.hpp" + +using namespace Lib; +using namespace std::chrono_literals; + +namespace { +// The timer thread cannot be stopped, so each test starts it in a child process. +void inFreshProcess(void (*test)(), int expectedExitCode = 0) +{ + auto child = Sys::fork(); + if (child == 0) { + test(); + std::exit(0); + } + auto result = Sys::waitForChildTermination(child); + ASS(!result.signalled); + ASS_EQ(result.code, expectedExitCode); +} +} + +// The timer can outlive env.options during global cleanup (#979). +TEST_FUN(does_not_read_options_after_start) +{ + inFreshProcess([] { + env.options->setTimeLimitInDeciseconds(0); + Timer::reinitialise(false); + auto* options = env.options; + env.options = nullptr; + std::this_thread::sleep_for(25ms); + env.options = options; + }); +} + +TEST_FUN(enforces_time_limit) +{ + inFreshProcess([] { + env.options->setTimeLimitInDeciseconds(1); + Timer::reinitialise(false); + std::this_thread::sleep_for(2s); + }, 1); +} diff --git a/cmake/sources.cmake b/cmake/sources.cmake index 6f0726138..610d399e2 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -118,6 +118,7 @@ set(UNIT_TESTS UnitTests/tTermIndex.cpp UnitTests/tTermOutput.cpp UnitTests/tTimeTrace.cpp + UnitTests/tTimer.cpp UnitTests/tTuple.cpp UnitTests/tUnificationWithAbstraction.cpp UnitTests/HOL/tHOL_Printing.cpp diff --git a/vampire.cpp b/vampire.cpp index 6dbd7eba7..418b482f0 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -668,13 +668,12 @@ int main(int argc, char* argv[]) interactiveMetamode(); } else { // can only happen after reading options as it relies on `env.options` - Timer::reinitialise(); // start our timer, so that we also limit parsing - + // start our timer, so that we also limit parsing #if VAMPIRE_PERF_EXISTS - unsigned saveInstrLimit = env.options->instructionLimit(); - if (env.options->parsingDoesNotCount()) { - env.options->setInstructionLimit(0); - } + // (with parsing_does_not_count, the instruction limit starts after parsing, see below) + Timer::reinitialise(true, !env.options->parsingDoesNotCount()); +#else + Timer::reinitialise(); #endif if (opts.inputFile().empty()) { @@ -692,7 +691,13 @@ int main(int argc, char* argv[]) addCommentSignForSZS(std::cout); std::cout << "Instructions burned parsing: " << burnedParsing << " (million)" << endl; - env.options->setInstructionLimit(saveInstrLimit+burnedParsing); + // 0 means no limit, also after parsing + unsigned instrLimit = env.options->instructionLimit(); + if (instrLimit) { + instrLimit += burnedParsing; + env.options->setInstructionLimit(instrLimit); + } + Timer::setInstructionLimit(instrLimit); } #endif