replace signal-based Timer with a ticking thread

CASC/PortfolioMode.cpp

@@ -109,11 +109,11 @@ bool PortfolioMode::perform(Problem* problem)
   if (outputAllowed()) {
     if (resValue) {
       addCommentSignForSZS(cout);
-      cout<<"Success in time "<<Timer::msToSecondsString(env.timer->elapsedMilliseconds())<<endl;
+      cout<<"Success in time "<<Timer::msToSecondsString(Timer::elapsedMilliseconds())<<endl;
     }
     else {
       addCommentSignForSZS(cout);
-      cout<<"Proof not found in time "<<Timer::msToSecondsString(env.timer->elapsedMilliseconds())<<endl;
+      cout<<"Proof not found in time "<<Timer::msToSecondsString(Timer::elapsedMilliseconds())<<endl;
       if (env.remainingTime()/100>0) {
         addCommentSignForSZS(cout);
         cout<<"SZS status GaveUp for "<<env.options->problemName()<<endl;
@@ -439,7 +439,7 @@ bool PortfolioMode::runSchedule(Schedule schedule) {
   Set<pid_t> processes;
   bool success = false;
   int remainingTime;
-  while(Timer::syncClock(), remainingTime = env.remainingTime() / 100, remainingTime > 0)
+  while(remainingTime = env.remainingTime() / 100, remainingTime > 0)
   {
     // running under capacity, wake up more tasks
     while(processes.size() < _numWorkers)
@@ -632,12 +632,7 @@ void PortfolioMode::runSlice(Options& strategyOpt)
 {
   System::registerForSIGHUPOnParentDeath();
   UIHelper::portfolioParent=false;
-
-  env.timer->reset();
-  env.timer->start();
-
-  Timer::resetInstructionMeasuring();
-  Timer::setLimitEnforcement(true);
+  Timer::reinitialise();
 
   Options opt = strategyOpt;
   //we have already performed the normalization (or don't care about it)

FMB/FiniteModelBuilder.cpp

@@ -1601,9 +1601,6 @@ MainLoopResult FiniteModelBuilder::runImpl()
       }
       cout << "]" << endl;
     }
-    Timer::syncClock();
-    if(env.timeLimitReached()){ return MainLoopResult(Statistics::TIME_LIMIT); }
-
     {
     TIME_TRACE("fmb constraint creation");
 

Forwards.hpp

@@ -20,7 +20,6 @@
 namespace Lib
 {
 struct EmptyStruct {};
-typedef void (*VoidFunc)();
 
 template<typename T> class VirtualIterator;
 
@@ -37,7 +36,6 @@ template<typename T> class SharedSet;
 
 typedef List<int> IntList;
 typedef Stack<vstring> StringStack;
-typedef List<VoidFunc> VoidFuncList;
 
 class DefaultHash;
 class DefaultHash2;
@@ -47,8 +45,6 @@ template <typename Key, typename Val, class Hash1=DefaultHash, class Hash2=Defau
 template <typename Val, class Hash1=DefaultHash, class Hash2=DefaultHash2> class DHSet;
 template <typename Val, class Hash1=DefaultHash, class Hash2=DefaultHash2> class DHMultiset;
 template <typename Val, class Hash=DefaultHash> class Set;
-
-class Timer;
 };
 
 namespace Kernel

Kernel/MLMatcher.cpp

@@ -398,7 +398,6 @@ class MLMatcher::Impl final
     // For backtracking support
     DArray<unsigned> s_matchRecord;
     unsigned s_currBLit;
-    int s_counter;
     bool s_multiset;
 };
 
@@ -557,7 +556,6 @@ void MLMatcher::Impl::init(Literal** baseLits, unsigned baseLen, Clause* instanc
 
   s_matchingData.nextAlts[0] = 0;
   s_currBLit = 0;
-  s_counter = 0;
   s_multiset = multiset;
 }
 
@@ -621,15 +619,6 @@ bool MLMatcher::Impl::nextMatch()
       if(s_currBLit==0) { return false; }
       s_currBLit--;
     }
-
-    s_counter++;
-    if(s_counter==50000) {
-      s_counter=0;
-      if(env.timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
-
   } // while (true)
 
   ASSERTION_VIOLATION; // unreachable

Kernel/MLMatcherSD.cpp

@@ -741,8 +741,6 @@ class MLMatcherSD::Impl final
     DArray<pair<int,int> > s_intersectionData;
 
     MatchingData s_matchingData;
-
-    int s_counter;
 };
 
 
@@ -889,8 +887,6 @@ void MLMatcherSD::Impl::init(Literal** baseLits, unsigned baseLen, Clause* insta
     std::cerr << "\tinstance: " << instance->toString() << std::endl;
 #endif
   initMatchingData(baseLits, baseLen, instance, alts);
-
-  s_counter = 0;
 }
 
 
@@ -1060,16 +1056,6 @@ bool MLMatcherSD::Impl::nextMatch()
         return false;
       }
     }
-
-    // Ensure vampire exits timely in pathological cases instead of appearing to be stuck
-    s_counter++;
-    if(s_counter==50000) {
-      // std::cerr << "counter reached 50k" << std::endl;
-      s_counter=0;
-      if(env.timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
   } // while (true)
 
   // We found a complete match

Kernel/MLVariant.cpp

@@ -410,8 +410,6 @@ bool MLVariant::isVariant(Literal* const * cl1Lits, Clause* cl2, LiteralList** a
   md->nextAlts[0]=0;
   unsigned currBLit=0;
 
-  int counter=0;
-
   while(true) {
     MatchingData::InitResult ires=md->ensureInit(currBLit);
     if(ires!=MatchingData::OK) {
@@ -448,14 +446,6 @@ bool MLVariant::isVariant(Literal* const * cl1Lits, Clause* cl2, LiteralList** a
       if(currBLit==0) { return false; }
       currBLit--;
     }
-
-    counter++;
-    if(counter==50000) {
-      counter=0;
-      if(env.timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
   }
   return true;
 }

Lib/Allocator.cpp

@@ -16,8 +16,10 @@
  * @since 24/07/2023, mostly replaced by a small-object allocator
  */
 
+#include <cstdlib>
+#include <limits>
+
 #include "Allocator.hpp"
-#include "Lib/Timer.hpp"
 
 #ifndef INDIVIDUAL_ALLOCATIONS
 Lib::SmallObjectAllocator Lib::GLOBAL_SMALL_OBJECT_ALLOCATOR;
@@ -42,7 +44,6 @@ void *operator new(size_t size, std::align_val_t align_val) {
     throw std::bad_alloc();
   ALLOCATED += size;
   {
-    Lib::TimeoutProtector tp;
     if(void *ptr = std::aligned_alloc(align, size))
       return ptr;
 
@@ -62,7 +63,6 @@ void *operator new(size_t size) {
     throw std::bad_alloc();
   ALLOCATED += size;
   {
-    Lib::TimeoutProtector tp;
     if(void *ptr = std::malloc(size))
       return ptr;
   }
@@ -73,7 +73,6 @@ void *operator new(size_t size) {
 void operator delete(void *ptr, size_t size) noexcept {
   ASS_GE(ALLOCATED, size)
   ALLOCATED -= size;
-  Lib::TimeoutProtector tp;
   std::free(ptr);
 }
 
@@ -88,6 +87,5 @@ void operator delete(void *ptr, size_t size, std::align_val_t align) noexcept {
 // occurs very rarely and usually from deep in the bowels of the standard library
 // TODO does cause us to slightly over-report allocated memory
 void operator delete(void *ptr) noexcept {
-  Lib::TimeoutProtector tp;
   std::free(ptr);
 }

Lib/Environment.cpp

@@ -48,9 +48,6 @@ Environment::Environment()
 {
   options = new Options;
 
-  // statistics calls the timer
-  timer = Timer::instance();
-
   statistics = new Statistics;
   signature = new Signature;
   sharing = new TermSharing;
@@ -71,31 +68,13 @@ Environment::Environment()
 
 Environment::~Environment()
 {
-  Timer::setLimitEnforcement(false);
-
   delete sharing;
   delete signature;
   delete statistics;
   if (predicateSineLevels) delete predicateSineLevels;
   delete options;
 }
 
-/**
- * If the global time limit reached set Statistics::terminationReason
- * to TIME_LIMIT and return true, otherwise return false.
- * @since 25/03/2008 Torrevieja
- */
-bool Environment::timeLimitReached() const
-{
-  if (options->timeLimitInDeciseconds() &&
-      timer->elapsedDeciseconds() > options->timeLimitInDeciseconds()) {
-    statistics->terminationReason = Shell::Statistics::TIME_LIMIT;
-    Timer::setLimitEnforcement(false);
-    return true;
-  }
-  return false;
-} // Environment::timeLimitReached
-
 /**
  * Return remaining time in miliseconds.
  */
@@ -105,7 +84,7 @@ int Environment::remainingTime() const
   if(options->timeLimitInDeciseconds() == 0){
     return 3600000;
   }
-  return options->timeLimitInDeciseconds()*100 - timer->elapsedMilliseconds();
+  return options->timeLimitInDeciseconds()*100 - Timer::elapsedMilliseconds();
 }
 
 // global environment object, constructed before main() and used everywhere

Lib/Environment.hpp

@@ -46,29 +46,13 @@ class Environment
   Indexing::TermSharing* sharing;
   /** Currently used statistics */
   Shell::Statistics* statistics;
-  /** Currently used timer, this is used by all timers as a global clock */
-  Timer* timer;
 
   unsigned char maxSineLevel;
 
   DHMap<unsigned, unsigned>* predicateSineLevels;
 
   DHMap<const Kernel::Unit*,vstring>* proofExtra; // maps Unit* pointers to the associated proof extra string, if available
 
-  bool timeLimitReached() const;
-
-  template<int Period>
-  void checkTimeSometime() const
-  {
-    static int counter=0;
-    counter++;
-    if(counter==Period) {
-      counter=0;
-      if(timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
-  }
   /** Time remaining until the end of the time-limit in miliseconds */
   int remainingTime() const;
   /** set to true when coloring is used for symbol elimination or interpolation */

Lib/Portability.hpp

@@ -19,4 +19,12 @@ static_assert(
     "Vampire assumes that there are 8 bits in a `char`"
 );
 
+#define VAMPIRE_PERF_EXISTS 0
+#ifdef __linux__
+#if __has_include(<linux/perf_event.h>)
+#undef VAMPIRE_PERF_EXISTS
+#define VAMPIRE_PERF_EXISTS 1
+#endif
+#endif
+
 #endif /*__Portability__*/

Lib/Sys/Multiprocessing.cpp

@@ -13,20 +13,15 @@
  */
 
 #include <cerrno>
-
-#include "Lib/Portability.hpp"
-
 #include <csignal>
 #include <unistd.h>
 #include <sys/types.h>
 #include <sys/wait.h>
 
-#include "Lib/Environment.hpp"
-#include "Lib/List.hpp"
-#include "Lib/Timer.hpp"
+#include "Debug/TimeProfiling.hpp"
+#include "Lib/Exception.hpp"
 
 #include "Multiprocessing.hpp"
-#include "Debug/TimeProfiling.hpp"
 
 namespace Lib
 {
@@ -39,56 +34,13 @@ Multiprocessing* Multiprocessing::instance()
   return &inst;
 }
 
-Multiprocessing::Multiprocessing()
-: _preFork(0), _postForkParent(0), _postForkChild(0)
-{
-
-}
-
-Multiprocessing::~Multiprocessing()
-{
-  VoidFuncList::destroy(_preFork);
-  VoidFuncList::destroy(_postForkParent);
-  VoidFuncList::destroy(_postForkChild);
-}
-
-void Multiprocessing::registerForkHandlers(VoidFunc before, VoidFunc afterParent, VoidFunc afterChild)
-{
-  if(before) {
-    VoidFuncList::push(before, _preFork);
-  }
-  if(afterParent) {
-    VoidFuncList::push(afterParent, _postForkParent);
-  }
-  if(afterChild) {
-    VoidFuncList::push(afterChild, _postForkChild);
-  }
-}
-
-void Multiprocessing::executeFuncList(VoidFuncList* lst)
-{
-  VoidFuncList::Iterator fit(lst);
-  while(fit.hasNext()) {
-    VoidFunc func=fit.next();
-    func();
-  }
-}
-
-
 pid_t Multiprocessing::fork()
 {
-  executeFuncList(_preFork);
   errno=0;
   pid_t res=::fork();
   if(res==-1) {
     SYSTEM_FAIL("Call to fork() function failed.", errno);
   }
-  if(res==0) {
-    executeFuncList(_postForkChild);
-  }
-  else {
-    executeFuncList(_postForkParent);
-  }
   return res;
 }