From 1b4c9f63cecb3c9f27fa336ed36e6aaf66d0020c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 May 2014 22:25:54 -0700 Subject: [PATCH] perf(kernel/environment): improve is_descendant performance, optimize for the common case: the is_descendant tree is huge but has few deep branches This is an important optimization for module.cpp. The benchmark tests/lua/slow/mod2.lua is a good example where the cost of is_descendant was neutralizing the benefit of the replace method. Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 50 +++++++++++++++++--- src/kernel/environment.h | 15 ++++-- src/tests/kernel/environment.cpp | 78 ++++++++++++++++++++++++++++++++ 3 files changed, 132 insertions(+), 11 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index ea3952b10..ab7ead794 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/thread.h" #include "kernel/environment.h" #include "kernel/kernel_exception.h" @@ -28,18 +29,53 @@ environment_header::environment_header(unsigned trust_lvl, bool prop_proof_irrel environment_extension::~environment_extension() {} -environment_id::environment_id():m_trail(0, list()) {} +struct environment_id::path { + unsigned m_next_depth; + unsigned m_start_depth; + mutex m_mutex; + path * m_prev; + MK_LEAN_RC(); // Declare m_rc counter + void dealloc() { delete this; } -environment_id::environment_id(environment_id const & ancestor, bool):m_trail(car(ancestor.m_trail) + 1, ancestor.m_trail) {} + path():m_next_depth(1), m_start_depth(0), m_prev(nullptr), m_rc(1) {} + path(unsigned start_depth, path * prev):m_next_depth(start_depth + 1), m_start_depth(start_depth), m_prev(prev), m_rc(1) { + if (prev) prev->inc_ref(); + } + ~path() { if (m_prev) m_prev->dec_ref(); } +}; +environment_id::environment_id():m_ptr(new path()), m_depth(0) {} +environment_id::environment_id(environment_id const & ancestor, bool) { + if (ancestor.m_depth == std::numeric_limits::max()) + throw exception("maximal depth in is_descendant tree has been reached, use 'forget' method to workaround this limitation"); + unique_lock lock(ancestor.m_ptr->m_mutex); + if (ancestor.m_ptr->m_next_depth == ancestor.m_depth + 1) { + m_ptr = ancestor.m_ptr; + m_depth = ancestor.m_depth + 1; + m_ptr->m_next_depth++; + m_ptr->inc_ref(); + } else { + m_ptr = new path(ancestor.m_depth+1, ancestor.m_ptr); + m_depth = ancestor.m_depth + 1; + } + lean_assert(m_depth == ancestor.m_depth+1); + lean_assert(m_ptr->m_next_depth == m_depth+1); +} +environment_id::environment_id(environment_id const & id):m_ptr(id.m_ptr), m_depth(id.m_depth) { if (m_ptr) m_ptr->inc_ref(); } +environment_id::environment_id(environment_id && id):m_ptr(id.m_ptr), m_depth(id.m_depth) { id.m_ptr = nullptr; } +environment_id::~environment_id() { if (m_ptr) m_ptr->dec_ref(); } +environment_id & environment_id::operator=(environment_id const & s) { m_depth = s.m_depth; LEAN_COPY_REF(s); } +environment_id & environment_id::operator=(environment_id && s) { m_depth = s.m_depth; LEAN_MOVE_REF(s); } bool environment_id::is_descendant(environment_id const & id) const { - list const * it = &m_trail; - while (!is_nil(*it)) { - if (is_eqp(*it, id.m_trail)) + if (m_depth < id.m_depth) + return false; + path * p = m_ptr; + while (p != nullptr) { + if (p == id.m_ptr) return true; - if (car(*it) < car(id.m_trail)) + if (p->m_start_depth <= id.m_depth) return false; - it = &cdr(*it); + p = p->m_prev; } return false; } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index c41e4ae9c..260448532 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -74,12 +74,13 @@ public: typedef std::vector> environment_extensions; -/** - \brief environment identifier that allows us to track descendants of a given environment. -*/ +/** \brief environment identifier for tracking descendants of a given environment. */ class environment_id { + friend class environment_id_tester; friend class environment; // Only the environment class can create object of this type. - list m_trail; //!< trail of ancestors. The unsigned value is redundant, it store the depth of the trail. + struct path; + path * m_ptr; + unsigned m_depth; /** \brief Create an identifier for an environment that is a direct descendant of the given one. The bool field is just to make sure this constructor is not confused with a copy constructor @@ -90,6 +91,12 @@ class environment_id { /** Create an identifier for an environment that is a direct descendant of the given one. */ static environment_id mk_descendant(environment_id const & ancestor) { return environment_id(ancestor, true); } public: + environment_id(environment_id const & id); + environment_id(environment_id && id); + ~environment_id(); + environment_id & operator=(environment_id const & s); + environment_id & operator=(environment_id && s); + /** \brief Return true iff this object is a descendant of the given one. */ bool is_descendant(environment_id const & id) const; }; diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index db86c428a..d95f252b9 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/test.h" #include "util/exception.h" #include "util/trace.h" @@ -158,11 +159,88 @@ static void tst4() { } } +namespace lean { +class environment_id_tester { +public: + static void tst1() { + environment_id id1; + environment_id id2 = environment_id::mk_descendant(id1); + environment_id id3 = environment_id::mk_descendant(id2); + environment_id id4 = environment_id::mk_descendant(id1); + environment_id id5 = environment_id::mk_descendant(id3); + environment_id id6 = environment_id::mk_descendant(id4); + environment_id id7 = environment_id::mk_descendant(id3); + environment_id id8 = environment_id::mk_descendant(id7); + lean_assert(id1.is_descendant(id1)); + lean_assert(id2.is_descendant(id1)); + lean_assert(!id1.is_descendant(id2)); + lean_assert(id3.is_descendant(id1)); + lean_assert(id3.is_descendant(id2)); + lean_assert(id4.is_descendant(id1)); + lean_assert(!id4.is_descendant(id2)); + lean_assert(!id4.is_descendant(id3)); + lean_assert(id5.is_descendant(id3)); + lean_assert(!id5.is_descendant(id4)); + lean_assert(id6.is_descendant(id4)); + lean_assert(!id6.is_descendant(id5)); + lean_assert(id5.is_descendant(id1)); + lean_assert(id6.is_descendant(id1)); + lean_assert(id7.is_descendant(id3)); + lean_assert(id7.is_descendant(id2)); + lean_assert(id7.is_descendant(id1)); + lean_assert(!id7.is_descendant(id4)); + lean_assert(!id7.is_descendant(id5)); + lean_assert(!id7.is_descendant(id6)); + lean_assert(id8.is_descendant(id7)); + lean_assert(id8.is_descendant(id3)); + lean_assert(id8.is_descendant(id2)); + lean_assert(id8.is_descendant(id1)); + lean_assert(!id8.is_descendant(id4)); + lean_assert(!id8.is_descendant(id5)); + lean_assert(!id8.is_descendant(id6)); + } + + static void tst2() { + constexpr unsigned num_paths = 50; + constexpr unsigned path_len = 100; + std::vector ids[num_paths]; + for (unsigned i = 0; i < num_paths; i++) { + if (i == 0) + ids[i].push_back(environment_id()); + else + ids[i].push_back(environment_id::mk_descendant(ids[i-1][1])); + for (unsigned j = 0; j < path_len; j++) { + ids[i].push_back(environment_id::mk_descendant(ids[i].back())); + } + } + for (unsigned i = 0; i < num_paths; i++) { + for (unsigned j = 0; j < path_len; j++) { + for (unsigned k = 0; k < i; k++) { + lean_assert(ids[i][j].is_descendant(ids[k][1])); + lean_assert(ids[i][j].is_descendant(ids[k][0])); + lean_assert(!ids[k][1].is_descendant(ids[i][j])); + lean_assert(!ids[k][0].is_descendant(ids[i][j])); + for (unsigned s = 2; s < path_len; s++) { + lean_assert(!ids[i][j].is_descendant(ids[k][s])); + } + } + for (unsigned k = 0; k < j; k++) { + lean_assert(ids[i][j].is_descendant(ids[i][k])); + lean_assert(!ids[i][k].is_descendant(ids[i][j])); + } + } + } + } +}; +} + int main() { save_stack_info(); tst1(); tst2(); tst3(); tst4(); + environment_id_tester::tst1(); + environment_id_tester::tst2(); return has_violations() ? 1 : 0; }