From 8f2fe273ea07e9eebc26a63d1bbb508ff899716c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Dec 2013 14:56:48 -0800 Subject: [PATCH] refactor(*): isolate std::thread dependency This commit allows us to build Lean without the pthread dependency. It is also useful if we want to implement multi-threading on top of Boost. Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 15 ++-- src/frontends/lean/frontend.cpp | 3 +- src/kernel/builtin.h | 20 ++--- src/kernel/environment.cpp | 15 ++-- src/kernel/expr.cpp | 4 +- src/kernel/expr.h | 4 +- src/kernel/threadsafe_environment.h | 4 +- src/library/io_state.cpp | 4 +- src/library/tactic/tactic.cpp | 2 +- src/library/tactic/tactic.h | 2 +- src/shell/CMakeLists.txt | 2 +- src/tests/kernel/normalizer.cpp | 6 +- src/tests/kernel/threads.cpp | 9 +- src/tests/kernel/type_checker.cpp | 6 +- src/tests/library/arith.cpp | 6 +- src/tests/library/tactic/tactic.cpp | 8 +- src/tests/util/lazy_list.cpp | 2 +- src/tests/util/thread.cpp | 78 ++++++++--------- src/util/exception.cpp | 5 +- src/util/interrupt.cpp | 15 ++-- src/util/interrupt.h | 13 ++- src/util/interruptable_ptr.h | 10 +-- src/util/interval/interval.cpp | 46 +++++------ src/util/interval/interval_instances.cpp | 1 + src/util/lazy_list_fn.h | 19 +++-- src/util/memory.cpp | 12 +-- src/util/name.cpp | 8 +- src/util/numerics/double.cpp | 3 +- src/util/numerics/double.h | 8 +- src/util/numerics/float.cpp | 3 +- src/util/numerics/float.h | 2 +- src/util/numerics/mpbq.cpp | 21 ++--- src/util/numerics/mpbq.h | 3 +- src/util/numerics/mpfp.cpp | 3 +- src/util/numerics/mpfp.h | 16 ++-- src/util/numerics/mpq.cpp | 5 +- src/util/numerics/mpz.cpp | 5 +- src/util/numerics/primes.cpp | 6 +- src/util/rc.h | 30 +++---- src/util/script_state.cpp | 42 +++++----- src/util/script_state.h | 8 +- src/util/sexpr/format.cpp | 2 +- src/util/shared_mutex.cpp | 34 ++++---- src/util/shared_mutex.h | 18 ++-- src/util/splay_tree.h | 5 +- src/util/stackinfo.cpp | 62 ++++++++++---- src/util/stackinfo.h | 2 + src/util/thread.h | 101 +++++++++++++++++++++++ src/util/trace.cpp | 2 +- src/util/trace.h | 6 +- src/util/unlock_guard.h | 8 +- 51 files changed, 417 insertions(+), 297 deletions(-) create mode 100644 src/util/thread.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6de61c2e2..00e54dc08 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -7,7 +7,7 @@ set(CMAKE_COLOR_MAKEFILE ON) enable_testing() option(TRACK_MEMORY_USAGE "TRACK_MEMORY_USAGE" ON) -option(THREAD_SAFE "THREAD_SAFE" ON) +option(MULTI_THREAD "MULTI_THREAD" ON) # Added for CTest INCLUDE(CTest) @@ -26,9 +26,10 @@ if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows")) set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS -D LEAN_WIN_STACK_SIZE=${LEAN_WIN_STACK_SIZE}") 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") +if("${MULTI_THREAD}" MATCHES "OFF") + message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel") +else() + set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_MULTI_THREAD") endif() # Set Module Path @@ -173,7 +174,11 @@ add_subdirectory(frontends/lean) set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) add_subdirectory(frontends/lua) set(LEAN_LIBS ${LEAN_LIBS} leanlua) -set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}") +if("${MULTI_THREAD}" MATCHES "ON") + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}") +else() + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}") +endif() set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage") set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) add_subdirectory(shell) diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index b691f3ee2..0351c5887 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include #include #include #include - +#include "util/thread.h" #include "util/map.h" #include "util/sstream.h" #include "util/exception.h" diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index 6bcb2701d..52898d232 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -195,21 +195,21 @@ void import_basic(environment & env); */ #define MK_BUILTIN(Name, ClassName) \ expr mk_##Name() { \ - static thread_local expr r = mk_value(*(new ClassName())); \ + static LEAN_THREAD_LOCAL expr r = mk_value(*(new ClassName())); \ return r; \ -} \ +} /** \brief Helper macro for generating "defined" constants. */ -#define MK_CONSTANT(Name, NameObj) \ -static name Name ## _name = NameObj; \ -expr mk_##Name() { \ - static thread_local expr r = mk_constant(Name ## _name); \ - return r ; \ -} \ -bool is_ ## Name(expr const & e) { \ - return is_constant(e) && const_name(e) == Name ## _name; \ +#define MK_CONSTANT(Name, NameObj) \ +static name Name ## _name = NameObj; \ +expr mk_##Name() { \ + static LEAN_THREAD_LOCAL expr r = mk_constant(Name ## _name); \ + return r ; \ +} \ +bool is_ ## Name(expr const & e) { \ + return is_constant(e) && const_name(e) == Name ## _name; \ } #define MK_IS_BUILTIN(Name, Builtin) \ diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 7cbc25a29..cc0e15d53 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -7,11 +7,10 @@ Author: Leonardo de Moura #include #include #include -#include #include #include #include -#include +#include "util/thread.h" #include "util/safe_arith.h" #include "util/realpath.h" #include "kernel/for_each_fn.h" @@ -26,17 +25,17 @@ namespace lean { static name g_builtin_module("builtin_module"); class extension_factory { std::vector m_makers; - std::mutex m_makers_mutex; + mutex m_makers_mutex; public: unsigned register_extension(environment::mk_extension mk) { - std::lock_guard lock(m_makers_mutex); + lock_guard lock(m_makers_mutex); unsigned r = m_makers.size(); m_makers.push_back(mk); return r; } std::unique_ptr mk(unsigned extid) { - std::lock_guard lock(m_makers_mutex); + lock_guard lock(m_makers_mutex); return m_makers[extid](); } }; @@ -61,11 +60,7 @@ struct environment::imp { std::vector m_constraints; std::vector m_uvars; // Children environment management -#ifdef LEAN_THREAD_UNSAFE - unsigned m_num_children; -#else - std::atomic m_num_children; -#endif + atomic m_num_children; std::shared_ptr m_parent; // Object management std::vector m_objects; diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 9d826f0ad..7bde07b8b 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -45,7 +45,7 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv): // Remark: using pointer address as a hash code is not a good idea. // - each execution run will behave differently. // - the hash is not diverse enough - static thread_local unsigned g_hash_alloc_counter = 0; + static LEAN_THREAD_LOCAL unsigned g_hash_alloc_counter = 0; m_hash_alloc = g_hash_alloc_counter; g_hash_alloc_counter++; } @@ -218,7 +218,7 @@ void expr_cell::dealloc() { } expr mk_type() { - static thread_local expr r = mk_type(level()); + static LEAN_THREAD_LOCAL expr r = mk_type(level()); return r; } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 9aa897f4b..54063b688 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -6,11 +6,11 @@ Author: Leonardo de Moura */ #pragma once #include -#include #include #include #include #include +#include "util/thread.h" #include "util/lua.h" #include "util/rc.h" #include "util/name.h" @@ -71,7 +71,7 @@ protected: #ifdef LEAN_THREAD_UNSAFE unsigned short m_flags; #else - std::atomic_ushort m_flags; + atomic_ushort m_flags; #endif unsigned m_hash; // hash based on the structure of the expression (this is a good hash for structural equality) unsigned m_hash_alloc; // hash based on 'time' of allocation (this is a good hash for pointer-based equality) diff --git a/src/kernel/threadsafe_environment.h b/src/kernel/threadsafe_environment.h index 19d2aa9fc..aad2b52c6 100644 --- a/src/kernel/threadsafe_environment.h +++ b/src/kernel/threadsafe_environment.h @@ -31,8 +31,8 @@ public: \brief See \c read_only_environment */ class read_write_environment { - environment m_env; - unique_lock m_lock; + environment m_env; + exclusive_lock m_lock; public: read_write_environment(environment const & env); ~read_write_environment(); diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index c172e04fe..bf1b7069b 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -121,7 +121,7 @@ int io_state_set_options(lua_State * L) { return 0; } -static std::mutex g_print_mutex; +static mutex g_print_mutex; static void print(io_state * ios, bool reg, char const * msg) { if (ios) { @@ -136,7 +136,7 @@ static void print(io_state * ios, bool reg, char const * msg) { /** \brief Thread safe version of print function */ static int print(lua_State * L, int start, bool reg) { - std::lock_guard lock(g_print_mutex); + lock_guard lock(g_print_mutex); io_state * ios = get_io_state(L); int n = lua_gettop(L); int i; diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 02e661529..b3783f932 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -689,7 +689,7 @@ static int mk_lua_tactic01(lua_State * L) { }); while (!done) { check_interrupted(); - std::this_thread::yield(); // give another thread a chance to execute + this_thread::yield(); // give another thread a chance to execute S_copy.exec_protected([&]() { done = resume(co, 0); }); diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index d6f7f82d7..2971b1ba5 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include #include #include -#include #include +#include "util/thread.h" #include "util/lazy_list.h" #include "library/io_state.h" #include "library/tactic/proof_state.h" diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index cb19253bd..074c17886 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -75,7 +75,7 @@ ENDFOREACH(T) # LEAN LUA THREAD TESTS if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux")) - if ((NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) AND (${THREAD_SAFE} MATCHES "ON")) + if ((NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) AND (${MULTI_THREAD} MATCHES "ON")) file(GLOB LEANLUATHREADTESTS "${LEAN_SOURCE_DIR}/../tests/lua/threads/*.lua") FOREACH(T ${LEANLUATHREADTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index b36468979..acd3d6f4d 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include #include +#include "util/thread.h" #include "util/test.h" #include "util/trace.h" #include "util/exception.h" @@ -213,7 +213,7 @@ static expr mk_big(unsigned depth) { } static void tst5() { -#ifndef __APPLE__ +#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env = mk_toplevel(); env.add_var("f", Bool >> (Bool >> Bool)); @@ -230,7 +230,7 @@ static void tst5() { std::cout << "interrupted\n"; } }); - std::this_thread::sleep_for(dura); + this_thread::sleep_for(dura); thread.request_interrupt(); thread.join(); #endif diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index 855f8ea05..0bf7e98ac 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include -#include #include +#include "util/thread.h" #include "util/test.h" #include "kernel/expr.h" #include "kernel/free_vars.h" @@ -48,11 +47,11 @@ static void tst1() { expr a = Const("a"); expr f = Const("f"); a = f(a, a); - std::vector ts; + std::vector ts; - #if !defined(__APPLE__) && !defined(LEAN_THREAD_UNSAFE) + #if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) for (unsigned i = 0; i < 8; i++) { - ts.push_back(std::thread([&](){ save_stack_info(); mk(a); })); + ts.push_back(thread([&](){ save_stack_info(); mk(a); })); } for (unsigned i = 0; i < 8; i++) { ts[i].join(); diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 2434cf2a6..e64cf43be 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include #include #include +#include "util/thread.h" #include "util/test.h" #include "util/trace.h" #include "util/exception.h" @@ -221,7 +221,7 @@ static expr mk_big(unsigned depth) { } static void tst12() { -#ifndef __APPLE__ +#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env = mk_toplevel(); env.add_var("f", Int >> (Int >> Int)); @@ -238,7 +238,7 @@ static void tst12() { std::cout << "interrupted\n"; } }); - std::this_thread::sleep_for(dura); + this_thread::sleep_for(dura); thread.request_interrupt(); thread.join(); #endif diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index dfffb1dbc..e0b47f4c2 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include +#include "util/thread.h" #include "util/test.h" #include "kernel/builtin.h" #include "kernel/normalizer.h" @@ -122,9 +122,9 @@ static void tst6() { std::cout << mk_int_add_fn().raw() << "\n"; #ifndef __APPLE__ - std::thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_int_add_fn().raw() << "\n"; }); + thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_int_add_fn().raw() << "\n"; }); t1.join(); - std::thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_int_add_fn().raw() << "\n"; }); + thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_int_add_fn().raw() << "\n"; }); t2.join(); #endif std::cout << mk_int_add_fn().raw() << "\n"; diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index b2427f215..d24795d5a 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -26,7 +26,7 @@ tactic loop_tactic() { }); } -tactic set_tactic(std::atomic * flag) { +tactic set_tactic(atomic * flag) { return mk_tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state { *flag = true; return s; @@ -65,14 +65,14 @@ static void tst1() { check_failure(now_tactic(), env, io, ctx, q); std::cout << "proof 2: " << orelse(fail_tactic(), t).solve(env, io, ctx, q).get_proof() << "\n"; -#if !defined(__APPLE__) +#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) check_failure(try_for(loop_tactic(), 100), env, io, ctx, q); std::cout << "proof 1: " << try_for(t, 10000).solve(env, io, s).get_proof() << "\n"; check_failure(try_for(orelse(try_for(loop_tactic(), 10000), trace_tactic(std::string("hello world"))), 100), env, io, ctx, q); - std::atomic flag1(false); + atomic flag1(false); check_failure(try_for(orelse(try_for(loop_tactic(), 10000), set_tactic(&flag1)), 100), @@ -83,10 +83,8 @@ static void tst1() { set_tactic(&flag1)), env, io, ctx, q); lean_assert(flag1); -#if !defined(LEAN_THREAD_UNSAFE) std::cout << "Before parallel 3 parallel tactics...\n"; std::cout << "proof 2: " << par(loop_tactic(), par(loop_tactic(), t)).solve(env, io, ctx, q).get_proof() << "\n"; -#endif #endif std::cout << "Before hello1 and 2...\n"; std::cout << "proof 2: " << orelse(then(repeat_at_most(append(trace_tactic("hello1"), trace_tactic("hello2")), 5), fail_tactic()), diff --git a/src/tests/util/lazy_list.cpp b/src/tests/util/lazy_list.cpp index a2b741bae..5367bdb9d 100644 --- a/src/tests/util/lazy_list.cpp +++ b/src/tests/util/lazy_list.cpp @@ -94,7 +94,7 @@ static void tst1() { display(orelse(lazy_list(), take(10, seq(100)))); display(orelse(take(0, seq(1)), take(10, seq(100)))); display(orelse(filter(take(100, seq(1)), [](int i) { return i < 0; }), take(10, seq(1000)))); -#if !defined(__APPLE__) && !defined(LEAN_THREAD_UNSAFE) +#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) display(timeout(append(append(take(10, seq(1)), loop()), seq(100)), 5)); display(take(10, par(seq(1), loop()))); #endif diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index c37ec02cd..bd7933028 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -5,18 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include #include -#include #include -#include +#include "util/thread.h" #include "util/debug.h" #include "util/shared_mutex.h" #include "util/interrupt.h" using namespace lean; +#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) void foo() { - static thread_local std::vector v(1024); + static LEAN_THREAD_LOCAL std::vector v(1024); if (v.size() != 1024) { std::cerr << "Error\n"; exit(1); @@ -26,7 +25,7 @@ void foo() { static void tst1() { unsigned n = 5; for (unsigned i = 0; i < n; i++) { - std::thread t([](){ foo(); }); + thread t([](){ foo(); }); t.join(); } } @@ -34,19 +33,19 @@ static void tst1() { static void tst2() { unsigned N = 10; unsigned n = 1; - lean::shared_mutex mut; - std::vector threads; + shared_mutex mut; + std::vector threads; for (unsigned i = 0; i < N; i++) { threads.emplace_back([&]() { unsigned sum = 0; { - lean::shared_lock lock(mut); + shared_lock lock(mut); for (unsigned i = 0; i < 1000000; i++) sum += n; } { - lean::unique_lock lock(mut); - std::cout << sum << "\n"; + exclusive_lock lock(mut); + std::cout << sum << "\n"; } }); } @@ -54,19 +53,18 @@ static void tst2() { threads[i].join(); } -#if !defined(__APPLE__) && !defined(LEAN_THREAD_UNSAFE) static void tst3() { shared_mutex mutex; - std::atomic t2_started(false); - std::atomic t2_done(false); + atomic t2_started(false); + atomic t2_done(false); std::chrono::milliseconds small_delay(10); - std::thread t1([&]() { + thread t1([&]() { while (!t2_started) { - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } while (!mutex.try_lock()) { - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } // test recursive try_lock lean_verify(mutex.try_lock()); @@ -76,11 +74,11 @@ static void tst3() { mutex.unlock(); }); - std::thread t2([&]() { + thread t2([&]() { { - unique_lock lock(mutex); + exclusive_lock lock(mutex); t2_started = true; - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } t2_done = true; }); @@ -92,16 +90,16 @@ static void tst3() { static void tst4() { shared_mutex mutex; - std::atomic t2_started(false); - std::atomic t2_done(false); + atomic t2_started(false); + atomic t2_done(false); std::chrono::milliseconds small_delay(10); - std::thread t1([&]() { + thread t1([&]() { while (!t2_started) { - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } while (!mutex.try_lock_shared()) { - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } // test recursive try_lock_shared lean_verify(mutex.try_lock_shared()); @@ -111,11 +109,11 @@ static void tst4() { mutex.unlock_shared(); }); - std::thread t2([&]() { + thread t2([&]() { { - unique_lock lock(mutex); + exclusive_lock lock(mutex); t2_started = true; - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } t2_done = true; }); @@ -126,31 +124,31 @@ static void tst4() { } static void tst5() { - shared_mutex mutex; - std::atomic t2_started(false); - std::atomic t1_done(false); + shared_mutex mutex; + atomic t2_started(false); + atomic t1_done(false); std::chrono::milliseconds small_delay(10); - std::thread t1([&]() { + thread t1([&]() { while (!t2_started) { - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } lean_verify(mutex.try_lock_shared()); // t2 is also using a shared lock - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); lean_verify(mutex.try_lock_shared()); - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); t1_done = true; mutex.unlock_shared(); - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); mutex.unlock_shared(); }); - std::thread t2([&]() { + thread t2([&]() { { shared_lock lock(mutex); t2_started = true; while (!t1_done) { - std::this_thread::sleep_for(small_delay); + this_thread::sleep_for(small_delay); } } }); @@ -162,8 +160,8 @@ static void tst5() { static void tst6() { interruptible_thread t1([]() { try { - // Remark: std::this_thread::sleep_for does not check whether the thread has been interrupted or not. - // std::this_thread::sleep_for(std::chrono::milliseconds(1000000)); + // Remark: this_thread::sleep_for does not check whether the thread has been interrupted or not. + // this_thread::sleep_for(std::chrono::milliseconds(1000000)); sleep_for(1000000); } catch (interrupted &) { std::cout << "interrupted...\n"; @@ -174,6 +172,8 @@ static void tst6() { t1.join(); } #else +static void tst1() {} +static void tst2() {} static void tst3() {} static void tst4() {} static void tst5() {} diff --git a/src/util/exception.cpp b/src/util/exception.cpp index 10d738051..020e74c05 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "util/exception.h" #include "util/sstream.h" +#include "util/thread.h" namespace lean { exception::exception(char const * msg):m_msg(msg) {} @@ -22,7 +23,7 @@ parser_exception::parser_exception(sstream const & msg, unsigned l, unsigned p): parser_exception::~parser_exception() noexcept {} char const * parser_exception::what() const noexcept { try { - static thread_local std::string buffer; + static LEAN_THREAD_LOCAL std::string buffer; std::ostringstream s; s << "(line: " << m_line << ", pos: " << m_pos << ") " << m_msg; buffer = s.str(); @@ -34,7 +35,7 @@ char const * parser_exception::what() const noexcept { } char const * stack_space_exception::what() const noexcept { - static thread_local std::string buffer; + static LEAN_THREAD_LOCAL std::string buffer; std::ostringstream s; s << "deep recursion was detected at '" << m_component_name << "' (potential solution: increase stack space in your system)"; buffer = s.str(); diff --git a/src/util/interrupt.cpp b/src/util/interrupt.cpp index 96d2be14f..d21b8329e 100644 --- a/src/util/interrupt.cpp +++ b/src/util/interrupt.cpp @@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/interrupt.h" #include "util/exception.h" namespace lean { -static thread_local std::atomic_bool g_interrupt; +static LEAN_THREAD_LOCAL atomic_bool g_interrupt; void request_interrupt() { g_interrupt.store(true); @@ -36,19 +37,19 @@ void sleep_for(unsigned ms, unsigned step_ms) { std::chrono::milliseconds c(step_ms); std::chrono::milliseconds r(ms % step_ms); for (unsigned i = 0; i < rounds; i++) { - std::this_thread::sleep_for(c); + this_thread::sleep_for(c); check_interrupted(); } - std::this_thread::sleep_for(r); + this_thread::sleep_for(r); check_interrupted(); } -std::atomic_bool * interruptible_thread::get_flag_addr() { +atomic_bool * interruptible_thread::get_flag_addr() { return &g_interrupt; } bool interruptible_thread::interrupted() const { - std::atomic_bool * f = m_flag_addr.load(); + atomic_bool * f = m_flag_addr.load(); if (f == nullptr) return false; return f->load(); @@ -56,12 +57,12 @@ bool interruptible_thread::interrupted() const { void interruptible_thread::request_interrupt(unsigned try_ms) { while (true) { - std::atomic_bool * f = m_flag_addr.load(); + atomic_bool * f = m_flag_addr.load(); if (f != nullptr) { f->store(true); return; } - std::this_thread::sleep_for(std::chrono::milliseconds(try_ms)); + this_thread::sleep_for(std::chrono::milliseconds(try_ms)); check_interrupted(); } } diff --git a/src/util/interrupt.h b/src/util/interrupt.h index 3c88932f0..9cbdb4b59 100644 --- a/src/util/interrupt.h +++ b/src/util/interrupt.h @@ -5,9 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include -#include #include +#include "util/thread.h" #include "util/stackinfo.h" #include "util/exception.h" @@ -46,7 +45,7 @@ void sleep_for(unsigned ms, unsigned step_ms = g_small_sleep); \brief Thread that provides a method for setting its interrupt flag. */ class interruptible_thread { - std::atomic m_flag_addr; + atomic m_flag_addr; /* The following auxiliary field is used to workaround a nasty bug that occurs in some platforms. On cygwin, it seems that the @@ -62,9 +61,9 @@ class interruptible_thread { m_dummy_addr before terminating the execution of the child thread. */ - std::atomic_bool m_dummy_addr; - std::thread m_thread; - static std::atomic_bool * get_flag_addr(); + atomic_bool m_dummy_addr; + thread m_thread; + static atomic_bool * get_flag_addr(); public: template interruptible_thread(Function && fun, Args &&... args): @@ -98,7 +97,7 @@ public: bool joinable(); }; -#ifdef LEAN_THREAD_UNSAFE +#if !defined(LEAN_MULTI_THREAD) inline void check_threadsafe() { throw exception("Lean was compiled without support for multi-threading"); } diff --git a/src/util/interruptable_ptr.h b/src/util/interruptable_ptr.h index c37c6843f..18696eb56 100644 --- a/src/util/interruptable_ptr.h +++ b/src/util/interruptable_ptr.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include "util/thread.h" namespace lean { /** @@ -23,20 +23,20 @@ namespace lean { */ template class interruptable_ptr { - T * m_ptr; - std::mutex m_mutex; + T * m_ptr; + mutex m_mutex; public: interruptable_ptr():m_ptr(nullptr) {} T * set(T * ptr) { - std::lock_guard lock(m_mutex); + lock_guard lock(m_mutex); T * old = m_ptr; m_ptr = ptr; return old; } void set_interrupt(bool flag) { - std::lock_guard lock(m_mutex); + lock_guard lock(m_mutex); if (m_ptr) m_ptr->set_interrupt(flag); } diff --git a/src/util/interval/interval.cpp b/src/util/interval/interval.cpp index a2a267108..19694cae4 100644 --- a/src/util/interval/interval.cpp +++ b/src/util/interval/interval.cpp @@ -280,8 +280,8 @@ template interval & interval::sub(interval const & o, interval_deps & deps) { if (compute_intv) { using std::swap; - static thread_local T new_l_val; - static thread_local T new_u_val; + static LEAN_THREAD_LOCAL T new_l_val; + static LEAN_THREAD_LOCAL T new_u_val; xnumeral_kind new_l_kind, new_u_kind; lean_trace("numerics", tout << "this: " << *this << " o: " << o << "\n";); round_to_minus_inf(); @@ -342,8 +342,8 @@ interval & interval::mul(interval const & o, interval_deps & deps) { bool c_o = i2.is_lower_open(); bool d_o = i2.is_upper_open(); - static thread_local T new_l_val; - static thread_local T new_u_val; + static LEAN_THREAD_LOCAL T new_l_val; + static LEAN_THREAD_LOCAL T new_u_val; xnumeral_kind new_l_kind, new_u_kind; if (i1.is_N()) { @@ -422,10 +422,10 @@ interval & interval::mul(interval const & o, interval_deps & deps) { deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; } } else if (i2.is_M()) { - static thread_local T ad; static thread_local xnumeral_kind ad_k; - static thread_local T bc; static thread_local xnumeral_kind bc_k; - static thread_local T ac; static thread_local xnumeral_kind ac_k; - static thread_local T bd; static thread_local xnumeral_kind bd_k; + static LEAN_THREAD_LOCAL T ad; static LEAN_THREAD_LOCAL xnumeral_kind ad_k; + static LEAN_THREAD_LOCAL T bc; static LEAN_THREAD_LOCAL xnumeral_kind bc_k; + static LEAN_THREAD_LOCAL T ac; static LEAN_THREAD_LOCAL xnumeral_kind ac_k; + static LEAN_THREAD_LOCAL T bd; static LEAN_THREAD_LOCAL xnumeral_kind bd_k; bool ad_o = a_o || d_o; bool bc_o = b_o || c_o; @@ -586,8 +586,8 @@ interval & interval::div(interval const & o, interval_deps & deps) { bool c_o = i2.m_lower_open; bool d_o = i2.m_upper_open; - static thread_local T new_l_val; - static thread_local T new_u_val; + static LEAN_THREAD_LOCAL T new_l_val; + static LEAN_THREAD_LOCAL T new_u_val; xnumeral_kind new_l_kind, new_u_kind; if (i1.is_N()) { @@ -795,7 +795,7 @@ interval & interval::operator-=(T const & o) { template interval & interval::operator*=(T const & o) { xnumeral_kind new_l_kind, new_u_kind; - static thread_local T tmp1; + static LEAN_THREAD_LOCAL T tmp1; if (this->is_zero()) { return *this; } @@ -831,7 +831,7 @@ interval & interval::operator*=(T const & o) { template interval & interval::operator/=(T const & o) { xnumeral_kind new_l_kind, new_u_kind; - static thread_local T tmp1; + static LEAN_THREAD_LOCAL T tmp1; if (this->is_zero()) { return *this; } @@ -872,8 +872,8 @@ void interval::inv(interval_deps & deps) { using std::swap; - static thread_local T new_l_val; - static thread_local T new_u_val; + static LEAN_THREAD_LOCAL T new_l_val; + static LEAN_THREAD_LOCAL T new_u_val; xnumeral_kind new_l_kind, new_u_kind; if (is_P1()) { @@ -1032,8 +1032,8 @@ void interval::power(unsigned n, interval_deps & deps) { // we need both bounds to justify upper bound xnumeral_kind un1_kind = lower_kind(); xnumeral_kind un2_kind = upper_kind(); - static thread_local T un1; - static thread_local T un2; + static LEAN_THREAD_LOCAL T un1; + static LEAN_THREAD_LOCAL T un2; if (compute_intv) { swap(un1, m_lower); swap(un2, m_upper); @@ -1106,7 +1106,7 @@ T a_div_x_n(T a, T const & x, unsigned n, bool to_plus_inf) { numeric_traits::set_rounding(to_plus_inf); a /= x; } else { - static thread_local T tmp; + static LEAN_THREAD_LOCAL T tmp; numeric_traits::set_rounding(!to_plus_inf); tmp = x; numeric_traits::power(tmp, n); @@ -1141,7 +1141,7 @@ void interval::display(std::ostream & out) const { template void interval::fmod(interval y) { T const & yb = numeric_traits::is_neg(m_lower) ? y.m_lower : y.m_upper; - static thread_local T n; + static LEAN_THREAD_LOCAL T n; numeric_traits::set_rounding(false); n = m_lower / yb; numeric_traits::floor(n); @@ -1149,7 +1149,7 @@ template void interval::fmod(interval y) { } template void interval::fmod(T y) { - static thread_local T n; + static LEAN_THREAD_LOCAL T n; numeric_traits::set_rounding(false); n = m_lower / y; numeric_traits::floor(n); @@ -1781,8 +1781,8 @@ void interval::tan(interval_deps & deps) { template template void interval::csc (interval_deps & deps) { - static thread_local T l; - static thread_local T u; + static LEAN_THREAD_LOCAL T l; + static LEAN_THREAD_LOCAL T u; if (compute_intv) { l = m_lower; u = m_upper; @@ -1975,8 +1975,8 @@ void interval::sec (interval_deps & deps) { template template void interval::cot (interval_deps & deps) { - static thread_local T l; - static thread_local T u; + static LEAN_THREAD_LOCAL T l; + static LEAN_THREAD_LOCAL T u; if (compute_intv) { l = m_lower; u = m_upper; diff --git a/src/util/interval/interval_instances.cpp b/src/util/interval/interval_instances.cpp index a4027ff0a..0c8f6ecff 100644 --- a/src/util/interval/interval_instances.cpp +++ b/src/util/interval/interval_instances.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/thread.h" #include "util/numerics/mpq.h" #include "util/numerics/double.h" #include "util/numerics/float.h" diff --git a/src/util/lazy_list_fn.h b/src/util/lazy_list_fn.h index 3a74d496d..0236d7e88 100644 --- a/src/util/lazy_list_fn.h +++ b/src/util/lazy_list_fn.h @@ -219,13 +219,19 @@ lazy_list repeat_at_most(T const & v, F && f, unsigned k, char const * cname \remark \c check_ms is how often the main thread checks whether the child thread finished. */ +#if !defined(LEAN_MULTI_THREAD) +template +lazy_list timeout(lazy_list const & l, unsigned, unsigned) { + return l; +} +#else template lazy_list timeout(lazy_list const & l, unsigned ms, unsigned check_ms = g_small_sleep) { if (check_ms == 0) check_ms = 1; return mk_lazy_list([=]() { typename lazy_list::maybe_pair r; - std::atomic done(false); + atomic done(false); interruptible_thread th([&]() { try { r = l.pull(); @@ -243,7 +249,7 @@ lazy_list timeout(lazy_list const & l, unsigned ms, unsigned check_ms = g_ if (std::chrono::duration_cast(curr - start) > d) break; check_interrupted(); - std::this_thread::sleep_for(small); + this_thread::sleep_for(small); } th.request_interrupt(); th.join(); @@ -258,13 +264,14 @@ lazy_list timeout(lazy_list const & l, unsigned ms, unsigned check_ms = g_ } }); } +#endif /** \brief Similar to interleave, but the heads are computed in parallel. Moreover, when pulling results from the lists, if one finishes before the other, then the other one is interrupted. */ -#ifdef LEAN_THREAD_UNSAFE +#if !defined(LEAN_MULTI_THREAD) template lazy_list par(lazy_list const & l1, lazy_list const & l2, unsigned = g_small_sleep) { return interleave(l1, l2); @@ -275,8 +282,8 @@ lazy_list par(lazy_list const & l1, lazy_list const & l2, unsigned chec return mk_lazy_list([=]() { typename lazy_list::maybe_pair r1; typename lazy_list::maybe_pair r2; - std::atomic done1(false); - std::atomic done2(false); + atomic done1(false); + atomic done2(false); interruptible_thread th1([&]() { try { r1 = l1.pull(); @@ -297,7 +304,7 @@ lazy_list par(lazy_list const & l1, lazy_list const & l2, unsigned chec std::chrono::milliseconds small(check_ms); while (!done1 && !done2) { check_interrupted(); - std::this_thread::sleep_for(small); + this_thread::sleep_for(small); } th1.request_interrupt(); th2.request_interrupt(); diff --git a/src/util/memory.cpp b/src/util/memory.cpp index 51cc802f9..1376c6a28 100644 --- a/src/util/memory.cpp +++ b/src/util/memory.cpp @@ -40,7 +40,7 @@ void free(void * ptr) { } #else -#include +#include "util/thread.h" #if defined(HAS_MALLOC_USABLE_SIZE) #include // NOLINT @@ -96,11 +96,7 @@ inline void free_core(void * ptr) { ::free(static_cast( namespace lean { class alloc_info { -#ifdef LEAN_THREAD_UNSAFE - size_t m_size; -#else - std::atomic m_size; -#endif + atomic m_size; public: alloc_info():m_size(0) {} ~alloc_info() {} @@ -118,8 +114,8 @@ public: long long size() const { return static_cast(m_size); } }; -static alloc_info g_global_memory; -static thread_local thread_alloc_info g_thread_memory; +static alloc_info g_global_memory; +static LEAN_THREAD_LOCAL thread_alloc_info g_thread_memory; size_t get_allocated_memory() { return g_global_memory.size(); } long long get_thread_allocated_memory() { return g_thread_memory.size(); } diff --git a/src/util/name.cpp b/src/util/name.cpp index a6b4db67c..116e49c1a 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include #include #include -#include +#include "util/thread.h" #include "util/name.h" #include "util/sstream.h" #include "util/debug.h" @@ -156,11 +156,7 @@ name const & name::anonymous() { return g_anonymous; } -#ifdef LEAN_THREAD_UNSAFE -static unsigned g_next_id(0); -#else -static std::atomic g_next_id(0); -#endif +static atomic g_next_id(0); name name::mk_internal_unique_name() { unsigned id = g_next_id++; diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp index 9c296be3d..ec52abd6f 100644 --- a/src/util/numerics/double.cpp +++ b/src/util/numerics/double.cpp @@ -5,12 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ #include +#include "util/thread.h" #include "util/numerics/numeric_traits.h" #include "util/numerics/double.h" namespace lean { -static thread_local mpfr_rnd_t g_rnd; +static LEAN_THREAD_LOCAL mpfr_rnd_t g_rnd; void set_double_rnd(bool plus_inf) { g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; } diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h index 727069584..d37fae57a 100644 --- a/src/util/numerics/double.h +++ b/src/util/numerics/double.h @@ -20,10 +20,10 @@ void double_ceil(double & v); void double_floor(double & v); // Macro to implement transcendental functions using MPFR -#define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd) \ - static thread_local mpfp t(53); \ - t = v; \ - t.f(rnd); \ +#define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd) \ + static LEAN_THREAD_LOCAL mpfp t(53); \ + t = v; \ + t.f(rnd); \ v = t.get_double(rnd); void set_double_rnd(bool plus_inf); diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp index 87ec243c8..b4ae1cb89 100644 --- a/src/util/numerics/float.cpp +++ b/src/util/numerics/float.cpp @@ -5,12 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ #include +#include "util/thread.h" #include "util/numerics/numeric_traits.h" #include "util/numerics/float.h" namespace lean { -static thread_local mpfr_rnd_t g_rnd; +static LEAN_THREAD_LOCAL mpfr_rnd_t g_rnd; void set_float_rnd(bool plus_inf) { g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; } diff --git a/src/util/numerics/float.h b/src/util/numerics/float.h index a5c86216a..a2c16d49f 100644 --- a/src/util/numerics/float.h +++ b/src/util/numerics/float.h @@ -21,7 +21,7 @@ void float_floor(float & v); // Macro to implement transcendental functions using MPFR #define LEAN_TRANS_FLOAT_FUNC(f, v, rnd) \ - static thread_local mpfp t(24); \ + static LEAN_THREAD_LOCAL mpfp t(24); \ t = v; \ t.f(rnd); \ v = t.get_float(rnd); diff --git a/src/util/numerics/mpbq.cpp b/src/util/numerics/mpbq.cpp index dbbdd01f1..4265d0007 100644 --- a/src/util/numerics/mpbq.cpp +++ b/src/util/numerics/mpbq.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/thread.h" #include "util/numerics/mpbq.h" namespace lean { @@ -15,7 +16,7 @@ bool set(mpbq & a, mpq const & b) { a.m_k = 0; return true; } else { - static thread_local mpz d; + static LEAN_THREAD_LOCAL mpz d; denominator(d, b); unsigned shift; if (d.is_power_of_two(shift)) { @@ -46,7 +47,7 @@ void mpbq::normalize() { } int cmp(mpbq const & a, mpbq const & b) { - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; if (a.m_k == b.m_k) { return cmp(a.m_num, b.m_num); } else if (a.m_k < b.m_k) { @@ -60,7 +61,7 @@ int cmp(mpbq const & a, mpbq const & b) { } int cmp(mpbq const & a, mpz const & b) { - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; if (a.m_k == 0) { return cmp(a.m_num, b); } else { @@ -73,8 +74,8 @@ int cmp(mpbq const & a, mpq const & b) { if (a.is_integer() && b.is_integer()) { return -cmp(b, a.m_num); } else { - static thread_local mpz tmp1; - static thread_local mpz tmp2; + static LEAN_THREAD_LOCAL mpz tmp1; + static LEAN_THREAD_LOCAL mpz tmp2; // tmp1 <- numerator(a)*denominator(b) denominator(tmp1, b); tmp1 *= a.m_num; // tmp2 <- numerator(b)*denominator(a) @@ -92,7 +93,7 @@ mpbq & mpbq::operator+=(mpbq const & a) { m_num += a.m_num; } else { lean_assert(m_k > a.m_k); - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; mul2k(tmp, a.m_num, m_k - a.m_k); m_num += tmp; } @@ -106,7 +107,7 @@ mpbq & mpbq::add_int(T const & a) { m_num += a; } else { lean_assert(m_k > 0); - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; tmp = a; mul2k(tmp, tmp, m_k); m_num += tmp; @@ -126,7 +127,7 @@ mpbq & mpbq::operator-=(mpbq const & a) { m_num -= a.m_num; } else { lean_assert(m_k > a.m_k); - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; mul2k(tmp, a.m_num, m_k - a.m_k); m_num -= tmp; } @@ -140,7 +141,7 @@ mpbq & mpbq::sub_int(T const & a) { m_num -= a; } else { lean_assert(m_k > 0); - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; tmp = a; mul2k(tmp, tmp, m_k); m_num -= tmp; @@ -302,7 +303,7 @@ bool lt_1div2k(mpbq const & a, unsigned k) { return false; } else { lean_assert(a.m_k > k); - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; tmp = 1; mul2k(tmp, tmp, a.m_k - k); return a.m_num < tmp; diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h index 50ffd9be4..babc903cf 100644 --- a/src/util/numerics/mpbq.h +++ b/src/util/numerics/mpbq.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/thread.h" #include "util/bit_tricks.h" #include "util/numerics/mpz.h" #include "util/numerics/mpq.h" @@ -268,7 +269,7 @@ public: template<> class numeric_traits { private: - static thread_local bool rnd; + static LEAN_THREAD_LOCAL bool rnd; public: static bool precise() { return true; } static bool is_zero(mpbq const & v) { return v.is_zero(); } diff --git a/src/util/numerics/mpfp.cpp b/src/util/numerics/mpfp.cpp index 3b8d7aedb..be76a5338 100644 --- a/src/util/numerics/mpfp.cpp +++ b/src/util/numerics/mpfp.cpp @@ -7,10 +7,11 @@ Author: Soonho Kong #include #include #include +#include "util/thread.h" #include "util/numerics/mpfp.h" namespace lean { -static thread_local mpfr_rnd_t g_mpfp_rnd = MPFR_RNDN; +static LEAN_THREAD_LOCAL mpfr_rnd_t g_mpfp_rnd = MPFR_RNDN; mpfp numeric_traits::pi_l; mpfp numeric_traits::pi_n; diff --git a/src/util/numerics/mpfp.h b/src/util/numerics/mpfp.h index c4fb51481..7b9ec087e 100644 --- a/src/util/numerics/mpfp.h +++ b/src/util/numerics/mpfp.h @@ -458,21 +458,21 @@ public: void rround(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_round(m_val, m_val, rnd); } void rtrunc(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_trunc(m_val, m_val, rnd); } - friend mpfp floor(mpfp const & a) { static thread_local mpfp tmp; tmp = a; tmp.floor(); return tmp; } - friend mpfp ceil (mpfp const & a) { static thread_local mpfp tmp; tmp = a; tmp.ceil(); return tmp; } - friend mpfp round(mpfp const & a) { static thread_local mpfp tmp; tmp = a; tmp.round(); return tmp; } - friend mpfp trunc(mpfp const & a) { static thread_local mpfp tmp; tmp = a; tmp.trunc(); return tmp; } + friend mpfp floor(mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.floor(); return tmp; } + friend mpfp ceil (mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.ceil(); return tmp; } + friend mpfp round(mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.round(); return tmp; } + friend mpfp trunc(mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.trunc(); return tmp; } friend mpfp rfloor(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static thread_local mpfp tmp; tmp = a; tmp.rfloor(rnd); return tmp; + static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rfloor(rnd); return tmp; } friend mpfp rceil (mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static thread_local mpfp tmp; tmp = a; tmp.rceil(rnd); return tmp; + static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rceil(rnd); return tmp; } friend mpfp rround(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static thread_local mpfp tmp; tmp = a; tmp.rround(rnd); return tmp; + static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rround(rnd); return tmp; } friend mpfp rtrunc(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static thread_local mpfp tmp; tmp = a; tmp.rtrunc(rnd); return tmp; + static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rtrunc(rnd); return tmp; } void power(mpfp const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow(m_val, m_val, b.m_val, rnd); } diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index ed202d1d6..f4e5cf2dc 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sstream.h" +#include "util/thread.h" #include "util/numerics/mpq.h" #include "util/numerics/mpbq.h" @@ -26,7 +27,7 @@ int cmp(mpq const & a, mpz const & b) { if (a.is_integer()) { return mpz_cmp(mpq_numref(a.m_val), mpq::zval(b)); } else { - static thread_local mpz tmp; + static LEAN_THREAD_LOCAL mpz tmp; mpz_mul(mpq::zval(tmp), mpq_denref(a.m_val), mpq::zval(b)); return mpz_cmp(mpq_numref(a.m_val), mpq::zval(tmp)); } @@ -128,7 +129,7 @@ DECL_UDATA(mpq) template static mpq const & to_mpq(lua_State * L) { - static thread_local mpq arg; + static LEAN_THREAD_LOCAL mpq arg; switch (lua_type(L, idx)) { case LUA_TNUMBER: arg = lua_tonumber(L, idx); return arg; case LUA_TSTRING: arg = mpq(lua_tostring(L, idx)); return arg; diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp index c37668c32..5b62ce773 100644 --- a/src/util/numerics/mpz.cpp +++ b/src/util/numerics/mpz.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" +#include "util/thread.h" #include "util/numerics/mpz.h" namespace lean { @@ -53,7 +54,7 @@ mpz operator%(mpz const & a, mpz const & b) { } bool root(mpz & root, mpz const & a, unsigned k) { - static thread_local mpz rem; + static LEAN_THREAD_LOCAL mpz rem; mpz_rootrem(root.m_val, rem.m_val, a.m_val, k); return rem.is_zero(); } @@ -87,7 +88,7 @@ DECL_UDATA(mpz) template static mpz const & to_mpz(lua_State * L) { - static thread_local mpz arg; + static LEAN_THREAD_LOCAL mpz arg; switch (lua_type(L, idx)) { case LUA_TNUMBER: arg = static_cast(lua_tointeger(L, idx)); return arg; case LUA_TSTRING: arg = mpz(lua_tostring(L, idx)); return arg; diff --git a/src/util/numerics/primes.cpp b/src/util/numerics/primes.cpp index 63be3ff50..3f5d67aca 100644 --- a/src/util/numerics/primes.cpp +++ b/src/util/numerics/primes.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include +#include "util/thread.h" #include "util/int64.h" #include "util/debug.h" #include "util/exception.h" @@ -91,7 +91,7 @@ public: }; static prime_generator g_prime_generator; -static std::mutex g_prime_generator_mutex; +static mutex g_prime_generator_mutex; prime_iterator::prime_iterator(): @@ -102,7 +102,7 @@ uint64 prime_iterator::next() { unsigned idx = m_idx; m_idx++; { - std::lock_guard guard(g_prime_generator_mutex); + lock_guard guard(g_prime_generator_mutex); return g_prime_generator(idx); } } diff --git a/src/util/rc.h b/src/util/rc.h index 3fe823adc..608ddb309 100644 --- a/src/util/rc.h +++ b/src/util/rc.h @@ -7,28 +7,18 @@ Author: Leonardo de Moura #pragma once // Goodies for reference counting -#ifdef LEAN_THREAD_UNSAFE -#define MK_LEAN_RC() \ -private: \ -unsigned m_rc; \ -public: \ -unsigned get_rc() const { return m_rc; } \ -void inc_ref() { m_rc++; } \ -bool dec_ref_core() { lean_assert(get_rc() > 0); m_rc--; return m_rc == 0; } \ -void dec_ref() { if (dec_ref_core()) dealloc(); } -#else -#include -#define MK_LEAN_RC() \ -private: \ -std::atomic m_rc; \ -public: \ -unsigned get_rc() const { return std::atomic_load(&m_rc); } \ -void inc_ref() { std::atomic_fetch_add_explicit(&m_rc, 1u, std::memory_order_relaxed); } \ -bool dec_ref_core() { lean_assert(get_rc() > 0); return std::atomic_fetch_sub_explicit(&m_rc, 1u, std::memory_order_relaxed) == 1u; } \ -void dec_ref() { if (dec_ref_core()) dealloc(); } -#endif +#include "util/thread.h" #include "util/debug.h" +#define MK_LEAN_RC() \ +private: \ +atomic m_rc; \ +public: \ +unsigned get_rc() const { return atomic_load(&m_rc); } \ +void inc_ref() { atomic_fetch_add_explicit(&m_rc, 1u, memory_order_relaxed); } \ +bool dec_ref_core() { lean_assert(get_rc() > 0); return atomic_fetch_sub_explicit(&m_rc, 1u, memory_order_relaxed) == 1u; } \ +void dec_ref() { if (dec_ref_core()) dealloc(); } + #define LEAN_COPY_REF(T, Arg) \ if (Arg.m_ptr) \ Arg.m_ptr->inc_ref(); \ diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp index 432a02eba..150a2e35c 100644 --- a/src/util/script_state.cpp +++ b/src/util/script_state.cpp @@ -5,12 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include -#include #include #include #include -#include +#include "util/thread.h" #include "util/lua.h" #include "util/debug.h" #include "util/exception.h" @@ -48,7 +46,7 @@ static char g_weak_ptr_key; // key for Lua registry (used at get_weak_ptr and sa struct script_state::imp { lua_State * m_state; - std::mutex m_mutex; + mutex m_mutex; static std::weak_ptr * get_weak_ptr(lua_State * L) { lua_pushlightuserdata(L, static_cast(&g_weak_ptr_key)); @@ -110,12 +108,12 @@ struct script_state::imp { } void dofile(char const * fname) { - std::lock_guard lock(m_mutex); + lock_guard lock(m_mutex); ::lean::dofile(m_state, fname); } void dostring(char const * str) { - std::lock_guard lock(m_mutex); + lock_guard lock(m_mutex); ::lean::dostring(m_state, str); } }; @@ -146,7 +144,7 @@ void script_state::dostring(char const * str) { m_ptr->dostring(str); } -std::mutex & script_state::get_mutex() { +mutex & script_state::get_mutex() { return m_ptr->m_mutex; } @@ -308,7 +306,7 @@ static void open_state(lua_State * L) { #define SMALL_DELAY 10 // in ms std::chrono::milliseconds g_small_delay(SMALL_DELAY); -#if !defined(LEAN_THREAD_UNSAFE) +#if defined(LEAN_MULTI_THREAD) /** \brief Channel for communicating with thread objects in the Lua API */ @@ -316,10 +314,10 @@ class data_channel { // We use a lua_State to implement the channel. This is quite hackish, // but it is a convenient storage for Lua objects sent from one state to // another. - script_state m_channel; - int m_ini; - std::mutex m_mutex; - std::condition_variable m_cv; + script_state m_channel; + int m_ini; + mutex m_mutex; + condition_variable m_cv; public: data_channel() { lua_State * channel = m_channel.m_ptr->m_state; @@ -335,7 +333,7 @@ public: // on m_channel. if (last < first) return; - std::lock_guard lock(m_mutex); + lock_guard lock(m_mutex); lua_State * channel = m_channel.m_ptr->m_state; bool was_empty = lua_gettop(channel) == m_ini; copy_values(src, first, last, channel); @@ -348,7 +346,7 @@ public: the execution of \c tgt if the channel is empty. */ int read(lua_State * tgt, int i) { - std::unique_lock lock(m_mutex); + unique_lock lock(m_mutex); lua_State * channel = m_channel.m_ptr->m_state; if (i > 0) { // i is the position of the timeout argument @@ -383,10 +381,10 @@ public: */ class data_channel_ref { std::unique_ptr m_channel; - std::mutex m_mutex; + mutex m_mutex; public: data_channel & get() { - std::lock_guard lock(m_mutex); + lock_guard lock(m_mutex); if (!m_channel) m_channel.reset(new data_channel()); lean_assert(m_channel); @@ -410,8 +408,8 @@ class leanlua_thread { script_state m_state; int m_sz_before; std::unique_ptr m_exception; - std::atomic m_in_channel_addr; - std::atomic m_out_channel_addr; + atomic m_in_channel_addr; + atomic m_out_channel_addr; interruptible_thread m_thread; public: leanlua_thread(script_state const & st, int sz_before, int num_args): @@ -460,7 +458,7 @@ public: void write(lua_State * src, int first, int last) { while (!m_in_channel_addr) { check_interrupted(); - std::this_thread::sleep_for(g_small_delay); + this_thread::sleep_for(g_small_delay); } data_channel & in = m_in_channel_addr.load()->get(); in.write(src, first, last); @@ -469,7 +467,7 @@ public: int read(lua_State * src) { if (!m_out_channel_addr) { check_interrupted(); - std::this_thread::sleep_for(g_small_delay); + this_thread::sleep_for(g_small_delay); } data_channel & out = m_out_channel_addr.load()->get(); int nargs = lua_gettop(src); @@ -588,7 +586,7 @@ static void open_interrupt(lua_State * L) { SET_GLOBAL_FUN(check_interrupted, "check_interrupted"); SET_GLOBAL_FUN(sleep, "sleep"); SET_GLOBAL_FUN(yield, "yield"); -#if !defined(LEAN_THREAD_UNSAFE) +#if defined(LEAN_MULTI_THREAD) SET_GLOBAL_FUN(channel_read, "read"); SET_GLOBAL_FUN(channel_write, "write"); #endif @@ -596,7 +594,7 @@ static void open_interrupt(lua_State * L) { void open_extra(lua_State * L) { open_state(L); -#if !defined(LEAN_THREAD_UNSAFE) +#if defined(LEAN_MULTI_THREAD) open_thread(L); #endif open_interrupt(L); diff --git a/src/util/script_state.h b/src/util/script_state.h index e755ac968..1896143ac 100644 --- a/src/util/script_state.h +++ b/src/util/script_state.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include -#include #include +#include "util/thread.h" #include "util/unlock_guard.h" namespace lean { @@ -20,7 +20,7 @@ public: private: std::shared_ptr m_ptr; friend script_state to_script_state(lua_State * L); - std::mutex & get_mutex(); + mutex & get_mutex(); lua_State * get_state(); friend class data_channel; public: @@ -50,7 +50,7 @@ public: */ template typename std::result_of::type apply(F && f) { - std::lock_guard lock(get_mutex()); + lock_guard lock(get_mutex()); return f(get_state()); } @@ -72,7 +72,7 @@ public: template void exec_protected(F && f) { - std::lock_guard lock(get_mutex()); + lock_guard lock(get_mutex()); f(); } }; diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 118d41191..3f71655be 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -120,7 +120,7 @@ format const & colon() { return g_colon; } format const & dot() { return g_dot; } // Auxiliary flag used to mark whether flatten // produce a different sexpr -static bool thread_local g_diff_flatten = false; +static bool LEAN_THREAD_LOCAL g_diff_flatten = false; // sexpr format::flatten(sexpr const & s) { lean_assert(is_cons(s)); diff --git a/src/util/shared_mutex.cpp b/src/util/shared_mutex.cpp index 8f8431e3f..2912e0c32 100644 --- a/src/util/shared_mutex.cpp +++ b/src/util/shared_mutex.cpp @@ -16,12 +16,12 @@ namespace lean { shared_mutex::shared_mutex():m_rw_counter(0), m_state(0) {} shared_mutex::~shared_mutex() { - std::lock_guard lock(m_mutex); + lock_guard lock(m_mutex); } void shared_mutex::lock() { - std::unique_lock lock(m_mutex); - if (m_rw_owner == std::this_thread::get_id()) { + unique_lock lock(m_mutex); + if (m_rw_owner == this_thread::get_id()) { m_rw_counter++; return; // already has the lock } @@ -31,20 +31,20 @@ void shared_mutex::lock() { while (m_state & readers) m_gate2.wait(lock); lean_assert(m_rw_counter == 0); - m_rw_owner = std::this_thread::get_id(); + m_rw_owner = this_thread::get_id(); m_rw_counter = 1; } bool shared_mutex::try_lock() { - std::unique_lock lock(m_mutex); - if (m_rw_owner == std::this_thread::get_id()) { + unique_lock lock(m_mutex); + if (m_rw_owner == this_thread::get_id()) { m_rw_counter++; return true; // already has the lock } if (m_state == 0) { m_state = write_entered; lean_assert(m_rw_counter == 0); - m_rw_owner = std::this_thread::get_id(); + m_rw_owner = this_thread::get_id(); m_rw_counter = 1; return true; } @@ -52,22 +52,22 @@ bool shared_mutex::try_lock() { } void shared_mutex::unlock() { - std::lock_guard lock(m_mutex); - lean_assert(m_rw_owner == std::this_thread::get_id()); + lock_guard lock(m_mutex); + lean_assert(m_rw_owner == this_thread::get_id()); lean_assert(m_rw_counter > 0); m_rw_counter--; if (m_rw_counter > 0) return; // keep the lock - m_rw_owner = std::thread::id(); // reset owner + m_rw_owner = thread::id(); // reset owner lean_assert(m_rw_counter == 0); - lean_assert(m_rw_owner != std::this_thread::get_id()); + lean_assert(m_rw_owner != this_thread::get_id()); m_state = 0; m_gate1.notify_all(); } void shared_mutex::lock_shared() { - std::unique_lock lock(m_mutex); - if (m_rw_owner == std::this_thread::get_id()) { + unique_lock lock(m_mutex); + if (m_rw_owner == this_thread::get_id()) { lean_assert(m_rw_counter > 0); m_rw_counter++; return; // already has the lock @@ -80,8 +80,8 @@ void shared_mutex::lock_shared() { } bool shared_mutex::try_lock_shared() { - std::unique_lock lock(m_mutex); - if (m_rw_owner == std::this_thread::get_id()) { + unique_lock lock(m_mutex); + if (m_rw_owner == this_thread::get_id()) { lean_assert(m_rw_counter > 0); m_rw_counter++; return true; // already has the lock @@ -97,8 +97,8 @@ bool shared_mutex::try_lock_shared() { } void shared_mutex::unlock_shared() { - std::lock_guard lock(m_mutex); - if (m_rw_owner == std::this_thread::get_id()) { + lock_guard lock(m_mutex); + if (m_rw_owner == this_thread::get_id()) { // if we have a rw (aka unshared) lock, then // the shared lock must be nested. lean_assert(m_rw_counter > 1); diff --git a/src/util/shared_mutex.h b/src/util/shared_mutex.h index d4bd0ef72..f91d3e01a 100644 --- a/src/util/shared_mutex.h +++ b/src/util/shared_mutex.h @@ -10,18 +10,16 @@ Hinnant. The proposal is also part of the Boost library which is licensed under http://www.boost.org/LICENSE_1_0.txt */ -#include -#include -#include #include +#include "util/thread.h" namespace lean { class shared_mutex { - std::mutex m_mutex; - std::thread::id m_rw_owner; + mutex m_mutex; + thread::id m_rw_owner; unsigned m_rw_counter; - std::condition_variable m_gate1; - std::condition_variable m_gate2; + condition_variable m_gate1; + condition_variable m_gate2; unsigned m_state; static constexpr unsigned write_entered = 1u << (sizeof(unsigned)*8 - 1); @@ -52,10 +50,10 @@ public: ~shared_lock() { m_mutex.unlock_shared(); } }; -class unique_lock { +class exclusive_lock { shared_mutex & m_mutex; public: - unique_lock(shared_mutex & m):m_mutex(m) { m_mutex.lock(); } - ~unique_lock() { m_mutex.unlock(); } + exclusive_lock(shared_mutex & m):m_mutex(m) { m_mutex.lock(); } + ~exclusive_lock() { m_mutex.unlock(); } }; } diff --git a/src/util/splay_tree.h b/src/util/splay_tree.h index b9d5feec0..630502ae7 100644 --- a/src/util/splay_tree.h +++ b/src/util/splay_tree.h @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "util/pair.h" #include "util/debug.h" #include "util/buffer.h" +#include "util/thread.h" namespace lean { /** @@ -223,7 +224,7 @@ class splay_tree : public CMP { } bool insert_pull(T const & v, bool is_insert) { - static thread_local std::vector path; + static LEAN_THREAD_LOCAL std::vector path; node * n = m_ptr; bool found = false; while (true) { @@ -271,7 +272,7 @@ class splay_tree : public CMP { void pull_max() { if (!m_ptr) return; - static thread_local std::vector path; + static LEAN_THREAD_LOCAL std::vector path; node * n = m_ptr; while (true) { lean_assert(n); diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp index a97aaac0c..618dcde80 100644 --- a/src/util/stackinfo.cpp +++ b/src/util/stackinfo.cpp @@ -7,8 +7,18 @@ Author: Leonardo de Moura #include #include #include +#include "util/thread.h" #include "util/exception.h" +#if defined(LEAN_WINDOWS) + // no extra included needed so far +#elif defined(__APPLE__) + #include // NOLINT +#else + #include // NOLINT + #include // NOLINT +#endif + #define LEAN_MIN_STACK_SPACE 128*1024 // 128 Kb namespace lean { @@ -16,12 +26,11 @@ void throw_get_stack_size_failed() { throw exception("failed to retrieve thread stack size"); } -#ifdef LEAN_WINDOWS +#if defined(LEAN_WINDOWS) size_t get_stack_size(int ) { return LEAN_WIN_STACK_SIZE; } #elif defined (__APPLE__) -#include size_t get_stack_size(int main) { if (main) { // Retrieve stack size of the main thread. @@ -31,6 +40,7 @@ size_t get_stack_size(int main) { } return curr.rlim_max; } else { + #if defined(LEAN_MULTI_THREAD) // This branch retrieves the default thread size for pthread threads. // This is *not* the stack size of the main thread. pthread_attr_t attr; @@ -41,29 +51,45 @@ size_t get_stack_size(int main) { throw_get_stack_size_failed(); } return result; + #else + return 0; + #endif } } #else -size_t get_stack_size(int ) { - pthread_attr_t attr; - memset (&attr, 0, sizeof(attr)); - if (pthread_getattr_np(pthread_self(), &attr) != 0) { - throw_get_stack_size_failed(); +size_t get_stack_size(int main) { + if (main) { + // Retrieve stack size of the main thread. + struct rlimit curr; + if (getrlimit(RLIMIT_STACK, &curr) != 0) { + throw_get_stack_size_failed(); + } + return curr.rlim_max; + } else { + #if defined(LEAN_MULTI_THREAD) + pthread_attr_t attr; + memset (&attr, 0, sizeof(attr)); + if (pthread_getattr_np(pthread_self(), &attr) != 0) { + throw_get_stack_size_failed(); + } + void * ptr; + size_t result; + if (pthread_attr_getstack (&attr, &ptr, &result) != 0) { + throw_get_stack_size_failed(); + } + if (pthread_attr_destroy(&attr) != 0) { + throw_get_stack_size_failed(); + } + return result; + #else + return 0; + #endif } - void * ptr; - size_t result; - if (pthread_attr_getstack (&attr, &ptr, &result) != 0) { - throw_get_stack_size_failed(); - } - if (pthread_attr_destroy(&attr) != 0) { - throw_get_stack_size_failed(); - } - return result; } #endif -static thread_local size_t g_stack_size; -static thread_local size_t g_stack_base; +static LEAN_THREAD_LOCAL size_t g_stack_size; +static LEAN_THREAD_LOCAL size_t g_stack_base; void save_stack_info(bool main) { g_stack_size = get_stack_size(main); diff --git a/src/util/stackinfo.h b/src/util/stackinfo.h index 6356ad1a4..72b59024b 100644 --- a/src/util/stackinfo.h +++ b/src/util/stackinfo.h @@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include + namespace lean { size_t get_stack_size(bool main); void save_stack_info(bool main = true); diff --git a/src/util/thread.h b/src/util/thread.h new file mode 100644 index 000000000..31b31d284 --- /dev/null +++ b/src/util/thread.h @@ -0,0 +1,101 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#if defined(LEAN_MULTI_THREAD) +#include +#include +#include +#include +#define LEAN_THREAD_LOCAL thread_local +namespace lean { +using std::thread; +using std::mutex; +using std::atomic; +using std::atomic_bool; +using std::atomic_ushort; +using std::condition_variable; +using std::lock_guard; +using std::unique_lock; +using std::atomic_load; +using std::atomic_fetch_add_explicit; +using std::atomic_fetch_sub_explicit; +using std::memory_order_relaxed; +namespace this_thread = std::this_thread; +} +#else +#include +#include +#define LEAN_THREAD_LOCAL +namespace lean { +constexpr int memory_order_relaxed = 0; +template +class atomic { + T m_value; +public: + atomic(T const & v = T()):m_value(v) {} + atomic(T && v):m_value(std::forward(v)) {} + atomic(atomic const & v):m_value(v.m_value) {} + atomic(atomic && v):m_value(std::forward(v.m_value)) {} + atomic & operator=(T const & v) { m_value = v; return *this; } + atomic & operator=(T && v) { m_value = std::forward(v); return *this; } + atomic & operator=(atomic const & v) { m_value = v.m_value; return *this; } + atomic & operator=(atomic && v) { m_value = std::forward(v.m_value); return *this; } + operator T() const { return m_value; } + void store(T const & v) { m_value = v; } + T load() const { return m_value; } + atomic & operator|=(T const & v) { m_value |= v; return *this; } + atomic & operator+=(T const & v) { m_value += v; return *this; } + atomic & operator-=(T const & v) { m_value -= v; return *this; } + atomic & operator++() { ++m_value; return *this; } + atomic operator++(int ) { atomic tmp(*this); ++m_value; return tmp; } + atomic & operator--() { --m_value; return *this; } + atomic operator--(int ) { atomic tmp(*this); --m_value; return tmp; } + friend T atomic_load(atomic const * a) { return a->m_value; } + friend T atomic_fetch_add_explicit(atomic * a, T const & v, int ) { T r(a->m_value); a->m_value += v; return r; } + friend T atomic_fetch_sub_explicit(atomic * a, T const & v, int ) { T r(a->m_value); a->m_value -= v; return r; } +}; +typedef atomic atomic_ushort; +typedef atomic atomic_bool; +class thread { +public: + thread() {} + template + thread(Function && fun, Args &&... args) { + fun(std::forward(args)...); + } + typedef unsigned id; + bool joinable() const { return true; } + void join() {} +}; +class this_thread { +public: + template + static void sleep_for(std::chrono::duration const &) {} + static thread::id get_id() { return 0; } + static void yield() {} +}; +class mutex { +public: + void lock() {} + void unlock() {} +}; +class condition_variable { +public: + template void wait(Lock const &) {} + void notify_all() {} + void notify_one() {} +}; +template class lock_guard { +public: + lock_guard(T const &) {} +}; +template class unique_lock { +public: + unique_lock(T const &) {} +}; +} +#endif diff --git a/src/util/trace.cpp b/src/util/trace.cpp index 76e44167c..9796e8d55 100644 --- a/src/util/trace.cpp +++ b/src/util/trace.cpp @@ -18,7 +18,7 @@ namespace lean { #ifdef LEAN_TRACE std::ofstream tout(LEAN_TRACE_OUT); -std::mutex trace_mutex; +mutex trace_mutex; #endif static std::unique_ptr> g_enabled_trace_tags; diff --git a/src/util/trace.h b/src/util/trace.h index e9d276794..dee441f96 100644 --- a/src/util/trace.h +++ b/src/util/trace.h @@ -7,13 +7,13 @@ Author: Leonardo de Moura #pragma once #ifdef LEAN_TRACE -#include +#include "util/thread.h" #include namespace lean { extern std::ofstream tout; -extern std::mutex trace_mutex; +extern mutex trace_mutex; } -#define TRACE_CODE(CODE) { std::lock_guard _lean_trace_lock_(lean::trace_mutex); CODE } +#define TRACE_CODE(CODE) { lock_guard _lean_trace_lock_(lean::trace_mutex); CODE } #else #define TRACE_CODE(CODE) #endif diff --git a/src/util/unlock_guard.h b/src/util/unlock_guard.h index 6b36d71d6..65cdccd4c 100644 --- a/src/util/unlock_guard.h +++ b/src/util/unlock_guard.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include "util/thread.h" namespace lean { /** \brief The class \c unlock_guard is a mutex wrapper that provides a @@ -17,7 +17,7 @@ namespace lean { Example: { - std::lock_guard lock(m); + lock_guard lock(m); ... { unlock_guard unlock(m); @@ -30,9 +30,9 @@ namespace lean { \warning The calling thread must own the lock to m_mutex */ class unlock_guard { - std::mutex & m_mutex; + mutex & m_mutex; public: - explicit unlock_guard(std::mutex & m):m_mutex(m) { m_mutex.unlock(); } + explicit unlock_guard(mutex & m):m_mutex(m) { m_mutex.unlock(); } unlock_guard(unlock_guard const &) = delete; unlock_guard(unlock_guard &&) = delete; unlock_guard & operator=(unlock_guard const &) = delete;