From a2aa90ae66a8b5056d2ca75e06ddf9b56cc1ad36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Nov 2013 15:40:37 -0800 Subject: [PATCH] refactor(util/script_state): replace std::recursive_mutex with std::mutex, and use unlock_guard The unlock_guard and exec_unprotected will be useful also for implementing the Lua tactic API. Signed-off-by: Leonardo de Moura --- src/frontends/lean/register_module.cpp | 11 +++++-- src/util/script_state.cpp | 10 +++--- src/util/script_state.h | 20 +++++++++--- src/util/unlock_guard.h | 42 ++++++++++++++++++++++++++ 4 files changed, 71 insertions(+), 12 deletions(-) create mode 100644 src/util/unlock_guard.h diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp index 71e81ecf2..78d83cb03 100644 --- a/src/frontends/lean/register_module.cpp +++ b/src/frontends/lean/register_module.cpp @@ -19,8 +19,11 @@ static int parse_lean_expr_core(lua_State * L, ro_environment const & env, io_st char const * src = luaL_checkstring(L, 1); std::istringstream in(src); script_state S = to_script_state(L); - push_expr(L, parse_expr(env, st, in, &S)); - return 1; + expr r; + S.exec_unprotected([&]() { + r = parse_expr(env, st, in, &S); + }); + return push_expr(L, r); } /** \see parse_lean_expr */ @@ -75,7 +78,9 @@ static void parse_lean_cmds_core(lua_State * L, rw_environment & env, io_state & char const * src = luaL_checkstring(L, 1); std::istringstream in(src); script_state S = to_script_state(L); - parse_commands(env, st, in, &S); + S.exec_unprotected([&]() { + parse_commands(env, st, in, &S); + }); } /** \see parse_lean_cmds */ diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp index a4dc5d05a..eaac79e34 100644 --- a/src/util/script_state.cpp +++ b/src/util/script_state.cpp @@ -41,8 +41,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; - std::recursive_mutex m_mutex; + lua_State * m_state; + std::mutex m_mutex; static std::weak_ptr * get_weak_ptr(lua_State * L) { lua_pushlightuserdata(L, static_cast(&g_weak_ptr_key)); @@ -92,12 +92,12 @@ struct script_state::imp { } void dofile(char const * fname) { - std::lock_guard lock(m_mutex); + std::lock_guard lock(m_mutex); ::lean::dofile(m_state, fname); } void dostring(char const * str) { - std::lock_guard lock(m_mutex); + std::lock_guard lock(m_mutex); ::lean::dostring(m_state, str); } }; @@ -126,7 +126,7 @@ void script_state::dostring(char const * str) { m_ptr->dostring(str); } -std::recursive_mutex & script_state::get_mutex() { +std::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 67a9b3c70..8bd14a47e 100644 --- a/src/util/script_state.h +++ b/src/util/script_state.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/unlock_guard.h" namespace lean { /** @@ -20,12 +21,12 @@ private: std::shared_ptr m_ptr; script_state(std::weak_ptr const & ptr); friend script_state to_script_state(lua_State * L); - std::recursive_mutex & get_mutex(); + std::mutex & get_mutex(); lua_State * get_state(); friend class data_channel; public: script_state(); - virtual ~script_state(); + ~script_state(); /** \brief Execute the file with the given name. @@ -36,14 +37,14 @@ public: \brief Execute the given string. This method throws an exception if an error occurs. */ - virtual void dostring(char const * str); + void dostring(char const * str); /** \brief Execute \c f in the using the internal Lua State. */ template typename std::result_of::type apply(F && f) { - std::lock_guard lock(get_mutex()); + std::lock_guard lock(get_mutex()); return f(get_state()); } @@ -51,6 +52,17 @@ public: static void register_module(reg_fn f); static void register_code(char const * code); + + /** + \brief Auxiliary function for writing API bindings + that release the lock to this object while executing + \c f. + */ + template + void exec_unprotected(F && f) { + unlock_guard unlock(get_mutex()); + f(); + } }; /** \brief Return a reference to the script_state object that is wrapping \c L. diff --git a/src/util/unlock_guard.h b/src/util/unlock_guard.h new file mode 100644 index 000000000..6b36d71d6 --- /dev/null +++ b/src/util/unlock_guard.h @@ -0,0 +1,42 @@ +/* +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 +#include +namespace lean { +/** + \brief The class \c unlock_guard is a mutex wrapper that provides a + convenient RAII-style mechanism for releasing a mutex for the + duration of a scoped block. + + It is the dual of lock_guard in the standard library. + + Example: + + { + std::lock_guard lock(m); + ... + { + unlock_guard unlock(m); + ... + } + ... + } + + + \warning The calling thread must own the lock to m_mutex +*/ +class unlock_guard { + std::mutex & m_mutex; +public: + explicit unlock_guard(std::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; + unlock_guard & operator=(unlock_guard &&) = delete; + ~unlock_guard() { m_mutex.lock(); } +}; +}