From f3bd1e81f686eaae3cf9431a06c08ff6650d53b3 Mon Sep 17 00:00:00 2001 From: Pietro Pellegrino <72952819+shalashaska117@users.noreply.github.com> Date: Fri, 23 Oct 2026 22:15:49 +0200 Subject: [PATCH] do not read env.options from the timer thread The detached timer thread read the instruction limits from env.options on every tick, so it could read freed Options during global cleanup. reinitialise() now passes the time and simulated instruction limits to the thread. The instruction limit lives in an atomic in Timer, because main sets it after parsing under --parsing_does_not_count; with that flag the timer starts without one. An unlimited budget now stays unlimited after parsing; before, it became the parsing cost. Closes #979. --- Lib/Timer.cpp | 30 ++++++++++++++++------ Lib/Timer.hpp | 5 +++- UnitTests/tTimer.cpp | 59 ++++++++++++++++++++++++++++++++++++++++++++ cmake/sources.cmake | 1 + vampire.cpp | 19 ++++++++------ 5 files changed, 99 insertions(+), 15 deletions(-) create mode 100644 UnitTests/tTimer.cpp 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