From e9ef59ab3e56ba9ba23a4aeaac063cee1c9ac933 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Jun 2014 15:46:16 -0700 Subject: [PATCH] feat(util): add global (thread local) script_state objects Signed-off-by: Leonardo de Moura --- src/tests/util/thread.cpp | 50 ++++++++++++++++--- src/util/CMakeLists.txt | 2 +- src/util/thread_script_state.cpp | 85 ++++++++++++++++++++++++++++++++ src/util/thread_script_state.h | 34 +++++++++++++ 4 files changed, 162 insertions(+), 9 deletions(-) create mode 100644 src/util/thread_script_state.cpp create mode 100644 src/util/thread_script_state.h diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index f251e4e70..e8b39298c 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/debug.h" #include "util/shared_mutex.h" #include "util/interrupt.h" +#include "util/thread_script_state.h" using namespace lean; #if defined(LEAN_MULTI_THREAD) @@ -171,14 +172,42 @@ static void tst6() { t1.request_interrupt(); t1.join(); } -#else -static void tst1() {} -static void tst2() {} -static void tst3() {} -static void tst4() {} -static void tst5() {} -static void tst6() {} -#endif + +static void tst7() { + std::cout << "start\n"; + system_dostring("print('hello'); x = 10;"); + interruptible_thread t1([]() { + script_state S = get_thread_script_state(); + S.dostring("print(x)\n" + "for i = 1, 100000 do\n" + " x = x + 1\n" + "end\n" + "print(x)\n"); + }); + interruptible_thread t2([]() { + script_state S = get_thread_script_state(); + S.dostring("print(x)\n" + "for i = 1, 20000 do\n" + " x = x + 1\n" + "end\n" + "print(x)\n"); + }); + t1.join(); t2.join(); + std::cout << "done\n"; +} + +static void tst8() { + std::cout << "starting tst8\n"; + interruptible_thread t1([]() { + script_state S = get_thread_script_state(); + S.dostring("print(x)\n" + "for i = 1, 10000 do\n" + " x = x + 1\n" + "end\n" + "print(x)\n"); + }); + t1.join(); +} int main() { save_stack_info(); @@ -188,5 +217,10 @@ int main() { tst4(); tst5(); tst6(); + tst7(); + tst8(); return has_violations() ? 1 : 0; } +#else +int main() { std::cout << "foo\n"; return 0; } +#endif diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 7dfc3d182..6174ae19b 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -9,6 +9,6 @@ add_library(util trace.cpp debug.cpp name.cpp name_set.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp - serializer.cpp lbool.cpp ${THREAD_CPP}) + serializer.cpp lbool.cpp thread_script_state.cpp ${THREAD_CPP}) target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/util/thread_script_state.cpp b/src/util/thread_script_state.cpp new file mode 100644 index 000000000..e50ed4311 --- /dev/null +++ b/src/util/thread_script_state.cpp @@ -0,0 +1,85 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "util/thread.h" +#include "util/script_state.h" + +namespace lean { +static mutex g_code_mutex; +static std::vector g_code; +static mutex g_state_mutex; +static std::vector g_states; +static std::vector g_available_states; + +/** \brief Execute \c code in all states in the pool */ +void system_dostring(char const * code) { + { + // Execute code in all existing states + lock_guard lk(g_state_mutex); + for (auto & s : g_states) { + s.dostring(code); + } + } + { + // Save code for future states + lock_guard lk(g_code_mutex); + g_code.push_back(code); + } +} + +static script_state get_state() { + { + // Try to reuse existing state + lock_guard lk(g_state_mutex); + if (!g_available_states.empty()) { + script_state r(g_available_states.back()); + g_available_states.pop_back(); + return r; + } + } + + { + // Execute existing code in new state + lock_guard lk(g_code_mutex); + script_state r; + for (auto & c : g_code) + r.dostring(c.c_str()); + g_states.push_back(r); + { + // save new state in vector of all states + lock_guard lk(g_state_mutex); + g_states.push_back(r); + } + return r; + } +} + +static void recycle_state(script_state s) { + lock_guard lk(g_state_mutex); + g_available_states.push_back(s); +} + +struct script_state_ref { + script_state m_state; + script_state_ref():m_state(get_state()) {} + ~script_state_ref() { recycle_state(m_state); } +}; + +// We should use std::unique_ptr, but clang++ 3.3.1 crashes when we use it. +std::shared_ptr LEAN_THREAD_LOCAL g_thread_state; + +script_state get_thread_script_state() { + if (!g_thread_state) + g_thread_state = std::make_shared(); + return g_thread_state->m_state; +} + +void release_thread_script_state() { + g_thread_state = nullptr; +} +} diff --git a/src/util/thread_script_state.h b/src/util/thread_script_state.h new file mode 100644 index 000000000..f1776e929 --- /dev/null +++ b/src/util/thread_script_state.h @@ -0,0 +1,34 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/script_state.h" +namespace lean { +/** + \brief Execute the given piece of code in all global/system script_state objects. + + \remark The code fragments are saved. If a new thread needs to create a new + script_state object, all code blocks are executed. + + \remark System code should be installed when Lean is started. +*/ +void system_dostring(char const * code); +/** + \brief Retrieve a script_state object for the current thread. + The thread has exclusive access until the thread is destroyed, + or the method \c release_thread_script_state is invoked. + + \remark For performance reasons global script_state objects + are recycled. So, users should not delete/redefine functions + defined using #system_dostring. So, side-effects are discouraged. +*/ +script_state get_thread_script_state(); +/** + \brief Put the thread script_state back on the state pool, + and available for other threads. +*/ +void release_thread_script_state(); +}