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

feat(runtime/object): given mk_task(o), mark objects reachable from o as MTHeap

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-17 10:29:04 -08:00
parent d100f95469
commit 827021a6c5
2 changed files with 94 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

58
src/runtime/object.cpp
View file

@ -777,10 +777,68 @@ static task_object * alloc_task(obj_arg v) {
return new (alloc_heap_object(sizeof(task_object))) task_object(v); // NOLINT
}
void to_mt(object * o);
static obj_res to_mt_fn(obj_arg o) {
to_mt(o);
dec(o);
return box(0);
}
void to_mt(object * o) {
if (is_scalar(o) || !is_st_heap_obj(o)) return;
o->m_mem_kind = static_cast<unsigned>(object_memory_kind::MTHeap);
switch (get_kind(o)) {
case object_kind::ScalarArray:
case object_kind::String:
case object_kind::MPZ:
return;
case object_kind::PArrayPop:
case object_kind::PArrayPush:
case object_kind::PArraySet:
case object_kind::PArrayRoot:
/* `to_mt` cannot be used with parray. They must be copied when used in multiple threads. */
lean_unreachable();
return;
case object_kind::External: {
object * fn = alloc_closure(reinterpret_cast<void*>(to_mt_fn), 1, 0);
to_external(o)->for_each_nested(fn);
dec(fn);
return;
}
case object_kind::Task:
to_mt(task_get(o));
return;
case object_kind::Constructor: {
object ** it = cnstr_obj_cptr(o);
object ** end = it + cnstr_num_objs(o);
for (; it != end; ++it) to_mt(*it);
break;
}
case object_kind::Closure: {
object ** it = closure_arg_cptr(o);
object ** end = it + closure_num_fixed(o);
for (; it != end; ++it) to_mt(*it);
break;
}
case object_kind::Array: {
object ** it = array_cptr(o);
object ** end = it + array_size(o);
for (; it != end; ++it) to_mt(*it);
break;
}
case object_kind::Thunk:
if (object * c = to_thunk(o)->m_closure) to_mt(c);
if (object * v = to_thunk(o)->m_value) to_mt(v);
break;
}
}
obj_res mk_task(obj_arg c, unsigned prio) {
if (!g_task_manager) {
return mk_thunk(c);
} else {
to_mt(c);
task_object * new_task = alloc_task(c, prio);
g_task_manager->enqueue(new_task);
return new_task;

69
src/runtime/object.h
View file

@ -77,6 +77,38 @@ struct constructor_object : public object {
object(object_kind::Constructor, m), m_tag(tag), m_num_objs(num_objs), m_scalar_size(scalar_sz) {}
};
/*
In our runtime, a Lean function consume the reference counter (RC) of its argument or not.
We say this behavior is part of the "calling convention" for the function. We say an argument uses:
1- "standard" calling convention if it consumes/decrements the RC.
In this calling convention each argument should be viewed as a resource that is consumed by the function.
This is roughly equivalent to `S && a` in C++, where `S` is a smart pointer, and `a` is the argument.
When this calling convention is used for an argument `x`, then it is safe to perform destructive updates to
`x` if its RC is 1.
2- "borrowed" calling convention if it doesn't consume/decrement the RC, and it is the responsability of the caller
to decrement the RC.
This is roughly equivalent to `S const & a` in C++, where `S` is a smart pointer, and `a` is the argument.
For returning objects, we also have two conventions
1- "standard" result. The caller is responsible for consuming the RC of the result.
This is roughly equivalent to returning a smart point `S` by value in C++.
2- "borrowed" result. The caller is not responsible for decreasing the RC.
This is roughly equivalent to returning a smart point reference `S const &` in C++.
Functions stored in closures use the "standard" calling convention.
*/
/* The following typedef's are used to document the calling convention for the primitives. */
typedef object * obj_arg; /* Standard object argument. */
typedef object * b_obj_arg; /* Borrowed object argument. */
typedef object * u_obj_arg; /* Unique (aka non shared) object argument. */
typedef object * obj_res; /* Standard object result. */
typedef object * b_obj_res; /* Borrowed object result. */
/* Array of objects.
Header size: 16 bytes in 32 bit machines and 32 bytes in 64 bit machines. */
struct array_object : public object {
@ -175,8 +207,11 @@ struct task_object : public object {
For example, we use it to wrap the Lean environment object. */
struct external_object : public object {
explicit external_object(object_memory_kind m = c_init_mem_kind): object(object_kind::External, m) {}
virtual void dealloc() {}
virtual ~external_object() {}
virtual void dealloc() {}
/* For each nested object `a`, execute `apply_1(fn, a)`.
Recall that apply_1 consumes the RC of `fn` and `a`. */
virtual void for_each_nested(b_obj_arg /* fn */) {}
};
inline bool is_null(object * o) { return o == nullptr; }
@ -473,38 +508,6 @@ bool int_big_eq(object * a1, object * a2);
bool int_big_le(object * a1, object * a2);
bool int_big_lt(object * a1, object * a2);
/*
In our runtime, a Lean function consume the reference counter (RC) of its argument or not.
We say this behavior is part of the "calling convention" for the function. We say an argument uses:
1- "standard" calling convention if it consumes/decrements the RC.
In this calling convention each argument should be viewed as a resource that is consumed by the function.
This is roughly equivalent to `S && a` in C++, where `S` is a smart pointer, and `a` is the argument.
When this calling convention is used for an argument `x`, then it is safe to perform destructive updates to
`x` if its RC is 1.
2- "borrowed" calling convention if it doesn't consume/decrement the RC, and it is the responsability of the caller
to decrement the RC.
This is roughly equivalent to `S const & a` in C++, where `S` is a smart pointer, and `a` is the argument.
For returning objects, we also have two conventions
1- "standard" result. The caller is responsible for consuming the RC of the result.
This is roughly equivalent to returning a smart point `S` by value in C++.
2- "borrowed" result. The caller is not responsible for decreasing the RC.
This is roughly equivalent to returning a smart point reference `S const &` in C++.
Functions stored in closures use the "standard" calling convention.
*/
/* The following typedef's are used to document the calling convention for the primitives. */
typedef object * obj_arg; /* Standard object argument. */
typedef object * b_obj_arg; /* Borrowed object argument. */
typedef object * u_obj_arg; /* Unique (aka non shared) object argument. */
typedef object * obj_res; /* Standard object result. */
typedef object * b_obj_res; /* Borrowed object result. */
// =======================================
// Constructor objects
inline obj_res alloc_cnstr(unsigned tag, unsigned num_objs, unsigned scalar_sz) {