feat(library): unique token generator

src/library/CMakeLists.txt

@@ -21,4 +21,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
   documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp
   pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp
-  context_cache.cpp)
+  context_cache.cpp token.cpp)

src/library/init_module.cpp

@@ -54,6 +54,7 @@ Author: Leonardo de Moura
 #include "library/parray.h"
 #include "library/profiling.h"
 #include "library/time_task.h"
+#include "library/token.h"
 
 namespace lean {
 void initialize_library_core_module() {
@@ -75,6 +76,7 @@ void finalize_library_core_module() {
 }
 
 void initialize_library_module() {
+    initialize_token();
     initialize_local_context();
     initialize_metavar_context();
     initialize_fingerprint();
@@ -166,5 +168,6 @@ void finalize_library_module() {
     finalize_fingerprint();
     finalize_metavar_context();
     finalize_local_context();
+    finalize_token();
 }
 }

src/library/token.cpp

@@ -0,0 +1,54 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+*/
+#include <limits>
+#include "util/thread.h"
+#include "util/exception.h"
+#include "library/token.h"
+
+namespace lean {
+static unsigned g_next_thread_id       = 0;
+static mutex *  g_next_thread_id_guard = nullptr;
+
+LEAN_THREAD_VALUE(unsigned, g_thread_id, std::numeric_limits<unsigned>::max());
+LEAN_THREAD_VALUE(unsigned, g_next_idx, 0);
+
+token::token():
+    m_thread_id(std::numeric_limits<unsigned>::max()),
+    m_id(0) {
+}
+
+bool token::is_valid() const {
+    return m_thread_id != std::numeric_limits<unsigned>::max();
+}
+
+token mk_unique_token() {
+    if (g_thread_id == std::numeric_limits<unsigned>::max()) {
+        lock_guard<mutex> lock(*g_next_thread_id_guard);
+        g_thread_id = g_next_thread_id;
+        g_next_thread_id++;
+        if (g_next_thread_id == std::numeric_limits<unsigned>::max()) {
+            g_next_thread_id--;
+            throw exception("failed to generate unique token, too many threads");
+        }
+    }
+    token r(g_thread_id, g_next_idx);
+    g_next_idx++;
+    if (g_next_idx == std::numeric_limits<unsigned>::max()) {
+        g_next_idx--;
+        throw exception("failed to generate unique token, too many tokens have been generated");
+    }
+    return r;
+}
+
+void initialize_token() {
+    g_next_thread_id_guard = new mutex();
+    register_thread_local_reset_fn([]() { g_next_idx = 0; });
+}
+
+void finalize_token() {
+    delete g_next_thread_id_guard;
+}
+}

src/library/token.h

@@ -0,0 +1,46 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/pair.h"
+
+namespace lean {
+class token {
+    unsigned m_thread_id;
+    unsigned m_id;
+    token(unsigned i1, unsigned i2):m_thread_id(i1), m_id(i2) {}
+    friend token mk_unique_token();
+    friend bool operator==(token const & t1, token const & t2) {
+        return t1.m_thread_id == t2.m_thread_id && t1.m_id == t2.m_id;
+    }
+public:
+    /* Use `mk_unique_token()`, this constructor produces invalid tokens.
+       It can be used to represent uninitialized token values. */
+    token();
+    bool is_valid() const;
+};
+
+inline bool operator!=(token const & t1, token const & t2) {
+    return !(t1 == t2);
+}
+
+/* Create a global unique token (modulo reset_thread_local).
+
+   Assumptions:
+   - We do not create more than 2^32 - 1 threads.
+     This is fine because we create a small set of threads
+     when we start the process, and then we create only tasks.
+
+   - Each thread does not create more than 2^32 tokens.
+     This is fine because we reset the thread local counters
+     after each \c reset_thread_local operation.
+
+   That being said, if the assumptions above are violated
+   \c mk_unique_token throws an exception */
+token mk_unique_token();
+
+void initialize_token();
+void finalize_token();
+}