turn locks into no-ops when compiled with -DSINGLE_THREAD

src/api/api_context.cpp

@@ -119,18 +119,18 @@ namespace api {
 
     context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
         m_ctx(ctx) {
-        std::lock_guard<std::mutex> lock(ctx.m_mux);
+        lock_guard lock(ctx.m_mux);
         SASSERT(m_ctx.m_interruptable == 0);
         m_ctx.m_interruptable = &i;        
     }
 
     context::set_interruptable::~set_interruptable() {
-        std::lock_guard<std::mutex> lock(m_ctx.m_mux);
+        lock_guard lock(m_ctx.m_mux);
         m_ctx.m_interruptable = nullptr;        
     }
 
     void context::interrupt() {
-        std::lock_guard<std::mutex> lock(m_mux);
+        lock_guard lock(m_mux);
         if (m_interruptable)
             (*m_interruptable)(API_INTERRUPT_EH_CALLER);
         m_limit.cancel();

src/api/api_context.h

@@ -42,7 +42,7 @@ Revision History:
 #include "ast/rewriter/seq_rewriter.h"
 #include "smt/smt_solver.h"
 #include "solver/solver.h"
-#include <mutex>
+#include "util/mutex.h"
 
 namespace smtlib {
     class parser;
@@ -80,7 +80,7 @@ namespace api {
         scoped_ptr<ast_manager>    m_manager;
         scoped_ptr<cmd_context>    m_cmd;
         add_plugins                m_plugins;
-        std::mutex                 m_mux;
+        mutex                      m_mux;
 
         arith_util                 m_arith_util;
         bv_util                    m_bv_util;

src/sat/sat_parallel.cpp

@@ -104,7 +104,7 @@ namespace sat {
         m_solvers.resize(num_extra_solvers);
         symbol saved_phase = s.m_params.get_sym("phase", symbol("caching"));
         for (unsigned i = 0; i < num_extra_solvers; ++i) {        
-            m_limits.push_back(alloc(reslimit));
+            m_limits.push_back(reslimit());
         }
         
         for (unsigned i = 0; i < num_extra_solvers; ++i) {
@@ -112,7 +112,7 @@ namespace sat {
             if (i == 1 + num_threads/2) {
                 s.m_params.set_sym("phase", symbol("random"));
             }                        
-            m_solvers[i] = alloc(sat::solver, s.m_params, *m_limits[i]);
+            m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]);
             m_solvers[i]->copy(s, true);
             m_solvers[i]->set_par(this, i);
             push_child(m_solvers[i]->rlimit());            

src/sat/sat_parallel.h

@@ -24,6 +24,7 @@ Revision History:
 #include "util/map.h"
 #include "util/rlimit.h"
 #include "util/scoped_ptr_vector.h"
+#include <mutex>
 
 namespace sat {
 
@@ -70,7 +71,7 @@ namespace sat {
         bool               m_consumer_ready;
 
         scoped_limits      m_scoped_rlimit;
-        scoped_ptr_vector<reslimit> m_limits;
+        vector<reslimit>   m_limits;
         ptr_vector<solver> m_solvers;
         
     public:
@@ -88,7 +89,7 @@ namespace sat {
 
         solver& get_solver(unsigned i) { return *m_solvers[i]; }
 
-        void cancel_solver(unsigned i) { m_limits[i]->cancel(); }
+        void cancel_solver(unsigned i) { m_limits[i].cancel(); }
 
         // exchange unit literals
         void exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out);

src/smt/asserted_formulas.cpp

@@ -435,12 +435,9 @@ void asserted_formulas::commit(unsigned new_qhead) {
     TRACE("asserted_formulas", tout << "commit " << new_qhead << "\n";);
     m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead);
     m_expr2depth.reset();
-    bool new_sub = false;
     for (unsigned i = m_qhead; i < new_qhead; ++i) {
         justified_expr const& j = m_formulas[i];
-        if (update_substitution(j.get_fml(), j.get_proof())) {
+        update_substitution(j.get_fml(), j.get_proof());
-            new_sub = true;
-        }
     }
     m_qhead = new_qhead;
 }

src/smt/theory_array_bapa.cpp

@@ -321,7 +321,6 @@ namespace smt {
                 sz_info& i = *kv.m_value;
                 if (is_leaf(&i) && (i.m_literal == null_literal || !is_true(i.m_literal))) {
                     rational value;
-                    expr* set = k->get_arg(0);
                     expr* sz  = k->get_arg(1);
                     if (!m_arith_value.get_value(sz, value)) {
                         return l_undef;

src/util/gparams.cpp

@@ -19,9 +19,9 @@ Notes:
 #include "util/gparams.h"
 #include "util/dictionary.h"
 #include "util/trace.h"
-#include <mutex>
+#include "util/mutex.h"
 
-static std::mutex gparams_mux;
+static mutex gparams_mux;
 
 extern void gparams_register_modules();
 
@@ -113,7 +113,7 @@ public:
     }
 
     void reset() {
-        std::lock_guard<std::mutex> lock(gparams_mux);
+        lock_guard lock(gparams_mux);
         m_params.reset();
         for (auto & kv : m_module_params) {
             dealloc(kv.m_value);
@@ -329,7 +329,7 @@ public:
         bool error = false;
         std::string error_msg;
         {
-            std::lock_guard<std::mutex> lock(gparams_mux);
+            lock_guard lock(gparams_mux);
             try {
                 symbol m, p;
                 normalize(name, m, p);
@@ -381,7 +381,7 @@ public:
         bool error = false;
         std::string error_msg;
         {
-            std::lock_guard<std::mutex> lock(gparams_mux);
+            lock_guard lock(gparams_mux);
             try {
                 symbol m, p;
                 normalize(name, m, p);
@@ -428,7 +428,7 @@ public:
         params_ref result;
         params_ref * ps = nullptr;
         {
-            std::lock_guard<std::mutex> lock(gparams_mux);
+            lock_guard lock(gparams_mux);
             if (m_module_params.find(module_name, ps)) {
                 result.copy(*ps);
             }
@@ -448,7 +448,7 @@ public:
 
     void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
         {
-            std::lock_guard<std::mutex> lock(gparams_mux);
+            lock_guard lock(gparams_mux);
             out << "Global parameters\n";
             get_param_descrs().display(out, indent + 4, smt2_style, include_descr);
             out << "\n";
@@ -470,7 +470,7 @@ public:
     }
 
     void display_modules(std::ostream & out) {
-        std::lock_guard<std::mutex> lock(gparams_mux);
+        lock_guard lock(gparams_mux);
         for (auto & kv : get_module_param_descrs()) {
             out << "[module] " << kv.m_key;
             char const * descr = nullptr;
@@ -484,7 +484,7 @@ public:
     void display_module(std::ostream & out, symbol const & module_name) {
         bool error = false;
         std::string error_msg;
-        std::lock_guard<std::mutex> lock(gparams_mux);
+        lock_guard lock(gparams_mux);
         try {
             param_descrs * d = nullptr;
             if (!get_module_param_descrs().find(module_name, d)) {
@@ -513,7 +513,7 @@ public:
         bool error = false;
         std::string error_msg;
         {
-            std::lock_guard<std::mutex> lock(gparams_mux);
+            lock_guard lock(gparams_mux);
             try {
                 symbol m, p;
                 normalize(name, m, p);

src/util/memory_manager.cpp

@@ -7,7 +7,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include<iostream>
 #include<stdlib.h>
 #include<climits>
-#include<mutex>
+#include "util/mutex.h"
 #include "util/trace.h"
 #include "util/memory_manager.h"
 #include "util/error_codes.h"
@@ -35,8 +35,8 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
 }
 
 
-static std::mutex g_memory_mux;
+static mutex g_memory_mux;
-static volatile bool g_memory_out_of_memory  = false;
+static atomic<bool> g_memory_out_of_memory(false);
 static bool       g_memory_initialized       = false;
 static long long  g_memory_alloc_size        = 0;
 static long long  g_memory_max_size          = 0;
@@ -55,10 +55,7 @@ void memory::exit_when_out_of_memory(bool flag, char const * msg) {
 }
 
 static void throw_out_of_memory() {
-    {
+    g_memory_out_of_memory = true;
-        std::lock_guard<std::mutex> lock(g_memory_mux);
-        g_memory_out_of_memory = true;
-    }
 
     if (g_exit_when_out_of_memory) {
         std::cerr << g_out_of_memory_msg << "\n";
@@ -92,7 +89,7 @@ mem_usage_report g_info;
 void memory::initialize(size_t max_size) {
     bool initialize = false;
     {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
+        lock_guard lock(g_memory_mux);
         // only update the maximum size if max_size != UINT_MAX
         if (max_size != UINT_MAX) 
             g_memory_max_size       = max_size;
@@ -116,12 +113,7 @@ void memory::initialize(size_t max_size) {
 }
 
 bool memory::is_out_of_memory() {
-    bool r = false;
+    return g_memory_out_of_memory;
-    {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
-        r = g_memory_out_of_memory;
-    }
-    return r;
 }
 
 void memory::set_high_watermark(size_t watermark) {
@@ -132,7 +124,7 @@ void memory::set_high_watermark(size_t watermark) {
 bool memory::above_high_watermark() {
     if (g_memory_watermark == 0)
         return false;
-    std::lock_guard<std::mutex> lock(g_memory_mux);
+    lock_guard lock(g_memory_mux);
     return g_memory_watermark < g_memory_alloc_size;
 }
 
@@ -161,7 +153,7 @@ void memory::finalize() {
 unsigned long long memory::get_allocation_size() {
     long long r;
     {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
+        lock_guard lock(g_memory_mux);
         r = g_memory_alloc_size;
     }
     if (r < 0)
@@ -172,7 +164,7 @@ unsigned long long memory::get_allocation_size() {
 unsigned long long memory::get_max_used_memory() {
     unsigned long long r;
     {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
+        lock_guard lock(g_memory_mux);
         r = g_memory_max_used_size;
     }
     return r;
@@ -256,7 +248,7 @@ static void synchronize_counters(bool allocating) {
     bool out_of_mem = false;
     bool counts_exceeded = false;
     {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
+        lock_guard lock(g_memory_mux);
         g_memory_alloc_size += g_memory_thread_alloc_size;
         g_memory_alloc_count += g_memory_thread_alloc_count;
         if (g_memory_alloc_size > g_memory_max_used_size)
@@ -337,7 +329,7 @@ void memory::deallocate(void * p) {
     size_t sz      = *sz_p;
     void * real_p  = reinterpret_cast<void*>(sz_p);
     {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
+        lock_guard lock(g_memory_mux);
         g_memory_alloc_size -= sz;
     }
     free(real_p);
@@ -347,7 +339,7 @@ void * memory::allocate(size_t s) {
     s = s + sizeof(size_t); // we allocate an extra field!
     bool out_of_mem = false, counts_exceeded = false;
     {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
+        lock_guard lock(g_memory_mux);
         g_memory_alloc_size += s;
         g_memory_alloc_count += 1;
         if (g_memory_alloc_size > g_memory_max_used_size)
@@ -377,7 +369,7 @@ void* memory::reallocate(void *p, size_t s) {
     s = s + sizeof(size_t); // we allocate an extra field!
     bool out_of_mem = false, counts_exceeded = false;
     {
-        std::lock_guard<std::mutex> lock(g_memory_mux);
+        lock_guard lock(g_memory_mux);
         g_memory_alloc_size += s - sz;
         g_memory_alloc_count += 1;
         if (g_memory_alloc_size > g_memory_max_used_size)

src/util/mpn.h

@@ -27,9 +27,14 @@ Revision History:
 typedef unsigned int mpn_digit;
 
 class mpn_manager {
+#ifndef SINGLE_THREAD
     std::recursive_mutex m_lock;
-#define MPN_BEGIN_CRITICAL() m_lock.lock();
+#define MPN_BEGIN_CRITICAL() m_lock.lock()
-#define MPN_END_CRITICAL() m_lock.unlock();
+#define MPN_END_CRITICAL() m_lock.unlock()
+#else
+#define MPN_BEGIN_CRITICAL() {}
+#define MPN_END_CRITICAL()   {}
+#endif
 
 public:
     mpn_manager();

src/util/mpz.h

@@ -135,9 +135,14 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); }
 template<bool SYNCH = true>
 class mpz_manager {
     mutable small_object_allocator  m_allocator;
-    mutable std::recursive_mutex         m_lock;
+#ifndef SINGLE_THREAD
-#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock();
+    mutable std::recursive_mutex    m_lock;
-#define MPZ_END_CRITICAL()   if (SYNCH) m_lock.unlock();
+#define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock()
+#define MPZ_END_CRITICAL()   if (SYNCH) m_lock.unlock()
+#else
+#define MPZ_BEGIN_CRITICAL() {}
+#define MPZ_END_CRITICAL()   {}
+#endif
     mutable mpn_manager             m_mpn_manager;
 
 #ifndef _MP_GMP
@@ -702,7 +707,11 @@ public:
     bool decompose(mpz const & n, svector<digit_t> & digits);
 };
 
+#ifndef SINGLE_THREAD
 typedef mpz_manager<true> synch_mpz_manager;
+#else
+typedef mpz_manager<false> synch_mpz_manager;
+#endif
 typedef mpz_manager<false> unsynch_mpz_manager;
 
 typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;

src/util/mutex.h

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    mutex.h
+
+Abstract:
+
+    Auxiliary macros for mutual exclusion
+
+--*/
+#pragma once
+
+#ifdef SINGLE_THREAD
+
+template<typename T> using atomic = T;
+
+struct mutex {
+  void lock() {}
+  void unlock() {}
+};
+
+struct lock_guard {
+  lock_guard(mutex &) {}
+};
+
+#else
+#include <atomic>
+#include <mutex>
+
+template<typename T> using atomic = std::atomic<T>;
+typedef std::mutex mutex;
+typedef std::lock_guard<std::mutex> lock_guard;
+#endif

src/util/prime_generator.cpp

@@ -17,7 +17,7 @@ Notes:
 
 --*/
 #include "util/prime_generator.h"
-#include <mutex>
+#include "util/mutex.h"
 
 #define PRIME_LIST_MAX_SIZE 1<<20
 
@@ -110,7 +110,7 @@ prime_iterator::prime_iterator(prime_generator * g):m_idx(0) {
     }
 }
 
-static std::mutex g_prime_iterator;
+static mutex g_prime_iterator;
 
 uint64_t prime_iterator::next() {
     unsigned idx = m_idx;
@@ -120,7 +120,7 @@ uint64_t prime_iterator::next() {
     }
     else {
         uint64_t r;
-        std::lock_guard<std::mutex> lock(g_prime_iterator);
+        lock_guard lock(g_prime_iterator);
         {
             r = (*m_generator)(idx);
         }
@@ -131,4 +131,3 @@ uint64_t prime_iterator::next() {
 void prime_iterator::finalize() {
     g_prime_generator.finalize();
 }
-

src/util/rational.cpp

@@ -17,12 +17,9 @@ Revision History:
 
 --*/
 #include<sstream>
-#include<mutex>
+#include "util/mutex.h"
 #include "util/util.h"
 #include "util/rational.h"
-#ifdef _WINDOWS
-#include<strsafe.h>
-#endif
 
 synch_mpq_manager *  rational::g_mpq_manager = nullptr;
 rational             rational::m_zero;
@@ -43,11 +40,11 @@ static void mk_power_up_to(vector<rational> & pws, unsigned n) {
     }
 }
 
-static std::mutex g_powers_of_two;
+static mutex g_powers_of_two;
 
 rational rational::power_of_two(unsigned k) {
     rational result;
-    std::lock_guard<std::mutex> lock(g_powers_of_two);
+    lock_guard lock(g_powers_of_two);
     {
         if (k >= m_powers_of_two.size())
             mk_power_up_to(m_powers_of_two, k+1);

src/util/rlimit.cpp

@@ -18,9 +18,10 @@ Revision History:
 --*/
 #include "util/rlimit.h"
 #include "util/common_msgs.h"
+#include "util/mutex.h"
 
 
-static std::mutex g_rlimit_mux;
+static mutex g_rlimit_mux;
 
 reslimit::reslimit():
     m_cancel(0),
@@ -72,34 +73,34 @@ char const* reslimit::get_cancel_msg() const {
 }
 
 void reslimit::push_child(reslimit* r) {
-    std::lock_guard<std::mutex> lock(g_rlimit_mux);
+    lock_guard lock(g_rlimit_mux);
     m_children.push_back(r);    
 }
 
 void reslimit::pop_child() {
-    std::lock_guard<std::mutex> lock(g_rlimit_mux);
+    lock_guard lock(g_rlimit_mux);
     m_children.pop_back();    
 }
 
 void reslimit::cancel() {
-    std::lock_guard<std::mutex> lock(g_rlimit_mux);
+    lock_guard lock(g_rlimit_mux);
     set_cancel(m_cancel+1);    
 }
 
 
 void reslimit::reset_cancel() {
-    std::lock_guard<std::mutex> lock(g_rlimit_mux);
+    lock_guard lock(g_rlimit_mux);
     set_cancel(0);    
 }
 
 void reslimit::inc_cancel() {
-    std::lock_guard<std::mutex> lock(g_rlimit_mux);
+    lock_guard lock(g_rlimit_mux);
     set_cancel(m_cancel+1);    
 }
 
 
 void reslimit::dec_cancel() {
-    std::lock_guard<std::mutex> lock(g_rlimit_mux);
+    lock_guard lock(g_rlimit_mux);
     if (m_cancel > 0) {
         set_cancel(m_cancel-1);
     }

src/util/rlimit.h

@@ -16,10 +16,8 @@ Author:
 Revision History:
 
 --*/
-#ifndef RLIMIT_H_
+#pragma once
-#define RLIMIT_H_
 
-#include <mutex>
 #include "util/vector.h"
 
 class reslimit {
@@ -29,14 +27,12 @@ class reslimit {
     uint64_t        m_limit;
     svector<uint64_t> m_limits;
     ptr_vector<reslimit> m_children;
-    std::mutex        m_mux;
 
     void set_cancel(unsigned f);
     friend class scoped_suspend_rlimit;
 
 public:
     reslimit();
-    ~reslimit() {}
     void push(unsigned delta_limit);
     void pop();
     void push_child(reslimit* r);
@@ -91,6 +87,3 @@ struct scoped_limits {
     ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); }
     void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
 };
-
-
-#endif

src/util/symbol.cpp

@@ -17,13 +17,13 @@ Revision History:
 
 --*/
 #include "util/symbol.h"
+#include "util/mutex.h"
 #include "util/str_hashtable.h"
 #include "util/region.h"
 #include "util/string_buffer.h"
 #include <cstring>
-#include <mutex>
 
-static std::mutex g_symbol_lock;
+static mutex g_symbol_lock;
 
 symbol symbol::m_dummy(TAG(void*, nullptr, 2));
 const symbol symbol::null;
@@ -38,7 +38,7 @@ public:
 
     char const * get_str(char const * d) {
         const char * result;
-        std::lock_guard<std::mutex> lock(g_symbol_lock);
+        lock_guard lock(g_symbol_lock);
         str_hashtable::entry * e;
         if (m_table.insert_if_not_there_core(d, e)) {
             // new entry

src/util/z3_exception.cpp

@@ -16,7 +16,6 @@ Author:
 Notes:
 
 --*/
-#include<sstream>
 #include<stdarg.h>
 #include<sstream>
 #include "util/z3_exception.h"