From feea8ecccd58f78be99184f97d26e1b306661d99 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Feb 2019 20:17:15 -0800 Subject: [PATCH] feat(library/compiler/llnf): avoid inc/dec operations on persistent objects inc/dec operations are noop's for persistent objects. --- gen/apply.lean | 4 +- src/kernel/expr.h | 2 +- src/library/compiler/llnf.cpp | 90 ++++++++++++++++++++++------------- src/runtime/apply.cpp | 34 ++++++------- 4 files changed, 76 insertions(+), 54 deletions(-) diff --git a/gen/apply.lean b/gen/apply.lean index 51919b2560..37ff4045a4 100644 --- a/gen/apply.lean +++ b/gen/apply.lean @@ -51,7 +51,7 @@ do emit $ sformat! "obj* apply_{n}(obj* f, {arg_decls}) {{\n", emit "unsigned arity = closure_arity(f);\n", emit "unsigned fixed = closure_num_fixed(f);\n", emit $ sformat! "if (arity == fixed + {n}) {{\n", - emit $ sformat! " if (!is_shared(f)) {{\n", + emit $ sformat! " if (is_exclusive(f)) {{\n", emit $ sformat! " switch (arity) {{\n", max.mrepeat $ λ i, do { let j := i + 1, @@ -152,7 +152,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) { obj * r = alloc_closure(closure_fun(f), arity, new_fixed); obj ** source = closure_arg_cptr(f); obj ** target = closure_arg_cptr(r); - if (is_shared(f)) { + if (!is_exclusive(f)) { for (unsigned i = 0; i < fixed; i++, source++, target++) { *target = *source; inc(*target); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 1bbff6a00c..b7d5ed8c43 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -250,7 +250,7 @@ inline name const & let_name(expr const & e) { lean_assert(is_le inline expr const & let_type(expr const & e) { lean_assert(is_let(e)); return static_cast(cnstr_get_ref(e, 1)); } inline expr const & let_value(expr const & e) { lean_assert(is_let(e)); return static_cast(cnstr_get_ref(e, 2)); } inline expr const & let_body(expr const & e) { lean_assert(is_let(e)); return static_cast(cnstr_get_ref(e, 3)); } -inline bool is_shared(expr const & e) { return is_shared(e.raw()); } +inline bool is_shared(expr const & e) { return !is_exclusive(e.raw()); } // // ======================================= diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 8f934e292f..137c4ef4a1 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -1445,8 +1445,9 @@ class explicit_rc_fn { buffer m_fvars; name m_x; unsigned m_next_idx{1}; - name_set m_borrowed; /* Set of variables marked as borrowed. */ + name_set m_is_borrowed; /* Set of variables marked as borrowed. */ name_set m_is_scalar; /* Set of variables of type `_obj` that are known to be a boxed scalar value. */ + name_set m_is_persistent; static bool is_jmp(expr const & e) { return is_llnf_jmp(get_app_fn(e)); @@ -1474,10 +1475,28 @@ class explicit_rc_fn { return r; } - expr mk_let_decl(expr const & type, expr const & e) { - expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e); - m_fvars.push_back(fvar); - return fvar; + bool is_borrowed(name const & fvar) const { + return m_is_borrowed.contains(fvar); + } + + bool is_borrowed(expr const & fvar) const { + return is_borrowed(fvar_name(fvar)); + } + + bool is_boxed_scalar(name const & fvar) const { + return m_is_scalar.contains(fvar); + } + + bool is_boxed_scalar(expr const & fvar) const { + return is_boxed_scalar(fvar_name(fvar)); + } + + bool is_persistent(name const & fvar) const { + return m_is_persistent.contains(fvar); + } + + bool is_persistent(expr const & fvar) const { + return is_persistent(fvar_name(fvar)); } void collect_live_vars_core(expr e, name_set & visited_jp, name_set & r) { @@ -1604,7 +1623,7 @@ class explicit_rc_fn { lean_assert(args.size() == borrowed_args.size()); unsigned n = get_num_consumptions(arg, args, borrowed_args); if (n > 0) { /* arg is consumed by f at least once */ - if (m_borrowed.contains(fvar_name(arg)) || /* arg is marked as borrowed, that is, it does not need to be consumed */ + if (is_borrowed(arg) || /* arg is marked as borrowed, that is, it does not need to be consumed */ live_obj_vars.contains(fvar_name(arg)) || /* arg is alive after application */ is_borrowed_arg(arg, args, borrowed_args)) { /* arg is also borrowed by f */ /* We must add n increments */ @@ -1649,14 +1668,15 @@ class explicit_rc_fn { expr const & arg = args[i]; if (is_fvar(arg) && !is_unboxed(get_type_of(arg)) && /* it is not a unboxed/scalar value */ - !m_is_scalar.contains(fvar_name(arg)) && /* it is not known to be a scalar here */ + !is_persistent(arg) && + !is_boxed_scalar(arg) && /* it is not known to be a scalar here */ is_first_occur(arg, i, args)) { unsigned n = get_num_incs(arg, args, f_borrowed_args, live_obj_vars); if (n > 0) { incs.emplace_back(arg, n); } /* Check if we need to add a decrement. */ - if (!m_borrowed.contains(fvar_name(arg)) && /* arg is not marked as borrowed */ + if (!is_borrowed(arg) && /* arg is not marked as borrowed */ !live_obj_vars.contains(fvar_name(arg)) && /* arg is not live after the f-application */ is_borrowed_arg(arg, args, f_borrowed_args)) { /* arg has been borrowed by f */ /* We must add 1 decrement. */ @@ -1711,7 +1731,7 @@ class explicit_rc_fn { expr val = get_value_of(x); lean_assert(is_app(val) && is_llnf_proj(app_fn(val))); expr arg = app_arg(val); - if (!m_borrowed.contains(fvar_name(arg)) && /* arg is not marked as borrowed */ + if (!is_borrowed(arg) && /* arg is not marked as borrowed */ !live_obj_vars.contains(fvar_name(arg))) { /* arg is not live after projection */ /* We must add decrement. */ add_dec(arg, entries); @@ -1773,7 +1793,8 @@ class explicit_rc_fn { expr const & arg = args[i]; if (is_fvar(arg) && !is_unboxed(get_type_of(arg)) && /* it is not a unboxed/scalar value */ - !m_is_scalar.contains(fvar_name(arg)) && + !is_persistent(arg) && + !is_boxed_scalar(arg) && is_first_occur(arg, i, args)) { unsigned n = get_num_incs(arg, args, borrowed_args, name_set()); if (n > 0) { @@ -1830,8 +1851,9 @@ class explicit_rc_fn { /* We must decrement (non-borrowed) variables that are live at `cases_live_vars`, but are not live at `arg_live_vars`. */ cases_live_vars.for_each([&](name const & x_name) { if (!arg_live_vars.contains(x_name) && - !m_is_scalar.contains(x_name) && - !m_borrowed.contains(x_name)) { + !is_persistent(x_name) && + !is_boxed_scalar(x_name) && + !is_borrowed(x_name)) { local_decl x_decl = m_lctx.get_local_decl(x_name); if (!is_unboxed(x_decl.get_type())) { expr x = x_decl.mk_ref(); @@ -1858,8 +1880,9 @@ class explicit_rc_fn { return e; } else if (is_fvar(e)) { /* If it is marked as borrowed, we should insert `inc`. */ - if (m_borrowed.contains(fvar_name(e)) && is_obj(e) && - !m_is_scalar.contains(fvar_name(e))) { + if (is_borrowed(e) && is_obj(e) && + !is_persistent(e) && + !is_boxed_scalar(e)) { add_inc(e, entries); } return e; @@ -1935,7 +1958,7 @@ class explicit_rc_fn { expr new_fvar = m_lctx.mk_local_decl(ngen(), next_name(), binding_domain(e), binding_info(e)); lean_assert(i < borrowed.size()); if (borrowed[i]) - m_borrowed.insert(fvar_name(new_fvar)); + m_is_borrowed.insert(fvar_name(new_fvar)); binding_fvars.push_back(new_fvar); e = binding_body(e); i++; @@ -1963,7 +1986,7 @@ class explicit_rc_fn { if (is_lit(val)) { return false; } else if (is_constant(val)) { - return !is_llnf_cnstr(val); + return false; } else if (is_app(val)) { buffer args; expr const & fn = get_app_args(val, args); @@ -2000,20 +2023,27 @@ class explicit_rc_fn { lit_value(e).get_nat() <= LEAN_MAX_SMALL_NAT); } + expr mk_fvar(name const & n, expr const & type, expr const & val) { + expr new_fvar = m_lctx.mk_local_decl(ngen(), n, type, val); + m_fvars.push_back(new_fvar); + if (should_mark_as_borrowed(val)) { + m_is_borrowed.insert(fvar_name(new_fvar)); + } + if (is_boxed_scalar(type, val)) { + m_is_scalar.insert(fvar_name(new_fvar)); + } + if (is_constant(val) && !is_llnf_cnstr(val)) { + m_is_persistent.insert(fvar_name(new_fvar)); + } + return new_fvar; + } + /* Make sure `e` is a cases, jmp or fvar */ expr ensure_terminal(expr const & e) { if (!is_cases_on_app(env(), e) && !is_jmp(e) && !is_fvar(e)) { /* ensure that `e` is a cases, jmp or fvar */ expr type = ll_infer_type(m_env, m_lctx, e); - expr new_fvar = m_lctx.mk_local_decl(ngen(), "_res", type, e); - if (should_mark_as_borrowed(e)) { - m_borrowed.insert(fvar_name(new_fvar)); - } - if (is_boxed_scalar(type, e)) { - m_is_scalar.insert(fvar_name(new_fvar)); - } - m_fvars.push_back(new_fvar); - return new_fvar; + return mk_fvar("_res", type, e); } else { return e; } @@ -2033,16 +2063,8 @@ class explicit_rc_fn { n = next_name(); } expr type = let_type(e); - expr new_fvar = m_lctx.mk_local_decl(ngen(), n, type, val); - if (should_mark_as_borrowed(val)) { - /* Remark: it is incorrect to mark it at `process`. */ - m_borrowed.insert(fvar_name(new_fvar)); - } - if (is_boxed_scalar(type, val)) { - m_is_scalar.insert(fvar_name(new_fvar)); - } + expr new_fvar = mk_fvar(n, type, val); fvars.push_back(new_fvar); - m_fvars.push_back(new_fvar); } e = let_body(e); } diff --git a/src/runtime/apply.cpp b/src/runtime/apply.cpp index f2f111ebdf..e6dc9c8d1f 100644 --- a/src/runtime/apply.cpp +++ b/src/runtime/apply.cpp @@ -19,7 +19,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) { obj * r = alloc_closure(closure_fun(f), arity, new_fixed); obj ** source = closure_arg_cptr(f); obj ** target = closure_arg_cptr(r); - if (is_shared(f)) { + if (!is_exclusive(f)) { for (unsigned i = 0; i < fixed; i++, source++, target++) { *target = *source; inc(*target); @@ -101,7 +101,7 @@ obj* apply_1(obj* f, obj* a1) { unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 1) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 1: { obj* r = FN1(f)(a1); free_heap_obj(f); return r; } case 2: { obj* r = FN2(f)(fx(0), a1); free_heap_obj(f); return r; } @@ -159,7 +159,7 @@ obj* apply_2(obj* f, obj* a1, obj* a2) { unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 2) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 2: { obj* r = FN2(f)(a1, a2); free_heap_obj(f); return r; } case 3: { obj* r = FN3(f)(fx(0), a1, a2); free_heap_obj(f); return r; } @@ -220,7 +220,7 @@ obj* apply_3(obj* f, obj* a1, obj* a2, obj* a3) { unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 3) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 3: { obj* r = FN3(f)(a1, a2, a3); free_heap_obj(f); return r; } case 4: { obj* r = FN4(f)(fx(0), a1, a2, a3); free_heap_obj(f); return r; } @@ -279,7 +279,7 @@ obj* apply_4(obj* f, obj* a1, obj* a2, obj* a3, obj* a4) { unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 4) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 4: { obj* r = FN4(f)(a1, a2, a3, a4); free_heap_obj(f); return r; } case 5: { obj* r = FN5(f)(fx(0), a1, a2, a3, a4); free_heap_obj(f); return r; } @@ -336,7 +336,7 @@ obj* apply_5(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5) { unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 5) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 5: { obj* r = FN5(f)(a1, a2, a3, a4, a5); free_heap_obj(f); return r; } case 6: { obj* r = FN6(f)(fx(0), a1, a2, a3, a4, a5); free_heap_obj(f); return r; } @@ -391,7 +391,7 @@ obj* apply_6(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6) { unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 6) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 6: { obj* r = FN6(f)(a1, a2, a3, a4, a5, a6); free_heap_obj(f); return r; } case 7: { obj* r = FN7(f)(fx(0), a1, a2, a3, a4, a5, a6); free_heap_obj(f); return r; } @@ -444,7 +444,7 @@ obj* apply_7(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 7) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 7: { obj* r = FN7(f)(a1, a2, a3, a4, a5, a6, a7); free_heap_obj(f); return r; } case 8: { obj* r = FN8(f)(fx(0), a1, a2, a3, a4, a5, a6, a7); free_heap_obj(f); return r; } @@ -495,7 +495,7 @@ obj* apply_8(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 8) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 8: { obj* r = FN8(f)(a1, a2, a3, a4, a5, a6, a7, a8); free_heap_obj(f); return r; } case 9: { obj* r = FN9(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8); free_heap_obj(f); return r; } @@ -544,7 +544,7 @@ obj* apply_9(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 9) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 9: { obj* r = FN9(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9); free_heap_obj(f); return r; } case 10: { obj* r = FN10(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9); free_heap_obj(f); return r; } @@ -591,7 +591,7 @@ obj* apply_10(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 10) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 10: { obj* r = FN10(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); free_heap_obj(f); return r; } case 11: { obj* r = FN11(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); free_heap_obj(f); return r; } @@ -636,7 +636,7 @@ obj* apply_11(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 11) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 11: { obj* r = FN11(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); free_heap_obj(f); return r; } case 12: { obj* r = FN12(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); free_heap_obj(f); return r; } @@ -679,7 +679,7 @@ obj* apply_12(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 12) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 12: { obj* r = FN12(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); free_heap_obj(f); return r; } case 13: { obj* r = FN13(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); free_heap_obj(f); return r; } @@ -720,7 +720,7 @@ obj* apply_13(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 13) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 13: { obj* r = FN13(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); free_heap_obj(f); return r; } case 14: { obj* r = FN14(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); free_heap_obj(f); return r; } @@ -759,7 +759,7 @@ obj* apply_14(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 14) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 14: { obj* r = FN14(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); free_heap_obj(f); return r; } case 15: { obj* r = FN15(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); free_heap_obj(f); return r; } @@ -796,7 +796,7 @@ obj* apply_15(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 15) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 15: { obj* r = FN15(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15); free_heap_obj(f); return r; } case 16: { obj* r = FN16(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15); free_heap_obj(f); return r; } @@ -831,7 +831,7 @@ obj* apply_16(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* unsigned arity = closure_arity(f); unsigned fixed = closure_num_fixed(f); if (arity == fixed + 16) { - if (!is_shared(f)) { + if (is_exclusive(f)) { switch (arity) { case 16: { obj* r = FN16(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16); free_heap_obj(f); return r; } }