From f3cd7d646d021a02d6d1dbc6a419ec22668b5158 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 10:42:42 +0000 Subject: [PATCH 1/9] further simplifications to scoped_timer --- src/util/scoped_timer.cpp | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index e3b96fa15..58416289a 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -26,39 +26,33 @@ Revision History: struct scoped_timer::imp { - event_handler * m_eh; +private: std::thread m_thread; std::timed_mutex m_mutex; - unsigned m_ms; - static void* thread_func(imp * st) { - auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(st->m_ms); + static void thread_func(unsigned ms, event_handler * eh, std::timed_mutex * mutex) { + auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(ms); - while (!st->m_mutex.try_lock_until(end)) { - if (std::chrono::steady_clock::now() > end) { - st->m_eh->operator()(TIMEOUT_EH_CALLER); - return nullptr; - } + while (!mutex->try_lock_until(end)) { + if (std::chrono::steady_clock::now() >= end) { + eh->operator()(TIMEOUT_EH_CALLER); + return; + } } - st->m_mutex.unlock(); - return nullptr; + mutex->unlock(); } - imp(unsigned ms, event_handler * eh): - m_eh(eh), m_ms(ms) { +public: + imp(unsigned ms, event_handler * eh) { m_mutex.lock(); - m_thread = std::thread(thread_func, this); + m_thread = std::thread(thread_func, ms, eh, &m_mutex); } ~imp() { m_mutex.unlock(); - while (!m_thread.joinable()) { - std::this_thread::yield(); - } m_thread.join(); } - }; scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { @@ -69,6 +63,5 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { } scoped_timer::~scoped_timer() { - if (m_imp) - dealloc(m_imp); + dealloc(m_imp); } From a76c0fbbfbb7e0e80c5d491da99fb6b56f408139 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 11:49:41 +0000 Subject: [PATCH 2/9] simplify timeout mechanism and fix race conditions there --- src/shell/main.cpp | 7 +++++-- src/util/timeout.cpp | 26 ++++++++++---------------- 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/src/shell/main.cpp b/src/shell/main.cpp index b036628b1..260cf8a79 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -115,6 +115,7 @@ void display_usage() { } void parse_cmd_line_args(int argc, char ** argv) { + long timeout = 0; int i = 1; char * eq_pos = nullptr; while (i < argc) { @@ -216,8 +217,7 @@ void parse_cmd_line_args(int argc, char ** argv) { else if (strcmp(opt_name, "T") == 0) { if (!opt_arg) error("option argument (-T:timeout) is missing."); - long tm = strtol(opt_arg, nullptr, 10); - set_timeout(tm * 1000); + timeout = strtol(opt_arg, nullptr, 10); } else if (strcmp(opt_name, "t") == 0) { if (!opt_arg) @@ -292,6 +292,9 @@ void parse_cmd_line_args(int argc, char ** argv) { } i++; } + + if (timeout) + set_timeout(timeout * 1000); } diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp index ad02a747d..1a92ae867 100644 --- a/src/util/timeout.cpp +++ b/src/util/timeout.cpp @@ -19,7 +19,6 @@ Revision History: --*/ #include -#include "util/z3_omp.h" #include "util/util.h" #include "util/timeout.h" #include "util/error_codes.h" @@ -34,26 +33,21 @@ namespace { class g_timeout_eh : public event_handler { public: void operator()(event_handler_caller_t caller_id) override { - #pragma omp critical (g_timeout_cs) - { - std::cout << "timeout\n"; - m_caller_id = caller_id; - if (g_on_timeout) - g_on_timeout(); - if (g_timeout) - delete g_timeout; - g_timeout = nullptr; - throw z3_error(ERR_TIMEOUT); - } + std::cout << "timeout\n"; + m_caller_id = caller_id; + if (g_on_timeout) + g_on_timeout(); + throw z3_error(ERR_TIMEOUT); } }; } -void set_timeout(long ms) { - if (g_timeout) - delete g_timeout; +static g_timeout_eh eh; - g_timeout = new scoped_timer(ms, new g_timeout_eh()); +void set_timeout(long ms) { + SASSERT(!g_timeout); + // this is leaked, but since it's only used in the shell, it's ok + g_timeout = new scoped_timer(ms, &eh); } void register_on_timeout_proc(void (*proc)()) { From 3a5263be9544a9801da9cf6b8397e5bf7819e77c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 13:30:27 +0000 Subject: [PATCH 3/9] modernize stopwatch --- src/util/stopwatch.h | 182 ++++++++----------------------------------- 1 file changed, 33 insertions(+), 149 deletions(-) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index a11a87484..44d7a104b 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -20,171 +20,55 @@ Revision History: #ifndef STOPWATCH_H_ #define STOPWATCH_H_ -#if defined(_WINDOWS) || defined(_CYGWIN) || defined(_MINGW) - -// Does this redefinition work? - -#include +#include "util/debug.h" +#include class stopwatch { -private: - LARGE_INTEGER m_elapsed; - LARGE_INTEGER m_last_start_time; - LARGE_INTEGER m_last_stop_time; - LARGE_INTEGER m_frequency; + std::chrono::time_point m_start; + std::chrono::steady_clock::duration m_elapsed; +#if Z3DEBUG + bool m_running = false; +#endif + + static std::chrono::time_point get() { + return std::chrono::steady_clock::now(); + } public: stopwatch() { - QueryPerformanceFrequency(&m_frequency); - reset(); + reset(); } - ~stopwatch() {}; - - void add (const stopwatch &s) {/* TODO */} - - void reset() { m_elapsed.QuadPart = 0; } - - void start() { - QueryPerformanceCounter(&m_last_start_time); - } - - void stop() { - QueryPerformanceCounter(&m_last_stop_time); - m_elapsed.QuadPart += m_last_stop_time.QuadPart - m_last_start_time.QuadPart; + void add(const stopwatch &s) { + m_elapsed += s.m_elapsed; } - double get_seconds() const { - return static_cast(m_elapsed.QuadPart / static_cast(m_frequency.QuadPart)) ; + void reset() { + m_elapsed = std::chrono::steady_clock::duration::zero(); + } + + void start() { + SASSERT(!m_running); + DEBUG_CODE(m_running = true); + m_start = get(); + } + + void stop() { + SASSERT(m_running); + DEBUG_CODE(m_running = false); + m_elapsed += get() - m_start; + } + + double get_seconds() const { + return std::chrono::duration_cast(m_elapsed).count() / 1000.0; } double get_current_seconds() const { - LARGE_INTEGER t; - QueryPerformanceCounter(&t); - return static_cast( (t.QuadPart - m_last_start_time.QuadPart) / static_cast(m_frequency.QuadPart)); + return std::chrono::duration_cast(get() - m_start).count() / 1000.0; } }; -#undef max -#undef min - - -#elif defined(__APPLE__) && defined (__MACH__) // macOS - -#include -#include - -class stopwatch { - unsigned long long m_time; // elapsed time in ns - bool m_running; - clock_serv_t m_host_clock; - mach_timespec_t m_start; - -public: - stopwatch():m_time(0), m_running(false) { - host_get_clock_service(mach_host_self(), SYSTEM_CLOCK, &m_host_clock); - } - - ~stopwatch() {} - - void add (const stopwatch &s) {m_time += s.m_time;} - - void reset() { - m_time = 0ull; - } - - void start() { - if (!m_running) { - clock_get_time(m_host_clock, &m_start); - m_running = true; - } - } - - void stop() { - if (m_running) { - mach_timespec_t _stop; - clock_get_time(m_host_clock, &_stop); - m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - m_time += (_stop.tv_nsec - m_start.tv_nsec); - m_running = false; - } - } - - double get_seconds() const { - if (m_running) { - const_cast(this)->stop(); - /* update m_time */ - const_cast(this)->start(); - } - return static_cast(m_time)/static_cast(1000000000ull); - } - - double get_current_seconds() const { - return get_seconds(); - } -}; - - -#else // Linux - -#include - -#ifndef CLOCK_PROCESS_CPUTIME_ID -/* BSD */ -# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC -#endif - -class stopwatch { - unsigned long long m_time; // elapsed time in ns - bool m_running; - struct timespec m_start; - -public: - stopwatch():m_time(0), m_running(false) { - } - - ~stopwatch() {} - - void add (const stopwatch &s) {m_time += s.m_time;} - - void reset() { - m_time = 0ull; - } - - void start() { - if (!m_running) { - clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &m_start); - m_running = true; - } - } - - void stop() { - if (m_running) { - struct timespec _stop; - clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &_stop); - m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec) - m_time += (_stop.tv_nsec - m_start.tv_nsec); - m_running = false; - } - } - - double get_seconds() const { - if (m_running) { - const_cast(this)->stop(); - /* update m_time */ - const_cast(this)->start(); - } - return static_cast(m_time)/static_cast(1000000000ull); - } - - double get_current_seconds() const { - return get_seconds(); - } -}; - -#endif struct scoped_watch { stopwatch &m_sw; From 3a7c467822f6792a57fb9b97a707efec1683bbfa Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 13:33:52 +0000 Subject: [PATCH 4/9] fix debug build.. --- src/util/stopwatch.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 44d7a104b..e35380153 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -50,13 +50,13 @@ public: void start() { SASSERT(!m_running); - DEBUG_CODE(m_running = true); + DEBUG_CODE(m_running = true;); m_start = get(); } void stop() { SASSERT(m_running); - DEBUG_CODE(m_running = false); + DEBUG_CODE(m_running = false;); m_elapsed += get() - m_start; } From 85162d90d1c68838f150704c672e82a457922e54 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 13:57:38 +0000 Subject: [PATCH 5/9] simplify timer.h --- src/util/timer.cpp | 40 ---------------------------------------- src/util/timer.h | 28 ++++++++++++++++++---------- 2 files changed, 18 insertions(+), 50 deletions(-) delete mode 100644 src/util/timer.cpp diff --git a/src/util/timer.cpp b/src/util/timer.cpp deleted file mode 100644 index 2d80b732c..000000000 --- a/src/util/timer.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - timer.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2009-01-06. - -Revision History: - ---*/ -#include "util/util.h" -#include "util/memory_manager.h" -#include "util/stopwatch.h" -#include "util/timer.h" - -timer::timer(){ - m_watch = alloc(stopwatch); - start(); -} - -timer::~timer() { - dealloc(m_watch); -} - -void timer::start() { - m_watch->start(); -} - -double timer::get_seconds() { - return m_watch->get_current_seconds(); -} - diff --git a/src/util/timer.h b/src/util/timer.h index b4a69f8bf..37566e613 100644 --- a/src/util/timer.h +++ b/src/util/timer.h @@ -19,21 +19,29 @@ Revision History: #ifndef TIMER_H_ #define TIMER_H_ -class stopwatch; +#include "util/stopwatch.h" /** - \brief Wrapper for the stopwatch class. It hides windows.h dependency. + \brief Wrapper for the stopwatch class. */ class timer { - stopwatch * m_watch; + stopwatch m_watch; public: - timer(); - ~timer(); - void start(); - double get_seconds(); - bool timeout(unsigned secs) { return secs > 0 && secs != UINT_MAX && get_seconds() > secs; } - bool ms_timeout(unsigned ms) { return ms > 0 && ms != UINT_MAX && get_seconds() * 1000 > ms; } + void start() { + m_watch.start(); + } + + double get_seconds() const { + return m_watch.get_current_seconds(); + } + + bool timeout(unsigned secs) const { + return secs != 0 && secs != UINT_MAX && get_seconds() > secs; + } + + bool ms_timeout(unsigned ms) const { + return ms != 0 && ms != UINT_MAX && get_seconds() * 1000 > ms; + } }; #endif /* TIMER_H_ */ - From 2f33bafd5a7696a57a04555bc6521063f069ef59 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 14:59:31 +0000 Subject: [PATCH 6/9] stopwatches: fix a few places that would call start/stop multiple times --- src/muz/rel/dl_instruction.cpp | 11 +++++------ src/sat/sat_local_search.cpp | 1 - src/smt/smt_context.cpp | 1 - src/util/timer.h | 2 +- 4 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 2b76d99f7..79508a4f6 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -41,7 +41,6 @@ namespace datalog { execution_context::~execution_context() { reset(); - dealloc(m_stopwatch); } void execution_context::reset() { @@ -104,15 +103,15 @@ namespace datalog { m_timelimit_ms = time_in_ms; if (!m_stopwatch) { m_stopwatch = alloc(stopwatch); + } else { + m_stopwatch->stop(); + m_stopwatch->reset(); } - m_stopwatch->stop(); - m_stopwatch->reset(); m_stopwatch->start(); } void execution_context::reset_timelimit() { - if (m_stopwatch) { - m_stopwatch->stop(); - } + dealloc(m_stopwatch); + m_stopwatch = nullptr; m_timelimit_ms = 0; } diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 7c3ebb688..cdb90e2a0 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -515,7 +515,6 @@ namespace sat { reinit(); DEBUG_CODE(verify_slack();); timer timer; - timer.start(); unsigned step = 0, total_flips = 0, tries = 0; for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 86b3374fc..ecb69b418 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3496,7 +3496,6 @@ namespace smt { m_case_split_queue ->init_search_eh(); m_next_progress_sample = 0; TRACE("literal_occ", display_literal_num_occs(tout);); - m_timer.start(); } void context::end_search() { diff --git a/src/util/timer.h b/src/util/timer.h index 37566e613..e2ddb55e7 100644 --- a/src/util/timer.h +++ b/src/util/timer.h @@ -27,7 +27,7 @@ Revision History: class timer { stopwatch m_watch; public: - void start() { + timer() { m_watch.start(); } From 3d7878bafc228877c77891a8985e78c21f780664 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 15:25:26 +0000 Subject: [PATCH 7/9] hopefully fix build with VS 2012 --- src/util/stopwatch.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index e35380153..e8665054b 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -31,7 +31,8 @@ class stopwatch bool m_running = false; #endif - static std::chrono::time_point get() { + // FIXME: just use auto with VS 2015+ + static decltype(std::chrono::steady_clock::now()) get() { return std::chrono::steady_clock::now(); } From 6598aedbb206986a9e48e5c1fe3b7ce807f97895 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 15:52:52 +0000 Subject: [PATCH 8/9] fix VS build, take 2 --- src/sat/sat_solver.cpp | 3 +++ src/util/CMakeLists.txt | 1 - src/util/stopwatch.h | 11 +++++++---- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3deb6fc17..8b7d53897 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -27,6 +27,9 @@ Revision History: #include "util/trace.h" #include "util/max_cliques.h" #include "util/gparams.h" +#ifdef _MSC_VER +# include +#endif // define to update glue during propagation #define UPDATE_GLUE diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index b6abb785f..5b1f336d1 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -56,7 +56,6 @@ z3_add_component(util symbol.cpp timeit.cpp timeout.cpp - timer.cpp trace.cpp util.cpp warning.cpp diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index e8665054b..5fe10fb3b 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -25,14 +25,17 @@ Revision History: class stopwatch { - std::chrono::time_point m_start; - std::chrono::steady_clock::duration m_elapsed; + typedef decltype(std::chrono::steady_clock::now()) clock_t; + typedef decltype(std::chrono::steady_clock::now() - std::chrono::steady_clock::now()) duration_t; + + clock_t m_start; + duration_t m_elapsed; #if Z3DEBUG bool m_running = false; #endif // FIXME: just use auto with VS 2015+ - static decltype(std::chrono::steady_clock::now()) get() { + static clock_t get() { return std::chrono::steady_clock::now(); } @@ -46,7 +49,7 @@ public: } void reset() { - m_elapsed = std::chrono::steady_clock::duration::zero(); + m_elapsed = duration_t::zero(); } void start() { From bb7aa16223965644a65e7f5f4eaf050fb5ef8058 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 21 Feb 2019 16:38:48 +0000 Subject: [PATCH 9/9] stopwatch: fix debug build crash in sat solver --- src/util/stopwatch.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 5fe10fb3b..1135c893e 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -50,6 +50,7 @@ public: void reset() { m_elapsed = duration_t::zero(); + DEBUG_CODE(m_running = false;); } void start() {