No reset/reuse instructions for simple conversion function
Closed this issue · 0 comments
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
Description
In the example
set_option trace.compiler.ir.reset_reuse true
def Sigma.toProd : (_ : α) × β → α × β
| ⟨a, b⟩ => (a, b)
we get the IR
[reset_reuse]
def Sigma.toProd._rarg (x_1 : obj) : obj :=
case x_1 : obj of
Sigma.mk →
let x_2 : obj := proj[0] x_1;
let x_3 : obj := proj[1] x_1;
let x_4 : obj := ctor_0[Prod.mk] x_2 x_3;
ret x_4
def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj :=
let x_3 : obj := pap Sigma.toProd._rarg;
ret x_3
As we can see, the memory cell of the input is not reused, even though the Sigma
and Prod
constructors are compatible. Ideally, the generated IR would be
[reset_reuse]
def Sigma.toProd._rarg (x_1 : obj) : obj :=
case x_1 : obj of
Sigma.mk →
let x_2 : obj := proj[0] x_1;
let x_3 : obj := proj[1] x_1;
let x_5 : obj := reset[2] x_1;
let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_2 x_3;
ret x_4
def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj :=
let x_3 : obj := pap Sigma.toProd._rarg;
ret x_3
so that the memory cell is reused if possible.
Context
The algorithm from the Counting Immutable Beans paper would insert reset/reuse instructions in this case. However, there is an explicit check in the Lean compiler that checks that reset/reuse instructions are only inserted if the type matches up. This makes sense: in an example like
def foo : List (Nat × Nat) → List Nat
| [] => []
| x :: xs => match x with
| (a, _) => a :: foo xs
without the check that the types match, the generated code would try to reuse the memory cells of the pairs instead of the list, so we wouldn't get a traditional destructive update, leading to performance degradation if the pairs in the input are all shared but the list itself is unique.
However, inserting some reset
/reuse
instructions should always be better than inserting none at all, so it would be nice if the heuristic could be tweaked to cover the case of conversion functions like Sigma.toProd
.
Steps to Reproduce
- Inspect the generated IR for the function
Sigma.toProd
above.
Expected behavior: reset
and reuse
instructions should be present in the IR.
Actual behavior: No reset
and reuse
instructions.
Versions
Lean (version 4.9.0, commit 883a3e7, Release)
Additional Information
[Additional information, configuration or data that might be necessary to reproduce the issue]
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.