diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 660ffc9734..0ada5be218 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -94,6 +94,23 @@ inline void dec(object * o, object* & todo) { void deactivate_task(task_object * t); +static size_t parray_data_capacity(object ** data) { + return reinterpret_cast(data)[-1]; +} + +static object ** alloc_parray_data(size_t c) { + size_t * mem = static_cast(malloc(sizeof(object*)*c + sizeof(size_t))); + *mem = c; + mem++; + return reinterpret_cast(mem); +} + +static void dealloc_parray_data(object ** data) { + size_t * mem = reinterpret_cast(data); + mem--; + free(mem); +} + void del(object * o) { object * todo = nullptr; while (true) { @@ -148,7 +165,7 @@ void del(object * o) { object ** it = to_parray(o)->m_data; object ** end = it + to_parray(o)->m_size; for (; it != end; ++it) dec(*it, todo); - free(to_parray(o)->m_data); + dealloc_parray_data(to_parray(o)->m_data); free_heap_obj(o); break; } @@ -189,23 +206,6 @@ static object * sarray_ensure_capacity(object * o, size_t extra) { // ======================================= // Persistent arrays -static size_t parray_data_capacity(object ** data) { - return reinterpret_cast(data)[-1]; -} - -static object ** alloc_parray_data(size_t c) { - size_t * mem = static_cast(malloc(sizeof(object*)*c + sizeof(size_t))); - *mem = c; - mem++; - return reinterpret_cast(mem); -} - -static void dealloc_parray_data(object ** data) { - size_t * mem = reinterpret_cast(data); - mem--; - free(mem); -} - static object ** parray_data_expand(object ** data, size_t sz) { size_t curr_capacity = parray_data_capacity(data); size_t new_capacity = curr_capacity == 0 ? 2 : (3 * curr_capacity + 1) >> 1; @@ -234,6 +234,7 @@ static void parray_reroot(object * c) { lean_assert(prev != nullptr); lean_assert(get_kind(it) == object_kind::PArrayRoot); lean_assert(it != c); + object * old_root = it; it->m_next = prev; object ** data = it->m_data; size_t sz = it->m_size; @@ -273,10 +274,14 @@ static void parray_reroot(object * c) { it->m_kind = static_cast(object_kind::PArrayRoot); it->m_data = data; it->m_size = sz; + dec_ref(old_root); + inc_ref(c); } static parray_object * move_parray_root(parray_object * src) { lean_assert(src->m_kind == static_cast(object_kind::PArrayRoot)); + lean_assert(get_rc(src) > 1); + dec_ref(src); parray_object * r = new (alloc_heap_object(sizeof(parray_object))) parray_object(); r->m_data = src->m_data; r->m_size = src->m_size; diff --git a/src/tests/util/object.cpp b/src/tests/util/object.cpp index af98f8c749..b0a8d8f12a 100644 --- a/src/tests/util/object.cpp +++ b/src/tests/util/object.cpp @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include #include #include #include "util/test.h" @@ -402,6 +404,8 @@ void tst14() { lean_assert(get_rc(b) == 2); a = parray_set(a, 0, box(1)); lean_assert(a != b); + lean_assert(get_rc(b) == 1); + lean_assert(get_rc(a) == 2); lean_assert(parray_get(a, 0) == box(1)); lean_assert(parray_get(a, 1) == box(0)); lean_assert(parray_get(b, 0) == box(0)); @@ -416,7 +420,9 @@ void tst14() { lean_assert(parray_get(c, 10) == box(20)); lean_assert(parray_get(a, 0) == box(1)); lean_assert(parray_get(b, 0) == box(0)); - dec(a); dec(b); dec(c); + dec_ref(a); dec_ref(b); + lean_assert(get_rc(c) == 1); + dec_ref(c); } obj_res mk_foo(unsigned n) { @@ -450,13 +456,88 @@ void tst15() { v1 = parray_pop(v1); lean_assert(parray_size(v1) == 10); lean_assert(parray_size(v3) == 12); - dec(v1); dec(v2); dec(v3); + dec_ref(v1); dec_ref(v2); + lean_assert(get_rc(v3) == 1); + dec_ref(v3); +} + +void driver(unsigned max_sz, unsigned max_val, unsigned num_it, + double push_freq, + double pop_freq, + double set_freq, + double copy_freq) { + object * v1 = alloc_parray(0); + std::vector v2; + std::mt19937 rng; + rng.seed(static_cast(time(0))); + std::uniform_int_distribution uint_dist; + std::vector>> copies; + lean_assert(get_rc(v1) == 1); + size_t acc_sz = 0; + for (unsigned i = 0; i < num_it; i++) { + acc_sz += parray_size(v1); + double f = static_cast(uint_dist(rng) % 10000) / 10000.0; + if (f < copy_freq) { + inc_ref(v1); + copies.emplace_back(v1, v2); + } + f = static_cast(uint_dist(rng) % 10000) / 10000.0; + if (f < push_freq) { + if (parray_size(v1) < max_sz) { + unsigned a = uint_dist(rng) % max_val; + v1 = parray_push(v1, box(a)); + v2.push_back(a); + } + } + if (parray_size(v1) > 0) { + f = static_cast(uint_dist(rng) % 10000) / 10000.0; + if (f < pop_freq) { + v1 = parray_pop(v1); + v2.pop_back(); + } + } + if (parray_size(v1) > 0) { + f = static_cast(uint_dist(rng) % 10000) / 10000.0; + if (f < set_freq) { + unsigned idx = uint_dist(rng) % parray_size(v1); + unsigned a = uint_dist(rng) % max_val; + v1 = parray_set(v1, idx, box(a)); + v2[idx] = a; + } + } + f = static_cast(uint_dist(rng) % 10000) / 10000.0; + lean_assert(parray_size(v1) == v2.size()); + for (unsigned i = 0; i < v2.size(); i++) { + lean_assert(unbox(parray_get(v1, i)) == v2[i]); + } + } + for (std::pair> const & p : copies) { + lean_assert(parray_size(p.first) == p.second.size()); + for (unsigned i = 0; i < p.second.size(); i++) { + lean_assert(unbox(parray_get(p.first, i)) == p.second[i]); + } + dec_ref(p.first); + } + std::cout << "\n"; + std::cout << "Copies created: " << copies.size() << "\n"; + std::cout << "Average size: " << static_cast(acc_sz) / static_cast(num_it) << "\n"; + lean_assert(get_rc(v1) == 1); + dec_ref(v1); +} + +static void tst16() { + driver(4, 32, 10000, 0.5, 0.1, 0.5, 0.1); + driver(4, 32, 10000, 0.5, 0.1, 0.5, 0.1); + driver(4, 32, 10000, 0.5, 0.1, 0.5, 0.5); + driver(16, 16, 100000, 0.5, 0.5, 0.5, 0.01); + driver(16, 16, 100000, 0.5, 0.1, 0.5, 0.01); + driver(16, 16, 100000, 0.5, 0.6, 0.5, 0.01); + driver(16, 16, 10000, 0.5, 0.1, 0.5, 0.0); } int main() { save_stack_info(); initialize_util_module(); -#if 0 tst1(); tst2(); tst3(); @@ -470,9 +551,9 @@ int main() { tst11(); tst12(); tst13(); -#endif tst14(); tst15(); + tst16(); finalize_util_module(); return has_violations() ? 1 : 0; }