feat(util): add global (thread local) script_state objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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

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})

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 <vector>
+#include <string>
+#include "util/thread.h"
+#include "util/script_state.h"
+
+namespace lean {
+static mutex g_code_mutex;
+static std::vector<std::string>  g_code;
+static mutex g_state_mutex;
+static std::vector<script_state> g_states;
+static std::vector<script_state> 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<mutex> lk(g_state_mutex);
+        for (auto & s : g_states) {
+            s.dostring(code);
+        }
+    }
+    {
+        // Save code for future states
+        lock_guard<mutex> lk(g_code_mutex);
+        g_code.push_back(code);
+    }
+}
+
+static script_state get_state() {
+    {
+        // Try to reuse existing state
+        lock_guard<mutex> 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<mutex> 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<mutex> lk(g_state_mutex);
+            g_states.push_back(r);
+        }
+        return r;
+    }
+}
+
+static void recycle_state(script_state s) {
+    lock_guard<mutex> 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<script_state_ref> LEAN_THREAD_LOCAL g_thread_state;
+
+script_state get_thread_script_state() {
+    if (!g_thread_state)
+        g_thread_state = std::make_shared<script_state_ref>();
+    return g_thread_state->m_state;
+}
+
+void release_thread_script_state() {
+    g_thread_state = nullptr;
+}
+}

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();
+}