Do not read env.options from the timer thread

Lib/Timer.cpp

@@ -12,6 +12,7 @@
  * Implements class Timer.
  */
 
+#include <atomic>
 #include <iostream>
 #include <mutex>
 #include <thread>
@@ -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<unsigned> 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<std::chrono::steady_clock> 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<std::chrono::steady_clock> 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() {

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();
 

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 <chrono>
+#include <cstdlib>
+#include <thread>
+
+#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);
+}

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

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