Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add replay history to match names between two downwards traversals #3302

Open
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

Gbury
Copy link
Contributor

@Gbury Gbury commented Nov 22, 2024

[Note: This is a pre-requisite of match-in-match; the mechanism introduced is not yet used in this PR, but will be used by continuation specialization when the PR for match-in-match is opened]

In some cases (mostly the upcoming continuation specialization for match-in-match), we are interested in doing multiple downwards pass on a single term. In such cases, it might be necessary to relate the names of variables and continuations from the first pass to those from the subsequent passes. The predominant use of that for now should be to correctly handle continuations that have been lifted during the first pass, and whose calls should be rewritten in subsequent passes (including their lifted arguments).

This is done by storing the sequence of names generated when opening name abstractions during the first downwards pass. On subsequent passes, each new variable and continuation "consumes" an element of that sequence, allowing to establish the correspondance between names. As a safety measure, we check that correspondings names are in the same "renaming equivalence class", though note that this is not a guarantee (for isntance, by default all continuation have no names and therefore will all be in the same "renaming equivalence class").

Additionally, and this is more specific to continuation specialization but generalizable to other future uses, it is necessary to have some kind of replayability of inlining decisions. Indeed each inlining decision will change the sequence of bound names that are opened during the downwards pass, which would currently break the hypothesis of replay histories that exactly the same sequence of binders are opened during both downwards passes. In the case of match-in-match this is simple: the handler that we want to specialize ends with a switch, which means that any call inside the handler have been inlined, so the replay history has a boolean to denote that we want to inline everything while replaying the handler downwards pass. For other more complex uses, inlining decisions could be stored alongside the bound variables and continuations, so that they can be replayed, either as is, or within some notion of compatibility.

Finally, we also need to make it so that recursive continuations are bound in an order that is stable through renaming, so we change the map of continuation to an Lmap for recursive continuation bindings.

In the future, this replay mechanism would also be useful to do widening for recursive continuations (but that's a far away future).

@Gbury Gbury added flambda2 Prerequisite for, or part of, flambda2 match-in-match prerequisites, or part of, match-in-match labels Nov 22, 2024
In some cases (mostly the upcoming continuation specialization for
match-in-match), we are interested in doing multiple downwards pass on a
single term. In such cases, it might be necessary to relate the names of
variables and continuations from the first pass to those from the
subsequent passes. The predominant use of that for now should be to
correctly handle continuations that have been lifted during the first
pass, and whose calls should be rewritten in subsequent passes
(including their lifted arguments).

This is done by storing the sequence of names generated when opening
name abstractions during the first downwards pass. On subsequent passes,
each new variable and continuation "consumes" an element of that
sequence, allowing to establish the correspondance between names. As a
safety measure, we check that correspondings names are in the same
"renaming equivalence class", though note that this is not a guarantee
(for isntance, by default all continuation have no names and therefore
will all be in the same "renaming equivalence class").

Additionally, and this is more specific to continuation specialization
but generalizable to other future uses, it is necessary to have some
kind of replayability of inlining decisions. Indeed each inlining
decision will change the sequence of bound names that are opened during
the downwards pass, which would currently break the hypothesis of replay
histories that exactly the same sequence of binders are opened. In the
case of match-in-match this is simple: the handler that we want to
specialize ends with a switch, which means that any call inside the
handler have been inlined, so the replay history has a boolean to denote
that we want to inline everything while replaying the handler downwards
pass. For other more complex uses, inlining decisions could be stored
alongside the bound variables and continuations, so that they can be
replayed, either as is, or within some notion of compatibility.

Finally, we also need to make it so that recursive continuations are
bound in an order that is stable through renaming, so we change the map
of continuation to an Lmap for recursive continuation bindings.

In the future, this replay mechanism would also be useful to do widening for
recursive continuations (but that's a far away future).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
flambda2 Prerequisite for, or part of, flambda2 match-in-match prerequisites, or part of, match-in-match
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants