From 3f57984840615685bc8049fafdd7e2ddc4fbb9a1 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Wed, 8 Jan 2025 14:27:27 +0000 Subject: [PATCH] Timer.cpp sets terminationReason only in limitReached, after acquiring the lock --- Lib/Timer.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Lib/Timer.cpp b/Lib/Timer.cpp index c25b6678d..ce8385527 100644 --- a/Lib/Timer.cpp +++ b/Lib/Timer.cpp @@ -69,12 +69,15 @@ static std::recursive_mutex EXIT_LOCK; // for debugging crashes of limitReached: it is good to know what was called by vampire proper just before the interrupt // Debug::Tracer::printStack(cout); - const char* REACHED[2] = {"Time limit reached!\n","Instruction limit reached!\n"}; + const char* REACHED[2] = {"Time limit reached! \n","Instruction limit reached! \n"}; // deliberate spaces before \n, so that it's a different string than in UIHelper::outputResult const char* STATUS[2] = {"% SZS status Timeout for ","% SZS status InstrOut for "}; + Shell::Statistics::TerminationReason REASON[2] = {Shell::Statistics::TIME_LIMIT,Shell::Statistics::INSTRUCTION_LIMIT}; // if we get this lock we can assume that the parent won't also try to exit EXIT_LOCK.lock(); + env.statistics->terminationReason = REASON[whichLimit]; + // NB unsynchronised output: // probably OK as we don't output anything in other parts of Vampire during search reportSpiderStatus('t'); @@ -115,8 +118,6 @@ static std::chrono::time_point START_TIME; unsigned limit = env.options->timeLimitInDeciseconds(); while(true) { if(limit && Timer::elapsedDeciseconds() >= limit) { - // in principle could have a race on terminationReason, seems unlikely/harmless in practice - env.statistics->terminationReason = Shell::Statistics::TIME_LIMIT; limitReached(TIME_LIMIT); } @@ -124,8 +125,6 @@ static std::chrono::time_point START_TIME; if(env.options->instructionLimit() || env.options->simulatedInstructionLimit()) { Timer::updateInstructionCount(); if (env.options->instructionLimit() && LAST_INSTRUCTION_COUNT_READ >= MEGA*(long long)env.options->instructionLimit()) { - // in principle could have a race on terminationReason, seems unlikely/harmless in practice - env.statistics->terminationReason = Shell::Statistics::INSTRUCTION_LIMIT; limitReached(INSTRUCTION_LIMIT); } }