Merge pull request #594 from vprover/michael-memory-rlimit

use rlimit to enforce memory limits rather than global allocators

CMakeLists.txt

@@ -19,8 +19,6 @@ if(CMAKE_CXX_COMPILER_ID STREQUAL GNU OR CMAKE_CXX_COMPILER_ID MATCHES Clang$)
   add_compile_options(-fno-threadsafe-statics)
   # ...or RTTI
   add_compile_options(-fno-rtti)
-  # enable standards-compliant standard library with sized operator delete
-  add_compile_options(-fsized-deallocation)
 endif()
 
 # compile command database

Lib/Allocator.cpp

@@ -16,86 +16,37 @@
  * @since 24/07/2023, mostly replaced by a small-object allocator
  */
 
-#include <cstdlib>
-#include <limits>
+#include <cstdio>
 
 #include "Allocator.hpp"
 
-#include <cstdlib>
-#include <limits>
-
-#ifdef __APPLE__
-#include <AvailabilityMacros.h>
-#endif
-
 #ifndef INDIVIDUAL_ALLOCATIONS
 Lib::SmallObjectAllocator Lib::GLOBAL_SMALL_OBJECT_ALLOCATOR;
 #endif
 
-static size_t ALLOCATED = 0;
-// set by main very soon after launch
-static size_t LIMIT = std::numeric_limits<size_t>::max();
-
-size_t Lib::getUsedMemory() { return ALLOCATED; }
-size_t Lib::getMemoryLimit() { return LIMIT; }
-void Lib::setMemoryLimit(size_t limit) { LIMIT = limit; }
-
-// override global allocators to keep track of allocated memory, doing very little else
-// TODO does not support get_new_handler/set_new_handler as we don't use it, but we could
-void *operator new(size_t size, std::align_val_t align_val) {
-  size_t align = static_cast<size_t>(align_val);
-  // standard says `size` must be an integer multiple of `align`
-  ASS_EQ(size % align, 0)
-
-  if(ALLOCATED + size > LIMIT)
-    throw std::bad_alloc();
-  ALLOCATED += size;
-  {
-// aligned_alloc is not supported prior to macOS 10.13
-#if !defined(__APPLE__) || (defined(__APPLE__) && MAC_OS_X_VERSION_MIN_REQUIRED >= 101300)
-    if(void *ptr = std::aligned_alloc(align, size))
-      return ptr;
+#if __has_include(<sys/resource.h>)
+#include <sys/resource.h>
+#define HAVE_RLIMIT
 #endif
 
-    // we might be here because `aligned_alloc` is finicky (Apple, looking at you)
-    // so try again with `malloc` and hope for good alignment
-    if(void *ptr = std::malloc(size))
-      return ptr;
+const size_t MIN_MEMORY = 20971520;
 
-  }
-  // no, we're actually out of memory
-  throw std::bad_alloc();
-}
+void Lib::setMemoryLimit(size_t limit) {
+  // if limit is less than floor, ignore it
+  if(limit < MIN_MEMORY)
+    return;
 
-// a version of the above operator-new without alignment information
-void *operator new(size_t size) {
-  if(ALLOCATED + size > LIMIT)
-    throw std::bad_alloc();
-  ALLOCATED += size;
-  {
-    if(void *ptr = std::malloc(size))
-      return ptr;
+#ifdef HAVE_RLIMIT
+  struct rlimit rlimit;
+  rlimit.rlim_cur = rlimit.rlim_max = limit;
+  if (setrlimit(RLIMIT_DATA, &rlimit) != 0) {
+#if defined(__APPLE__) && defined(__MACH__)
+    if (errno != EINVAL) // silence buggy failure on OSX
+#endif
+      std::perror("memory limiting failed");
   }
-  throw std::bad_alloc();
-}
-
-// normal delete, just decrements `ALLOCATED` and calls free()
-void operator delete(void *ptr, size_t size) noexcept {
-  ASS_GE(ALLOCATED, size)
-  ALLOCATED -= size;
-  std::free(ptr);
-}
 
-// aligned-and-sized delete
-// forwards to the sized delete as we don't use the alignment information
-void operator delete(void *ptr, size_t size, std::align_val_t align) noexcept {
-  operator delete(ptr, size);
-}
-
-// unsized (and unaligned) delete
-// called if we don't know the size of the deallocated object somehow,
-// 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 {
-  std::free(ptr);
+#else
+  // TODO should we warn here?
+#endif
 }

Lib/Allocator.hpp

@@ -24,7 +24,6 @@
 #include <new>
 
 #include "Debug/Assertion.hpp"
-#include "Portability.hpp"
 
 /*
  * uncomment the following to use Valgrind more profitably
@@ -34,25 +33,18 @@
 // #define INDIVIDUAL_ALLOCATIONS
 
 namespace Lib {
-
-// get the amount of memory used by global operator new so far
-size_t getUsedMemory();
-
-// get the memory limit for global operator new
-size_t getMemoryLimit();
-// set the memory limit for global operator new
+// attempt to set a memory limit for this process by system call
 void setMemoryLimit(size_t bytes);
-
 }
 
 #ifdef INDIVIDUAL_ALLOCATIONS
 namespace Lib {
 inline void *alloc(size_t size, size_t align = alignof(std::max_align_t)) {
-  return ::operator new(size, (std::max_align_t)align);
+  return ::operator new(size, (std::align_val_t)align);
 }
 
 inline void free(void *pointer, size_t size, size_t align = alignof(std::max_align_t)) {
-  ::operator delete(pointer);
+  ::operator delete(pointer, (std::align_val_t)align);
 }
 } // namespace Lib
 #define USE_GLOBAL_SMALL_OBJECT_ALLOCATOR(C)
@@ -215,7 +207,7 @@ class SmallObjectAllocator {
     if(size <= 8 * sizeof(void *))
       return FSA8.free(pointer);
 
-    ::operator delete(pointer, size, (std::align_val_t)align);
+    ::operator delete(pointer, (std::align_val_t)align);
   }
 
 private:

Saturation/ProvingHelper.cpp

@@ -57,9 +57,6 @@ using namespace Shell;
   catch(const std::bad_alloc &) {
     env.statistics->terminationReason=Statistics::MEMORY_LIMIT;
     env.statistics->refutation=0;
-    size_t limit=Lib::getMemoryLimit();
-    //add extra 1 MB to allow proper termination
-    Lib::setMemoryLimit(limit+1000000);
   }
   catch(TimeLimitExceededException&) {
     env.statistics->terminationReason=Statistics::TIME_LIMIT;
@@ -107,9 +104,6 @@ void ProvingHelper::runVampire(Problem& prb, const Options& opt)
   catch(const std::bad_alloc &) {
     env.statistics->terminationReason=Statistics::MEMORY_LIMIT;
     env.statistics->refutation=0;
-    size_t limit=Lib::getMemoryLimit();
-    //add extra 1 MB to allow proper termination
-    Lib::setMemoryLimit(limit+1000000);
   }
   catch(TimeLimitExceededException&) {
     env.statistics->terminationReason=Statistics::TIME_LIMIT;

Shell/Options.cpp

@@ -93,7 +93,7 @@ void Options::init()
                                        131072   // 128 GB (current max on the StarExecs)
 #endif
                                        );
-    _memoryLimit.description="Memory limit in MB";
+    _memoryLimit.description="Attempt to limit memory use (in MB). Limits less than 20MB are ignored to allow Vampire to start. Known not to work on MacOS for mysterious reasons: https://forums.developer.apple.com/forums/thread/702803";
     _lookup.insert(&_memoryLimit);
 
 #if VAMPIRE_PERF_EXISTS

Shell/Statistics.cpp

@@ -18,7 +18,6 @@
 
 #include "Debug/RuntimeStatistics.hpp"
 
-#include "Lib/Allocator.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Timer.hpp"
 #include "SAT/Z3Interfacing.hpp"
@@ -469,21 +468,19 @@ void Statistics::print(ostream& out)
 
   }
 
-  COND_OUT("Memory used [KB]", Lib::getUsedMemory()/1024);
-
   addCommentSignForSZS(out);
   out << "Time elapsed: ";
   Timer::printMSString(out,Timer::elapsedMilliseconds());
   out << endl;
-  
+
   Timer::updateInstructionCount();
   unsigned instr = Timer::elapsedMegaInstructions();
   if (instr) {
     addCommentSignForSZS(out);
     out << "Instructions burned: " << instr << " (million)";
     out << endl;
   }
-  
+
   addCommentSignForSZS(out);
   out << "------------------------------\n";
 

Shell/UIHelper.cpp

@@ -106,7 +106,6 @@ void reportSpiderStatus(char status)
     << (problemName.length() == 0 ? "unknown" : problemName) << " "
     << Timer::elapsedDeciseconds() << " "
     << Timer::elapsedMegaInstructions() << " "
-    << Lib::getUsedMemory()/1048576 << " "
     << (Lib::env.options ? Lib::env.options->testId() : "unknown") << " "
     << commitNumber << ':' << z3Version << endl;
 #endif