From ea8e1075d2f6d8410ce80e7e8fd030bc4f46ff43 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Aug 2018 09:40:56 -0700 Subject: [PATCH] feat(runtime/thunk): add runtime support for thunks We did not use constructor objects for implementing thunks because we wanted to use `atomic` to implement the cached result. --- src/runtime/object.cpp | 8 ++++ src/runtime/object.h | 34 ++++++++++++++- src/tests/util/CMakeLists.txt | 3 ++ src/tests/util/object.cpp | 78 +++++++++++++++++++++++++++++++++++ 4 files changed, 122 insertions(+), 1 deletion(-) create mode 100644 src/tests/util/object.cpp diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 0558174529..542bdb59f4 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include "runtime/object.h" #include "runtime/utf8.h" +#include "runtime/apply.h" namespace lean { size_t obj_byte_size(object * o) { @@ -19,6 +20,7 @@ size_t obj_byte_size(object * o) { case object_kind::ScalarArray: return sarray_byte_size(o); case object_kind::String: return string_byte_size(o); case object_kind::MPZ: return sizeof(mpz_object); + case object_kind::Thunk: return sizeof(thunk_object); case object_kind::External: lean_unreachable(); } lean_unreachable(); @@ -32,6 +34,7 @@ size_t obj_header_size(object * o) { case object_kind::ScalarArray: return sizeof(sarray_object); case object_kind::String: return sizeof(string_object); case object_kind::MPZ: return sizeof(mpz_object); + case object_kind::Thunk: return sizeof(thunk_object); case object_kind::External: lean_unreachable(); } lean_unreachable(); @@ -99,6 +102,11 @@ void del(object * o) { free(o); break; case object_kind::MPZ: dealloc_mpz(o); break; + case object_kind::Thunk: + dec_ref(to_thunk(o)->m_closure, todo); + if (object * v = to_thunk(o)->m_value) dec_ref(v, todo); + free(o); + break; case object_kind::External: dealloc_external(o); break; } diff --git a/src/runtime/object.h b/src/runtime/object.h index b00c14c2a8..dbf2716fbb 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -24,7 +24,7 @@ inline void * alloca(size_t s) { #endif } -enum class object_kind { Constructor, Closure, Array, ScalarArray, String, MPZ, External }; +enum class object_kind { Constructor, Closure, Array, ScalarArray, String, MPZ, Thunk, External }; /* The reference counter is a uintptr_t, because at deletion time, we use this field to implement a linked list of objects to be deleted. */ @@ -108,6 +108,12 @@ struct mpz_object : public object { object(object_kind::MPZ), m_value(v) {} }; +struct thunk_object : public object { + object * m_closure; + atomic m_value; + thunk_object(object * c); +}; + /* Base class for wrapping external_object data. For example, we use it to wrap the Lean environment object. */ struct external_object : public object { @@ -153,6 +159,7 @@ inline bool is_array(object * o) { return get_kind(o) == object_kind::Array; } inline bool is_sarray(object * o) { return get_kind(o) == object_kind::ScalarArray; } inline bool is_string(object * o) { return get_kind(o) == object_kind::String; } inline bool is_mpz(object * o) { return get_kind(o) == object_kind::MPZ; } +inline bool is_thunk(object * o) { return get_kind(o) == object_kind::Thunk; } inline bool is_external(object * o) { return get_kind(o) == object_kind::External; } /* Casting */ @@ -162,6 +169,7 @@ inline array_object * to_array(object * o) { lean_assert(is_array(o)); return st inline sarray_object * to_sarray(object * o) { lean_assert(is_sarray(o)); return static_cast(o); } inline string_object * to_string(object * o) { lean_assert(is_string(o)); return static_cast(o); } inline mpz_object * to_mpz(object * o) { lean_assert(is_mpz(o)); return static_cast(o); } +inline thunk_object * to_thunk(object * o) { lean_assert(is_thunk(o)); return static_cast(o); } inline external_object * to_external(object * o) { lean_assert(is_external(o)); return static_cast(o); } /* The memory associated with all Lean objects but `mpz_object` and `external_object` can be deallocated using `free`. @@ -320,6 +328,30 @@ inline void sarray_set_size(object * o, size_t sz) { inline object * alloc_mpz(mpz const & m) { return new mpz_object(m); } inline mpz const & mpz_value(object * o) { return to_mpz(o)->m_value; } +/* Thunks */ + +inline thunk_object::thunk_object(object * c): + object(object_kind::Thunk), m_closure(c), m_value(nullptr) { + /* Remark: the implementation relies on the fact that nullptr is not a valid lean object. */ + lean_assert(is_closure(c)); + inc_ref(c); +} + +inline object * alloc_thunk(object * c) { + return new (malloc(sizeof(thunk_object))) thunk_object(c); // NOLINT +} + +object * apply_1(object * f, object * a1); + +inline object * thunk_get(object * t) { + if (object * r = to_thunk(t)->m_value) + return r; + object * r = apply_1(to_thunk(t)->m_closure, box(0)); + lean_assert(r != nullptr); /* Closure must return a valid lean object */ + to_thunk(t)->m_value = r; + return r; +} + /* String */ inline object * alloc_string(size_t size, size_t capacity, size_t len) { return new (malloc(sizeof(string_object) + capacity)) string_object(size, capacity, len); // NOLINT diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 31466def78..ff722300eb 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -1,3 +1,6 @@ +add_executable(object object.cpp $ $) +target_link_libraries(object ${EXTRA_LIBS}) +add_exec_test(object "object") add_executable(name name.cpp $ $) target_link_libraries(name ${EXTRA_LIBS}) add_exec_test(name "name") diff --git a/src/tests/util/object.cpp b/src/tests/util/object.cpp new file mode 100644 index 0000000000..ff5fe9d4b0 --- /dev/null +++ b/src/tests/util/object.cpp @@ -0,0 +1,78 @@ +/* +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 +#include "util/test.h" +#include "util/object_ref.h" +#include "util/init_module.h" +using namespace lean; + +object * f(object *) { + std::cout << "executing f...\n"; + return box(10); +} + +static void tst1() { + object_ref c(alloc_closure(f, 1, 0)); + object_ref t(alloc_thunk(c.raw())); + object * r1 = thunk_get(t.raw()); + object * r2 = thunk_get(t.raw()); + std::cout << "thunk value: " << unbox(r1) << "\n"; + std::cout << "thunk value: " << unbox(r2) << "\n"; +} + +static unsigned g_g_counter = 0; + +object * g(object *) { + g_g_counter++; + return box(g_g_counter); +} + +static void tst2() { + object_ref c(alloc_closure(g, 1, 0)); + object * r1 = apply_1(c.raw(), box(0)); + object * r2 = apply_1(c.raw(), box(0)); + lean_assert(unbox(r1) == 1); + lean_assert(unbox(r2) == 2); + object_ref t(alloc_thunk(c.raw())); + object * r3 = thunk_get(t.raw()); + object * r4 = thunk_get(t.raw()); + lean_assert(unbox(r3) == 3); + lean_assert(unbox(r4) == 3); +} + +static unsigned g_h_counter = 0; + +object * h(object *) { + g_h_counter++; + return box(0); +} + +/* Make sure box(0) is not mistaken by cached value has not been initialized yet. + + The thunk implementation relies on the fact that nullptr is not a scalar nor a valid + Lean object. */ +static void tst3() { + object_ref c(alloc_closure(h, 1, 0)); + object_ref t(alloc_thunk(c.raw())); + lean_assert(g_h_counter == 0); + object * r3 = thunk_get(t.raw()); + lean_assert(g_h_counter == 1); + object * r4 = thunk_get(t.raw()); + lean_assert(g_h_counter == 1); + lean_assert(unbox(r3) == 0); + lean_assert(unbox(r4) == 0); +} + +int main() { + save_stack_info(); + initialize_util_module(); + tst1(); + tst2(); + tst3(); + finalize_util_module(); + return has_violations() ? 1 : 0; +}