Lots of unnecessary copies of object_ref

[legrosbuffle]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X ] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Move constructors for objects deriving from object_ref in lean are making a copy, probably due to the assumption that an rvalue reference is propagated as such across function calls.

Example:

expr(expr && other):object_ref(other)

should be:

expr(expr && other):object_ref(std::move(other))

As a result, there are a lot of unnecessary incref/decref calls on object_ref. We've measured that expr copying and assignment by itself uses 10% of total runtime on our workloads.

Context

No specific context.

Steps to Reproduce

Expected behavior:

expr::expr(expr&& other) calls object_ref::object_ref(object_ref&&), which steals refcount from other, no incref happens.

Actual behavior:

expr::expr(expr&& other) calls object_ref::object_ref(const object_ref&), which increfs other's refcount. Then the callee decrefs other's refcount.

Versions

v4.7.0

Additional Information

n/a

Impact

Performance only.

[eric-wieser]

@legrosbuffle, thanks for this; can this issue be closed, or do you intend to track more improvements with this issue?

[legrosbuffle]

I have a few more :)