From 6129cccc66cd9fa05ab50f5b551005da26b3e700 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 May 2014 08:34:44 -0700
Subject: [PATCH] perf(library/shared_environment): replace shared_mutex with
 simple mutex, the shared_mutex is just overhead and impacts negatively on
 performance tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/shared_environment.cpp | 10 +++++-----
 src/library/shared_environment.h   |  2 +-
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/library/shared_environment.cpp b/src/library/shared_environment.cpp
index f165bafa4d..b60b76e10f 100644
--- a/src/library/shared_environment.cpp
+++ b/src/library/shared_environment.cpp
@@ -11,27 +11,27 @@ shared_environment::shared_environment() {}
 shared_environment::shared_environment(environment const & env):m_env(env) {}
 
 environment shared_environment::get_environment() const {
-    shared_lock l(m_mutex);
+    unique_lock<mutex> l(m_mutex);
     return m_env;
 }
 
 void shared_environment::add(certified_declaration const & d) {
-    exclusive_lock l(m_mutex);
+    unique_lock<mutex> l(m_mutex);
     m_env = m_env.add(d);
 }
 
 void shared_environment::add(declaration const & d) {
-    exclusive_lock l(m_mutex);
+    unique_lock<mutex> l(m_mutex);
     m_env = m_env.add(d);
 }
 
 void shared_environment::replace(certified_declaration const & t) {
-    exclusive_lock l(m_mutex);
+    unique_lock<mutex> l(m_mutex);
     m_env = m_env.replace(t);
 }
 
 void shared_environment::update(std::function<environment(environment const &)> const & f) {
-    exclusive_lock l(m_mutex);
+    unique_lock<mutex> l(m_mutex);
     m_env = f(m_env);
 }
 }
diff --git a/src/library/shared_environment.h b/src/library/shared_environment.h
index 3a52a2a03e..eb68e06ff9 100644
--- a/src/library/shared_environment.h
+++ b/src/library/shared_environment.h
@@ -13,7 +13,7 @@ namespace lean {
 /** \brief Auxiliary object used when multiple threads are trying to populate the same environment. */
 class shared_environment {
     environment          m_env;
-    mutable shared_mutex m_mutex;
+    mutable mutex        m_mutex;
 public:
     shared_environment();
     shared_environment(environment const & env);