feat: add ability to log inc/dec usage, teach temci about these.

src/include/lean/lean.h

@@ -91,6 +91,13 @@ static inline bool lean_is_big_object_tag(uint8_t tag) {
 
 LEAN_CASSERT(sizeof(size_t) == sizeof(void*));
 
+#ifdef LEAN_RUNTIME_STATS
+extern "C" void increment_lean_num_inc_1();
+extern "C" void increment_lean_num_inc_n();
+extern "C" void increment_lean_num_dec();
+extern "C" void increment_lean_num_is_shared();
+#endif
+
 /*
 Lean object header.
 
@@ -420,6 +427,9 @@ LEAN_EXPORT void lean_inc_ref_cold(lean_object * o);
 LEAN_EXPORT void lean_inc_ref_n_cold(lean_object * o, unsigned n);
 
 static inline void lean_inc_ref(lean_object * o) {
+#ifdef LEAN_RUNTIME_STATS
+    increment_lean_num_inc_1();
+#endif
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_rc++;
     } else if (o->m_rc != 0) {
@@ -428,6 +438,9 @@ static inline void lean_inc_ref(lean_object * o) {
 }
 
 static inline void lean_inc_ref_n(lean_object * o, size_t n) {
+#ifdef LEAN_RUNTIME_STATS
+    increment_lean_num_inc_n();
+#endif
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_rc += n;
     } else if (o->m_rc != 0) {
@@ -438,6 +451,9 @@ static inline void lean_inc_ref_n(lean_object * o, size_t n) {
 LEAN_EXPORT void lean_dec_ref_cold(lean_object * o);
 
 static inline void lean_dec_ref(lean_object * o) {
+#ifdef LEAN_RUNTIME_STATS
+    increment_lean_num_dec();
+#endif
     if (LEAN_LIKELY(o->m_rc > 1)) {
         o->m_rc--;
     } else if (o->m_rc != 0) {
@@ -485,6 +501,9 @@ static inline bool lean_is_exclusive(lean_object * o) {
 }
 
 static inline bool lean_is_shared(lean_object * o) {
+#ifdef LEAN_RUNTIME_STATS
+    increment_lean_num_is_shared();
+#endif
     if (LEAN_LIKELY(lean_is_st(o))) {
         return o->m_rc > 1;
     } else {

src/runtime/alloc.cpp

@@ -50,6 +50,10 @@ static atomic<uint64_t> g_num_segments(0);
 static atomic<uint64_t> g_num_pages(0);
 static atomic<uint64_t> g_num_exports(0);
 static atomic<uint64_t> g_num_recycled_pages(0);
+static std::atomic<uint64_t> g_num_inc_1(0);
+static std::atomic<uint64_t> g_num_inc_n(0);
+static std::atomic<uint64_t> g_num_dec(0);
+static std::atomic<uint64_t> g_num_is_shared(0);
 
 uint64_t get_num_alloc() { return g_num_alloc; }
 uint64_t get_num_small_alloc () { return g_num_small_alloc; }
@@ -60,6 +64,12 @@ uint64_t get_num_pages() { return g_num_pages; }
 uint64_t get_num_exports() { return g_num_exports; }
 uint64_t get_num_recycled_pages() { return g_num_recycled_pages; }
 
+extern "C" {
+  void increment_lean_num_inc_1() { g_num_inc_1++; };
+  void increment_lean_num_inc_n() { g_num_inc_n++; };
+  void increment_lean_num_dec() { g_num_dec++; };
+  void increment_lean_num_is_shared() { g_num_is_shared++; };
+}
 
 struct alloc_stats {
     ~alloc_stats() {
@@ -71,6 +81,11 @@ struct alloc_stats {
         // std::cerr << "num. pages:          " << g_num_pages << "\n";
         // std::cerr << "num. recycled pages: " << g_num_recycled_pages << "\n";
         // std::cerr << "num. exports:        " << g_num_exports << "\n";
+        // std::cerr << "num. inc. 1:         " << g_num_inc_1 << "\n";
+        // std::cerr << "num. inc. n:         " << g_num_inc_n << "\n";
+        // std::cerr << "num. inc. (total):   " << g_num_inc_1 + g_num_inc_n << "\n";
+        // std::cerr << "num. dec.:           " << g_num_dec << "\n";
+        // std::cerr << "num. is_shared.:     " << g_num_is_shared << "\n";
     }
 };
 static alloc_stats g_alloc_stats;

src/runtime/research.cpp

@@ -71,12 +71,14 @@ std::string getEnvVarString(const char *name) {
   }
 }
 
+
 extern "C" {
+const char *g_ResearchAllocatorLogEnvVarName = "RESEARCH_LEAN_RUNTIME_ALLOCATOR_LOG";
+
 // dump allocator info into logfile.
 // TODO: rename into research_runtime_dump_allocator_log_at_end_of_run();
 void research_dump_allocator_log() {
-  const char *envVarName = "RESEARCH_LEAN_RUNTIME_ALLOCATOR_LOG";
-  const char *_envVarName = std::getenv(envVarName);
+  const char *_envVarName = std::getenv(g_ResearchAllocatorLogEnvVarName);
   std::string out_path(_envVarName ? _envVarName : "");
   if (out_path == "") { return; }
 
@@ -91,17 +93,17 @@ void research_dump_allocator_log() {
 
   assert(o);
 
-  (*o << "rss, " << lean::get_peak_rss()) << "\n";
+  (*o << "rss: " << lean::get_peak_rss()) << "\n";
 #ifdef LEAN_RUNTIME_STATS
-  (*o << "num_alloc, " << lean::allocator::get_num_alloc()) << "\n";
-  (*o << "num_small_alloc, " << lean::allocator::get_num_small_alloc()) << "\n";
-  (*o << "num_dealloc, " << lean::allocator::get_num_dealloc()) << "\n";
-  (*o << "num_small_dealloc, " << lean::allocator::get_num_small_dealloc())
+  (*o << "num_alloc: " << lean::allocator::get_num_alloc()) << "\n";
+  (*o << "num_small_alloc: " << lean::allocator::get_num_small_alloc()) << "\n";
+  (*o << "num_dealloc: " << lean::allocator::get_num_dealloc()) << "\n";
+  (*o << "num_small_dealloc: " << lean::allocator::get_num_small_dealloc())
       << "\n";
-  (*o << "num_segments, " << lean::allocator::get_num_segments()) << "\n";
-  (*o << "num_pages, " << lean::allocator::get_num_pages()) << "\n";
-  (*o << "num_exports, " << lean::allocator::get_num_exports()) << "\n";
-  (*o << "num_recycled_pages, " << lean::allocator::get_num_recycled_pages())
+  (*o << "num_segments: " << lean::allocator::get_num_segments()) << "\n";
+  (*o << "num_pages: " << lean::allocator::get_num_pages()) << "\n";
+  (*o << "num_exports: " << lean::allocator::get_num_exports()) << "\n";
+  (*o << "num_recycled_pages: " << lean::allocator::get_num_recycled_pages())
       << "\n";
 #endif
   if (of) {

src/runtime/research.h

@@ -2,12 +2,10 @@
 #include "util/io.h"
 #include "runtime/optional.h"
 
-
-
-// std::string getEnvVarString(const char *name);
-// bool research_isResearchLogVerbose();
-
 extern "C" {
-uint8_t research_isReuseAcrossConstructorsEnabled(lean_object *);
-void research_dump_allocator_log();
+  uint8_t research_isReuseAcrossConstructorsEnabled(lean_object *);
+  void research_dump_allocator_log();
+  extern const char *g_ResearchAllocatorLogEnvVarName;
 }
+
+

tests/bench/.gitignore

@@ -6,3 +6,6 @@
 *.cmi
 *.cmx
 *.o
+temci-*.txt
+*.erroneous.yaml
+run_output.yaml

tests/bench/research-runtime-allocator.exec.yaml

@@ -0,0 +1,30 @@
+- attributes:
+    description: binarytrees
+  build_config:
+    cmd: ./compile.sh binarytrees.lean 2>/dev/null
+  run_config:
+    cmd: |
+      bash -c 'temi-RESEARCH_LEAN_RUNTIME_ALLOCATOR_LOG="temci-binarytrees.txt" ./binarytrees.lean.out 20 2>/dev/null 1>/dev/null; 
+      cat temci-binarytrees.txt'
+    max_runs: 3
+    parse_output: true
+- attributes:
+    description: binarytrees.st
+  run_config:
+    cmd: |
+      bash -c 'RESEARCH_LEAN_RUNTIME_ALLOCATOR_LOG="temci-binarytrees.st.txt" ./binarytrees.st.lean.out 20 2>/dev/null 1>/dev/null;
+      cat temci-binarytrees.st.txt'
+  build_config:
+    cmd: ./compile.sh binarytrees.st.lean
+    max_runs: 3
+    parse_output: true
+- attributes:
+    description: const_fold
+  run_config:
+    cmd: |
+      bash -c 'RESEARCH_LEAN_RUNTIME_ALLOCATOR_LOG="temci-const_fold.txt" ./const_fold.lean.out 16 2>/dev/null 1>/dev/null;
+      cat temci-const_fold.txt'
+    max_runs: 3
+    parse_output: true
+  build_config:
+    cmd: ./compile.sh const_fold.lean