max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/vm/vm): remove atomic from VM object reference counter

Browse source 
VM objects should not be shared between different threads.
So, the atomic<unsigned> in the reference counter produces an
unnecessary performance penalty.
This commit is contained in:
Leonardo de Moura 2016-05-13 11:00:33 -07:00
parent 2bd400964c
commit 35cf7bf8e2
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/vm/vm.h
View file

@ -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<vm_obj_cell*> & 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<size_t>(obj) & 1) == 0)