fix(lua): make sure environment objects can be safely accessed/updated from current threads

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

src/bindings/lua/environment.cpp

@@ -21,10 +21,18 @@ bool is_environment(lua_State * L, int idx) {
     return testudata(L, idx, environment_mt);
 }
 
-environment & to_environment(lua_State * L, int idx) {
+static environment & to_environment(lua_State * L, int idx) {
     return *static_cast<environment*>(luaL_checkudata(L, idx, environment_mt));
 }
 
+ro_environment::ro_environment(lua_State * L, int idx):
+    read_only_environment(to_environment(L, idx)) {
+}
+
+rw_environment::rw_environment(lua_State * L, int idx):
+    read_write_environment(to_environment(L, idx)) {
+}
+
 static int environment_gc(lua_State * L) {
     to_environment(L, 1).~environment();
     return 0;
@@ -43,67 +51,76 @@ static int mk_environment(lua_State * L) {
 }
 
 static int environment_add_uvar(lua_State * L) {
+    rw_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        to_environment(L, 1).add_uvar(to_name_ext(L, 2));
+        env->add_uvar(to_name_ext(L, 2));
     else
-        to_environment(L, 1).add_uvar(to_name_ext(L, 2), to_level(L, 3));
+        env->add_uvar(to_name_ext(L, 2), to_level(L, 3));
     return 0;
 }
 
 static int environment_is_ge(lua_State * L) {
-    lua_pushboolean(L, to_environment(L, 1).is_ge(to_level(L, 2), to_level(L, 3)));
+    ro_environment env(L, 1);
+    lua_pushboolean(L, env->is_ge(to_level(L, 2), to_level(L, 3)));
     return 1;
 }
 
 static int environment_get_uvar(lua_State * L) {
-    return push_level(L, to_environment(L, 1).get_uvar(to_name_ext(L, 2)));
+    ro_environment env(L, 1);
+    return push_level(L, env->get_uvar(to_name_ext(L, 2)));
 }
 
 static int environment_add_definition(lua_State * L) {
+    rw_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 3) {
-        to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3));
+        env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3));
     } else if (nargs == 4) {
         if (is_expr(L, 4))
-            to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4));
+            env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4));
         else
-            to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), lua_toboolean(L, 4));
+            env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), lua_toboolean(L, 4));
     } else {
-        to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4), lua_toboolean(L, 5));
+        env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4), lua_toboolean(L, 5));
     }
     return 0;
 }
 
 static int environment_add_theorem(lua_State * L) {
-    to_environment(L, 1).add_theorem(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4));
+    rw_environment env(L, 1);
+    env->add_theorem(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4));
     return 0;
 }
 
 static int environment_add_var(lua_State * L) {
-    to_environment(L, 1).add_var(to_name_ext(L, 2), to_nonnull_expr(L, 3));
+    rw_environment env(L, 1);
+    env->add_var(to_name_ext(L, 2), to_nonnull_expr(L, 3));
     return 0;
 }
 
 static int environment_add_axiom(lua_State * L) {
-    to_environment(L, 1).add_axiom(to_name_ext(L, 2), to_nonnull_expr(L, 3));
+    rw_environment env(L, 1);
+    env->add_axiom(to_name_ext(L, 2), to_nonnull_expr(L, 3));
     return 0;
 }
 
 static int environment_check_type(lua_State * L) {
+    ro_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        return push_expr(L, to_environment(L, 1).infer_type(to_nonnull_expr(L, 2)));
+        return push_expr(L, env->infer_type(to_nonnull_expr(L, 2)));
     else
-        return push_expr(L, to_environment(L, 1).infer_type(to_nonnull_expr(L, 2), to_context(L, 3)));
+        return push_expr(L, env->infer_type(to_nonnull_expr(L, 2), to_context(L, 3)));
 }
 
 static int environment_normalize(lua_State * L) {
+    ro_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        return push_expr(L, to_environment(L, 1).normalize(to_nonnull_expr(L, 2)));
+        return push_expr(L, env->normalize(to_nonnull_expr(L, 2)));
     else
-        return push_expr(L, to_environment(L, 1).normalize(to_nonnull_expr(L, 2), to_context(L, 3)));
+        return push_expr(L, env->normalize(to_nonnull_expr(L, 2), to_context(L, 3)));
 }
 
 static int environment_pred(lua_State * L) {

src/bindings/lua/environment.h

@@ -6,12 +6,14 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <lua.hpp>
+#include "kernel/threadsafe_environment.h"
+
 namespace lean {
 class environment;
 void open_environment(lua_State * L);
 bool is_environment(lua_State * L, int idx);
-environment & to_environment(lua_State * L, int idx);
 int push_environment(lua_State * L, environment const & env);
+
 /**
    \brief Auxiliary class for setting the Lua registry of a Lua state
    with an environment object.
@@ -22,4 +24,22 @@ public:
     set_environment(lua_State * L, environment & env);
     ~set_environment();
 };
+
+/**
+   \brief Helper class for getting a read-only reference
+   for an environment object on the Lua stack.
+*/
+class ro_environment : public read_only_environment {
+public:
+    ro_environment(lua_State * L, int idx);
+};
+
+/**
+   \brief Helper class for getting a read-write reference
+   for an environment object on the Lua stack.
+*/
+class rw_environment : public read_write_environment {
+public:
+    rw_environment(lua_State * L, int idx);
+};
 }

src/kernel/environment.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/environment.h"
+#include "kernel/threadsafe_environment.h"
 #include "kernel/type_checker.h"
 #include "kernel/normalizer.h"
 
@@ -70,6 +71,10 @@ struct environment::imp {
     std::vector<std::unique_ptr<extension>> m_extensions;
     friend class extension;
 
+    // This mutex is only used to implement threadsafe environment objects
+    // in the external APIs
+    shared_mutex                         m_mutex;
+
     extension & get_extension_core(unsigned extid) {
         if (extid >= m_extensions.size())
             m_extensions.resize(extid+1);
@@ -514,11 +519,11 @@ object const & environment::get_object(unsigned i, bool local) const {
     return m_ptr->get_object(i, local);
 }
 
-expr environment::infer_type(expr const & e, context const & ctx) {
+expr environment::infer_type(expr const & e, context const & ctx) const {
     return m_ptr->infer_type(e, ctx);
 }
 
-expr environment::normalize(expr const & e, context const & ctx) {
+expr environment::normalize(expr const & e, context const & ctx) const {
     return m_ptr->normalize(e, ctx);
 }
 
@@ -560,4 +565,16 @@ environment::extension const * environment::extension::get_parent_core() const {
     }
     return nullptr;
 }
+
+read_only_environment::read_only_environment(environment const & env):
+    m_env(env),
+    m_lock(m_env.m_ptr->m_mutex) {
+}
+read_only_environment::~read_only_environment() {}
+
+read_write_environment::read_write_environment(environment & env):
+    m_env(env),
+    m_lock(m_env.m_ptr->m_mutex) {
+}
+read_write_environment::~read_write_environment() {}
 }

src/kernel/environment.h

@@ -25,6 +25,8 @@ private:
     explicit environment(std::shared_ptr<imp> const & ptr);
     unsigned get_num_objects(bool local) const;
     object const & get_object(unsigned i, bool local) const;
+    friend class read_only_environment;
+    friend class read_write_environment;
 public:
     environment();
     ~environment();
@@ -145,12 +147,12 @@ public:
     /**
        \brief Return the type of \c e in the given context and this environment.
     */
-    expr infer_type(expr const & e, context const & ctx = context());
+    expr infer_type(expr const & e, context const & ctx = context()) const;
 
     /**
        \brief Normalize \c e in the given context and this environment.
     */
-    expr normalize(expr const & e, context const & ctx = context());
+    expr normalize(expr const & e, context const & ctx = context()) const;
 
     /** \brief Iterator for Lean environment objects. */
     class object_iterator {

src/kernel/threadsafe_environment.h

@@ -0,0 +1,41 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/shared_mutex.h"
+#include "kernel/environment.h"
+
+namespace lean {
+/**
+   \brief The environment object is not thread safe.
+   The helper classes \c read_only_environment and \c read_write_environment
+   provides thread safe access to the environment object.
+
+   \remark We do not use these classes internally.
+   They are only used for implementing external APIs.
+*/
+class read_only_environment {
+    environment   m_env;
+    shared_lock   m_lock;
+public:
+    read_only_environment(environment const & env);
+    ~read_only_environment();
+    operator environment const &() const { return m_env; }
+    environment const * operator->() const { return &m_env; }
+};
+
+/**
+   \brief See \c read_only_environment
+*/
+class read_write_environment {
+    environment  m_env;
+    unique_lock  m_lock;
+public:
+    read_write_environment(environment & env);
+    ~read_write_environment();
+    operator environment &() { return m_env; }
+    environment * operator->() { return &m_env; }
+};
+}

src/util/shared_mutex.cpp

@@ -1,5 +1,15 @@
-// C++11 does not support std::shared_mutex and std::shared_lock yet.
-// This piece of Code is based on the proposal for C++14
+/**
+   Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+   Released under Apache 2.0 license as described in the file LICENSE.
+
+   Author: Leonardo de Moura
+
+   C++11 does not support std::shared_mutex and std::shared_lock yet.
+   This piece of code is based on the proposal submitted to the C++
+   standardization committee. The proposal was written by Howard
+   Hinnant. The proposal is also part of the Boost library which is
+   licensed under http://www.boost.org/LICENSE_1_0.txt
+*/
 #include "util/shared_mutex.h"
 
 namespace lean {
@@ -41,8 +51,7 @@ void shared_mutex::lock_shared() {
     m_state |= num_readers;
 }
 
-bool shared_mutex::try_lock_shared()
-{
+bool shared_mutex::try_lock_shared() {
     std::unique_lock<std::mutex> lock(m_mutex);
     unsigned num_readers = m_state & readers;
     if (!(m_state & write_entered) && num_readers != readers) {

src/util/shared_mutex.h

@@ -1,5 +1,15 @@
-// C++11 does not support std::shared_mutex and std::shared_lock yet.
-// This piece of Code is based on the proposal for C++14
+/**
+   Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+   Released under Apache 2.0 license as described in the file LICENSE.
+
+   Author: Leonardo de Moura
+
+   C++11 does not support std::shared_mutex and std::shared_lock yet.
+   This piece of code is based on the proposal submitted to the C++
+   standardization committee. The proposal was written by Howard
+   Hinnant. The proposal is also part of the Boost library which is
+   licensed under http://www.boost.org/LICENSE_1_0.txt
+*/
 #include <mutex>
 #include <condition_variable>
 #include <climits>