From 3036b88f094fc5a468aa3ea04fb8fb5de0830563 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Oct 2021 13:35:23 +0200 Subject: [PATCH] support threading for TRACE mode --- src/math/simplex/bit_matrix.cpp | 1 + src/solver/assertions/asserted_formulas.cpp | 12 +++---- src/util/small_object_allocator.h | 1 + src/util/trace.cpp | 19 ++++++++++ src/util/trace.h | 40 ++++++++++++++++++--- src/util/util.cpp | 18 ---------- src/util/util.h | 28 +-------------- 7 files changed, 64 insertions(+), 55 deletions(-) diff --git a/src/math/simplex/bit_matrix.cpp b/src/math/simplex/bit_matrix.cpp index fa4b481b5..097dd4396 100644 --- a/src/math/simplex/bit_matrix.cpp +++ b/src/math/simplex/bit_matrix.cpp @@ -15,6 +15,7 @@ Notes: #include "math/simplex/bit_matrix.h" #include "util/stopwatch.h" +#include "util/trace.h" #include diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 9e9b54140..b3be7e8ab 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -213,13 +213,13 @@ void asserted_formulas::force_push() { } void asserted_formulas::pop_scope(unsigned num_scopes) { - if (m_lazy_scopes > 0) { - unsigned n = std::min(num_scopes, m_lazy_scopes); - m_lazy_scopes -= n; - num_scopes -= n; - if (num_scopes == 0) - return; + if (num_scopes <= m_lazy_scopes) { + m_lazy_scopes -= num_scopes; + return; } + num_scopes -= m_lazy_scopes; + m_lazy_scopes = 0; + TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";); m_bv_sharing.pop_scope(num_scopes); m_macro_manager.pop_scope(num_scopes); diff --git a/src/util/small_object_allocator.h b/src/util/small_object_allocator.h index 028c79645..05fe32ef0 100644 --- a/src/util/small_object_allocator.h +++ b/src/util/small_object_allocator.h @@ -21,6 +21,7 @@ Revision History: #include "util/machine.h" #include "util/debug.h" +#include "util/trace.h" class small_object_allocator { static const unsigned CHUNK_SIZE = (8192 - sizeof(void*)*2); diff --git a/src/util/trace.cpp b/src/util/trace.cpp index 5e2930999..d6e6323fc 100644 --- a/src/util/trace.cpp +++ b/src/util/trace.cpp @@ -19,6 +19,25 @@ Revision History: #include "util/trace.h" #include "util/str_hashtable.h" +#ifndef SINGLE_THREAD +#include +#include + +static std::mutex g_verbose_mux; +void verbose_lock() { g_verbose_mux.lock(); } +void verbose_unlock() { g_verbose_mux.unlock(); } + +static std::thread::id g_thread_id = std::this_thread::get_id(); +static bool g_is_threaded = false; + +bool is_threaded() { + if (g_is_threaded) return true; + g_is_threaded = std::this_thread::get_id() != g_thread_id; + return g_is_threaded; +} + +#endif + #ifdef _TRACE std::ofstream tout(".z3-trace"); diff --git a/src/util/trace.h b/src/util/trace.h index fad4707c0..2a63bfaf9 100644 --- a/src/util/trace.h +++ b/src/util/trace.h @@ -21,6 +21,33 @@ Revision History: #include +#ifdef SINGLE_THREAD +# define is_threaded() false +#else +bool is_threaded(); +#endif + +#ifdef SINGLE_THREAD +#define LOCK_CODE(CODE) CODE; +#define THREAD_LOCK(CODE) CODE + +#else +void verbose_lock(); +void verbose_unlock(); + +#define LOCK_CODE(CODE) \ + { \ + verbose_lock(); \ + CODE; \ + verbose_unlock(); \ + } + +#define THREAD_LOCK(CODE) if (is_threaded()) { LOCK_CODE(CODE); } else { CODE; } + +#endif + + + #ifdef _TRACE extern std::ofstream tout; #define TRACE_CODE(CODE) { CODE } ((void) 0 ) @@ -48,10 +75,15 @@ static inline void open_trace() {} static inline void finalize_trace() {} #endif -#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); }) +#define TRACEH(TAG) tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n" +#define TRACEEND tout << "------------------------------------------------\n" +#define TRACEBODY(TAG, CODE) TRACEH(TAG); CODE; TRACEEND; tout.flush() +#define STRACEBODY(CODE) CODE; tout.flush() -#define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); }) +#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); }) -#define SCTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { CODE tout.flush(); }) +#define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { THREAD_LOCK(STRACEBODY(CODE)); }) -#define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); }) +#define SCTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { THREAD_LOCK(STRACEBODY(CODE)); }) + +#define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { THREAD_LOCK(TRACEBODY(TAG, CODE)); }) diff --git a/src/util/util.cpp b/src/util/util.cpp index 714c947a9..a59b26990 100644 --- a/src/util/util.cpp +++ b/src/util/util.cpp @@ -19,14 +19,6 @@ Revision History: #include "util/util.h" -#ifndef SINGLE_THREAD -#include -#include - -static std::mutex g_verbose_mux; -void verbose_lock() { g_verbose_mux.lock(); } -void verbose_unlock() { g_verbose_mux.unlock(); } -#endif static unsigned g_verbosity_level = 0; @@ -44,16 +36,6 @@ void set_verbose_stream(std::ostream& str) { g_verbose_stream = &str; } -#ifndef SINGLE_THREAD -static std::thread::id g_thread_id = std::this_thread::get_id(); -static bool g_is_threaded = false; - -bool is_threaded() { - if (g_is_threaded) return true; - g_is_threaded = std::this_thread::get_id() != g_thread_id; - return g_is_threaded; -} -#endif std::ostream& verbose_stream() { return *g_verbose_stream; diff --git a/src/util/util.h b/src/util/util.h index 8d3682943..4cac2123a 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -169,37 +169,11 @@ void set_verbosity_level(unsigned lvl); unsigned get_verbosity_level(); std::ostream& verbose_stream(); void set_verbose_stream(std::ostream& str); -#ifdef SINGLE_THREAD -# define is_threaded() false -#else -bool is_threaded(); -#endif -#define IF_VERBOSE(LVL, CODE) { \ - if (get_verbosity_level() >= LVL) { \ - if (is_threaded()) { \ - LOCK_CODE(CODE); \ - } \ - else { \ - CODE; \ - } \ - } } ((void) 0) +#define IF_VERBOSE(LVL, CODE) { if (get_verbosity_level() >= LVL) { THREAD_LOCK(CODE); } } ((void) 0) -#ifdef SINGLE_THREAD -#define LOCK_CODE(CODE) CODE; -#else -void verbose_lock(); -void verbose_unlock(); - -#define LOCK_CODE(CODE) \ - { \ - verbose_lock(); \ - CODE; \ - verbose_unlock(); \ - } -#endif template struct default_eq {