feat(make): add THREAD_SAFE build option

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/CMakeLists.txt

@@ -7,6 +7,7 @@ set(CMAKE_COLOR_MAKEFILE ON)
 enable_testing()
 
 option(TRACK_MEMORY_USAGE "TRACK_MEMORY_USAGE" ON)
+option(THREAD_SAFE "THREAD_SAFE" ON)
 
 # Added for CTest
 INCLUDE(CTest)
@@ -23,6 +24,11 @@ if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_DEFAULT_PP_UNICODE=false")
 endif()
 
+if("${THREAD_SAFE}" MATCHES "OFF")
+  message(STATUS "Disabled thread-safety, it will not be safe to run multiple threads in parallel")
+  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_THREAD_UNSAFE")
+endif()
+
 # Set Module Path
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules/")
 

src/kernel/environment.cpp

@@ -25,7 +25,11 @@ struct environment::imp {
     std::vector<constraint>              m_constraints;
     std::vector<level>                   m_uvars;
     // Children environment management
+#ifdef LEAN_THREAD_UNSAFE
+    unsigned                             m_num_children;
+#else
     std::atomic<unsigned>                m_num_children;
+#endif
     std::shared_ptr<imp>                 m_parent;
     // Object management
     std::vector<object>                  m_objects;

src/kernel/expr.h

@@ -64,7 +64,11 @@ typedef list<local_entry> local_context;
 class expr_cell {
 protected:
     unsigned short     m_kind;
+#ifdef LEAN_THREAD_UNSAFE
+    unsigned short     m_flags;
+#else
     std::atomic_ushort m_flags;
+#endif
     unsigned m_hash;
     MK_LEAN_RC(); // Declare m_rc counter
     void dealloc();

src/util/memory.cpp

@@ -96,7 +96,11 @@ inline void   free_core(void * ptr)               { ::free(static_cast<size_t*>(
 
 namespace lean {
 class alloc_info {
+#ifdef LEAN_THREAD_UNSAFE
+    size_t              m_size;
+#else
     std::atomic<size_t> m_size;
+#endif
 public:
     alloc_info():m_size(0) {}
     ~alloc_info() {}

src/util/name.cpp

@@ -155,10 +155,14 @@ name const & name::anonymous() {
     return g_anonymous;
 }
 
+#ifdef LEAN_THREAD_UNSAFE
+static unsigned g_next_id(0);
+#else
 static std::atomic<unsigned> g_next_id(0);
+#endif
 
 name name::mk_internal_unique_name() {
-    unsigned id = std::atomic_fetch_add(&g_next_id, 1u);
+    unsigned id = g_next_id++;
     return name(id);
 }
 

src/util/rc.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 
 // Goodies for reference counting
-#ifdef LEAN_THREAD_UNSAFE_REF_COUNT
+#ifdef LEAN_THREAD_UNSAFE
 #define MK_LEAN_RC()                                                    \
 private:                                                                \
 unsigned m_rc;                                                          \