diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp
index 9ccc00063c..6cef5eb68f 100644
--- a/src/tests/util/thread.cpp
+++ b/src/tests/util/thread.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <mutex>
 #include <vector>
+#include "util/shared_mutex.h"
 
 void foo() {
     static thread_local std::vector<int> v(1024);
@@ -26,6 +27,30 @@ static void tst1() {
     }
 }
 
+static void tst2() {
+    unsigned N = 10;
+    unsigned n = 1;
+    lean::shared_mutex mut;
+    std::vector<std::thread> threads;
+    for (unsigned i = 0; i < N; i++) {
+        threads.emplace_back([&]() {
+                unsigned sum = 0;
+                {
+                    lean::shared_lock lock(mut);
+                    for (unsigned i = 0; i < 1000000; i++)
+                        sum += n;
+                }
+                {
+                   lean::unique_lock lock(mut);
+                   std::cout << sum << "\n";
+                }
+            });
+    }
+    for (unsigned i = 0; i < N; i++)
+        threads[i].join();
+}
+
 int main() {
+    tst2(); return 0;
     tst1();
 }
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index de6ff5448e..5f43c10aac 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_library(util trace.cpp debug.cpp name.cpp exception.cpp
   hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp
-  memory.cpp)
+  memory.cpp shared_mutex.cpp)
diff --git a/src/util/shared_mutex.cpp b/src/util/shared_mutex.cpp
new file mode 100644
index 0000000000..abcdba940c
--- /dev/null
+++ b/src/util/shared_mutex.cpp
@@ -0,0 +1,70 @@
+// 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
+#include "util/shared_mutex.h"
+
+namespace lean {
+shared_mutex::shared_mutex():m_state(0) {}
+shared_mutex::~shared_mutex() {
+    std::lock_guard<std::mutex> lock(m_mutex);
+}
+
+void shared_mutex::lock() {
+    std::unique_lock<std::mutex> lock(m_mutex);
+    while (m_state & write_entered)
+        m_gate1.wait(lock);
+    m_state |= write_entered;
+    while (m_state & readers)
+        m_gate2.wait(lock);
+}
+
+bool shared_mutex::try_lock() {
+    std::unique_lock<std::mutex> lock(m_mutex);
+    if (m_state == 0) {
+        m_state = write_entered;
+        return true;
+    }
+    return false;
+}
+
+void shared_mutex::unlock() {
+    std::lock_guard<std::mutex> lock(m_mutex);
+    m_state = 0;
+    m_gate1.notify_all();
+}
+
+void shared_mutex::lock_shared() {
+    std::unique_lock<std::mutex> lock(m_mutex);
+    while ((m_state & write_entered) || (m_state & readers) == readers)
+        m_gate1.wait(lock);
+    unsigned num_readers = (m_state & readers) + 1;
+    m_state &= ~readers;
+    m_state |= num_readers;
+}
+
+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) {
+        ++num_readers;
+        m_state &= ~readers;
+        m_state |= num_readers;
+        return true;
+    }
+    return false;
+}
+
+void shared_mutex::unlock_shared() {
+    std::lock_guard<std::mutex> lock(m_mutex);
+    unsigned num_readers = (m_state & readers) - 1;
+    m_state &= ~readers;
+    m_state |= num_readers;
+    if (m_state & write_entered) {
+        if (num_readers == 0)
+            m_gate2.notify_one();
+    } else {
+        if (num_readers == readers - 1)
+            m_gate1.notify_one();
+    }
+}
+}
diff --git a/src/util/shared_mutex.h b/src/util/shared_mutex.h
new file mode 100644
index 0000000000..876407f914
--- /dev/null
+++ b/src/util/shared_mutex.h
@@ -0,0 +1,48 @@
+// 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
+#include <mutex>
+#include <condition_variable>
+#include <climits>
+
+namespace lean {
+class shared_mutex {
+    std::mutex              m_mutex;
+    std::condition_variable m_gate1;
+    std::condition_variable m_gate2;
+    unsigned                m_state;
+
+    static constexpr unsigned write_entered = 1u << (sizeof(unsigned)*8 - 1);
+    static constexpr unsigned readers       = ~write_entered;
+
+public:
+    shared_mutex();
+    ~shared_mutex();
+
+    shared_mutex(shared_mutex const &) = delete;
+    shared_mutex(shared_mutex &&) = delete;
+    shared_mutex& operator=(shared_mutex const &) = delete;
+    shared_mutex&& operator=(shared_mutex &&) = delete;
+
+    void lock();
+    bool try_lock();
+    void unlock();
+
+    void lock_shared();
+    bool try_lock_shared();
+    void unlock_shared();
+};
+
+class shared_lock {
+    shared_mutex & m_mutex;
+public:
+    shared_lock(shared_mutex & m):m_mutex(m) { m_mutex.lock_shared(); }
+    ~shared_lock() { m_mutex.unlock_shared(); }
+};
+
+class unique_lock {
+    shared_mutex & m_mutex;
+public:
+    unique_lock(shared_mutex & m):m_mutex(m) { m_mutex.lock(); }
+    ~unique_lock() { m_mutex.unlock(); }
+};
+}