From 9452d164eced4904b2d689d894320da50679aa9d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 May 2014 12:27:12 -0700
Subject: [PATCH] feat(util/script_state): use recursive_mutex instead of mutex

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/script_state.cpp | 10 +++++-----
 src/util/script_state.h   |  8 ++++----
 src/util/thread.h         |  8 +++++++-
 src/util/unlock_guard.h   |  5 +++--
 4 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp
index 04d0e72f1..c345ab867 100644
--- a/src/util/script_state.cpp
+++ b/src/util/script_state.cpp
@@ -40,8 +40,8 @@ void open_extra(lua_State * L);
 static char g_weak_ptr_key; // key for Lua registry (used at get_weak_ptr and save_weak_ptr)
 
 struct script_state::imp {
-    lua_State * m_state;
-    mutex       m_mutex;
+    lua_State *           m_state;
+    recursive_mutex       m_mutex;
     std::unordered_set<std::string> m_imported_modules;
 
     static std::weak_ptr<imp> * get_weak_ptr(lua_State * L) {
@@ -100,12 +100,12 @@ struct script_state::imp {
     }
 
     void dofile(char const * fname) {
-        lock_guard<mutex> lock(m_mutex);
+        lock_guard<recursive_mutex> lock(m_mutex);
         ::lean::dofile(m_state, fname);
     }
 
     void dostring(char const * str) {
-        lock_guard<mutex> lock(m_mutex);
+        lock_guard<recursive_mutex> lock(m_mutex);
         ::lean::dostring(m_state, str);
     }
 
@@ -162,7 +162,7 @@ bool script_state::import_explicit(char const * str) {
     return m_ptr->import_explicit(str);
 }
 
-mutex & script_state::get_mutex() {
+recursive_mutex & script_state::get_mutex() {
     return m_ptr->m_mutex;
 }
 
diff --git a/src/util/script_state.h b/src/util/script_state.h
index d4a931288..ff1a1d2ba 100644
--- a/src/util/script_state.h
+++ b/src/util/script_state.h
@@ -20,7 +20,7 @@ public:
 private:
     std::shared_ptr<imp> m_ptr;
     friend script_state to_script_state(lua_State * L);
-    mutex & get_mutex();
+    recursive_mutex & get_mutex();
     lua_State * get_state();
     friend class data_channel;
 public:
@@ -60,7 +60,7 @@ public:
     */
     template<typename F>
     typename std::result_of<F(lua_State * L)>::type apply(F && f) {
-        lock_guard<mutex> lock(get_mutex());
+        lock_guard<recursive_mutex> lock(get_mutex());
         return f(get_state());
     }
 
@@ -74,13 +74,13 @@ public:
     */
     template<typename F>
     void exec_unprotected(F && f) {
-        unlock_guard unlock(get_mutex());
+        unlock_guard<recursive_mutex> unlock(get_mutex());
         f();
     }
 
     template<typename F>
     void exec_protected(F && f) {
-        lock_guard<mutex> lock(get_mutex());
+        lock_guard<recursive_mutex> lock(get_mutex());
         f();
     }
 };
diff --git a/src/util/thread.h b/src/util/thread.h
index d328fd4b7..22440cbfa 100644
--- a/src/util/thread.h
+++ b/src/util/thread.h
@@ -18,6 +18,7 @@ namespace lean {
 inline void set_thread_stack_size(size_t ) {}
 using std::thread;
 using std::mutex;
+using std::recursive_mutex;
 using std::atomic;
 using std::atomic_bool;
 using std::atomic_ushort;
@@ -40,7 +41,7 @@ namespace lean {
 void set_thread_stack_size(size_t );
 boost::thread::attributes const & get_thread_attributes();
 using boost::thread;
-using boost::mutex;
+using boost::recursive_mutex;
 using boost::atomic;
 using boost::memory_order_relaxed;
 using boost::condition_variable;
@@ -118,6 +119,11 @@ public:
     void lock() {}
     void unlock() {}
 };
+class recursive_mutex {
+public:
+    void lock() {}
+    void unlock() {}
+};
 class condition_variable {
 public:
     template<typename Lock> void wait(Lock const &) {}
diff --git a/src/util/unlock_guard.h b/src/util/unlock_guard.h
index 65cdccd4c..1ed621974 100644
--- a/src/util/unlock_guard.h
+++ b/src/util/unlock_guard.h
@@ -29,10 +29,11 @@ namespace lean {
 
    \warning The calling thread must own the lock to m_mutex
 */
+template<typename Mutex>
 class unlock_guard {
-    mutex & m_mutex;
+    Mutex & m_mutex;
 public:
-    explicit unlock_guard(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;