From 35cf7bf8e25a543f80cc58485ccc1345492eceb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 May 2016 11:00:33 -0700 Subject: [PATCH] feat(library/vm/vm): remove atomic from VM object reference counter VM objects should not be shared between different threads. So, the atomic in the reference counter produces an unnecessary performance penalty. --- src/library/vm/vm.h | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index ea2877d060..9123fc40f1 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -21,13 +21,22 @@ enum class vm_obj_kind { Simple, Constructor, Closure, MPZ, External }; \remark Simple objects are encoded as tagged pointers. */ class vm_obj_cell { protected: - MK_LEAN_RC(); // Declare m_rc counter + friend class vm_obj; + unsigned m_rc; vm_obj_kind m_kind; + void inc_ref() { m_rc++; } + bool dec_ref_core() { + lean_assert(m_rc > 0); + m_rc--; + return m_rc == 0; + } + void dec_ref() { if (dec_ref_core()) { dealloc(); } } void dealloc(); void dec_ref(vm_obj & o, buffer & todelete); vm_obj_cell(vm_obj_kind k):m_rc(0), m_kind(k) {} public: vm_obj_kind kind() const { return m_kind; } + unsigned get_rc() const { return m_rc; } }; #define LEAN_VM_IS_PTR(obj) ((reinterpret_cast(obj) & 1) == 0)