diff --git a/src/library/mt_task_queue.cpp b/src/library/mt_task_queue.cpp index ec14fb2e13..14775a1872 100644 --- a/src/library/mt_task_queue.cpp +++ b/src/library/mt_task_queue.cpp @@ -110,6 +110,7 @@ void mt_task_queue::spawn_worker() { reset_thread_local(); { flet _(this_worker->m_current_task, t); + set_fresh_name_generator(t->get_name_generator()); scoped_current_task scope_cur_task(&t); notify_queue_changed(); lock.unlock(); diff --git a/src/util/fresh_name.cpp b/src/util/fresh_name.cpp index ea5dd3eba7..9905e14c22 100644 --- a/src/util/fresh_name.cpp +++ b/src/util/fresh_name.cpp @@ -12,49 +12,17 @@ Author: Leonardo de Moura #include "util/shared_mutex.h" namespace lean { -static name_set * g_fresh_name_prefixes = nullptr; -static shared_mutex * g_fresh_name_prefixes_guard = nullptr; - -static void register_fresh_name_prefix(name const & p) { - exclusive_lock lock(*g_fresh_name_prefixes_guard); - g_fresh_name_prefixes->insert(p); -} - -/* CACHE_RESET: NO */ -MK_THREAD_LOCAL_GET_DEF(name, get_prefix); -/* CACHE_RESET: YES */ -LEAN_THREAD_VALUE(unsigned, g_next_idx, 0); - -static bool is_fresh_prefix(name const & p) { - if (p == get_prefix()) - return true; - shared_lock lock(*g_fresh_name_prefixes_guard); - return g_fresh_name_prefixes->contains(p); -}; +static name * g_fresh = nullptr; +MK_THREAD_LOCAL_GET(name_generator, get_name_generator, *g_fresh); name mk_fresh_name() { - name & prefix = get_prefix(); - if (prefix.is_anonymous()) { - // prefix has not been initialized for this thread yet. - prefix = name::mk_internal_unique_name(); - register_fresh_name_prefix(prefix); - } - /* REMARK: after we implement RESET operation we will not need the following test anymore */ - if (g_next_idx == std::numeric_limits::max()) { - // avoid overflow - prefix = name(prefix, g_next_idx); - register_fresh_name_prefix(prefix); - g_next_idx = 0; - } - name r(prefix, g_next_idx); - g_next_idx++; - return r; + return get_name_generator().next(); } bool is_fresh_name(name const & n) { if (n.is_anonymous() || !n.is_numeral()) return false; - else if (is_fresh_prefix(n.get_prefix())) + else if (n.get_prefix() == *g_fresh) return true; else return is_fresh_name(n.get_prefix()); @@ -81,19 +49,7 @@ name sanitize_if_fresh(name const & n) { name mk_tagged_fresh_name(name const & tag) { lean_assert(tag.is_atomic()); - name & prefix = get_prefix(); - if (prefix.is_anonymous()) { - // prefix has not been initialized for this thread yet. - prefix = name::mk_internal_unique_name(); - } - if (g_next_idx == std::numeric_limits::max()) { - // avoid overflow - prefix = name(prefix, g_next_idx); - g_next_idx = 0; - } - name r(tag + prefix, g_next_idx); - g_next_idx++; - return r; + return tag + mk_fresh_name(); } bool is_tagged_by(name const & n, name const & tag) { @@ -123,13 +79,23 @@ optional get_tagged_name_suffix(name const & n, name const & tag) { } } +name_generator get_fresh_name_generator_snapshot() { + return get_name_generator(); +} + +void set_fresh_name_generator(name_generator const & g) { + get_name_generator() = g; +} + +name_generator mk_fresh_name_generator_child() { + return get_name_generator().mk_child(); +} + void initialize_fresh_name() { - g_fresh_name_prefixes = new name_set(); - g_fresh_name_prefixes_guard = new shared_mutex(); + g_fresh = new name("_fresh"); } void finalize_fresh_name() { - delete g_fresh_name_prefixes; - delete g_fresh_name_prefixes_guard; + delete g_fresh; } } diff --git a/src/util/fresh_name.h b/src/util/fresh_name.h index 0e771dfec5..9556571074 100644 --- a/src/util/fresh_name.h +++ b/src/util/fresh_name.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "util/name.h" +#include "util/name_generator.h" namespace lean { /** \brief Create a unique fresh name. This operation is thread-safe, and it guarantees the names are unique @@ -24,6 +25,26 @@ optional get_tagged_name_suffix(name const & n, name const & tag); bool is_fresh_name(name const & n); name sanitize_if_fresh(name const & n); +/* Return a snapshot of the thread local name_generator for fresh names. + We use this operation to save the state of the fresh name_generator in the parser snapshots. */ +name_generator get_fresh_name_generator_snapshot(); + +/* Set the thread local name_generator. + + We use this operation: + 1- to restore the state of the fresh name_generator when we restore parser snapshots. + 2- to set the fresh name_generator for a task. + + \pre \c g must have been created using `get_fresh_name_generator_snapshot` or `mk_fresh_name_generator_child`. +*/ +void set_fresh_name_generator(name_generator const & g); + +/* Create a new name_generator that does not create names that may conflict with names + generated by the current thread local fresh name_generator. + + We use this operation to set the name_generator before we execute a task. */ +name_generator mk_fresh_name_generator_child(); + void initialize_fresh_name(); void finalize_fresh_name(); } diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp index 56703a8f0b..c2b44f349f 100644 --- a/src/util/init_module.cpp +++ b/src/util/init_module.cpp @@ -19,10 +19,12 @@ void initialize_util_module() { initialize_thread(); initialize_ascii(); initialize_name(); + initialize_name_generator(); initialize_fresh_name(); } void finalize_util_module() { finalize_fresh_name(); + finalize_name_generator(); finalize_name(); finalize_ascii(); finalize_thread(); diff --git a/src/util/task.h b/src/util/task.h index 7a92cbffbb..c42b4ba8f7 100644 --- a/src/util/task.h +++ b/src/util/task.h @@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ #pragma once +#include #include "util/buffer.h" #include "util/thread.h" #include "util/cancellable.h" -#include +#include "util/fresh_name.h" namespace lean { @@ -61,13 +62,19 @@ class gtask_cell : public cancellable { virtual void execute() {}; - gtask_cell(task_state state) : m_state(state) {} - atomic m_state; std::unique_ptr m_data; std::exception_ptr m_exception; + name_generator m_name_gen; - gtask_cell(gtask_imp * imp, task_flags flags) : m_state(task_state::Created) { + gtask_cell(task_state state) : + m_state(state), + m_name_gen(mk_fresh_name_generator_child()) { + } + + gtask_cell(gtask_imp * imp, task_flags flags) : + m_state(task_state::Created), + m_name_gen(mk_fresh_name_generator_child()) { m_data.reset(new gtask_data(imp, flags)); } @@ -79,6 +86,8 @@ public: bool peek_is_finished() const { return m_state.load() > task_state::Running; } std::exception_ptr peek_exception() const; + name_generator const & get_name_generator() const { return m_name_gen; } + virtual ~gtask_cell() {} };