Add multi-thread tests

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

src/tests/kernel/CMakeLists.txt

@@ -4,3 +4,6 @@ add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr_tst)
 add_executable(normalize normalize.cpp)
 target_link_libraries(normalize ${EXTRA_LIBS})
 add_test(normalize ${CMAKE_CURRENT_BINARY_DIR}/normalize)
+add_executable(threads threads.cpp)
+target_link_libraries(threads ${EXTRA_LIBS})
+add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads)

src/tests/kernel/threads.cpp

@@ -0,0 +1,53 @@
+/*
+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 <thread>
+#include <mutex>
+#include <vector>
+#include "expr.h"
+#include "max_sharing.h"
+#include "free_vars.h"
+#include "deep_copy.h"
+#include "abstract.h"
+#include "normalize.h"
+#include "test.h"
+using namespace lean;
+
+static void mk(expr const & a) {
+    expr b = constant("b");
+    for (unsigned i = 0; i < 100; i++) {
+        expr h = constant("h");
+        h = h(a);
+        for (unsigned j = 0; j < 100; j++)
+            h = app(h, b);
+        h = max_sharing(h);
+        lean_assert(closed(h));
+        h = normalize(h);
+        h = abstract(a, h);
+        lean_assert(!closed(h));
+        h = deep_copy(h);
+    }
+}
+
+static void tst1() {
+    expr a = constant("a");
+    expr f = constant("f");
+    a = f(a, a);
+    std::vector<std::thread> ts;
+
+    for (unsigned i = 0; i < 8; i++) {
+        ts.push_back(std::thread([&](){ mk(a); }));
+    }
+    for (unsigned i = 0; i < 8; i++) {
+        ts[i].join();
+        std::cout << "finished " << i << "\n";
+    }
+}
+
+int main() {
+    tst1();
+    return 0;
+}