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

[WIP] Stop materializing placeholder liveness at all points #157

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from

Conversation

lqd
Copy link
Member

@lqd lqd commented Dec 23, 2020

To align the code with the datalog rules, and clean up our laziness love for simplicity, we'd have to remove the workaround where we materialized liveness data for the placeholder origins to be live at all points, where we historically had more complex rules in our soufflé prototypes, involving ; for every join ensuring an origin's liveness.

Doing that with datafrog is painful and verbose of course, but the point of opening this draft PR is for discussion during the next sprint. And see whether the cost is worth the gain.

While the LocationInsensitive and Naive uses are mostly straightforward cases of switching from origin_live_on_entry(Origin1, TargetNode) predicates to (origin_live_on_entry(Origin1, TargetNode); placeholder(Origin1, _)) predicates by expanding the whole rule for each of the alternatives, the Opt variant contains more subtle cases (in addition to these simple but verbose ones).

Since the variant is trying to limit the subset TC to origins dying along an edge, detecting when liveness ends is required, and relies on many instances of !origin_live_on_entry(Origin1, TargetNode) antijoins. In some rules, there seems to be nothing required for these antijoins to support the now-missing materialization: some rules which were not applicable to placeholders (whether because of fact generation, or earlier-rules filtering them out) when they were present in origin_live_on_entry, still aren't.

For example, Opt rule 14:

dead_borrow_region_can_reach_root((origin, point), loan) :-
  loan_issued_at(origin, loan, point),
  !origin_live_on_entry(origin, point).

No loans are issued in placeholders, this relation is the same whether they're present in origin_live_on_entry or not.

For others, like Opt rule 3 which uses both polarities, it doesn't seem to be that simple:

live_to_dying_regions(origin1, origin2, point1, point2) :-
  subset(origin1, origin2, point1),
  cfg_edge(point1, point2),
  (origin_live_on_entry(origin1, point2); placeholder_origin(origin1)),
  !origin_live_on_entry(origin2, point2).

If origin2 is a placeholder, the antijoin would have previously eliminated it from live_to_dying_regions, but now it seems we'd need to add another predicate like so:

live_to_dying_regions(origin1, origin2, point1, point2) :-
  subset(origin1, origin2, point1),
  cfg_edge(point1, point2),
  (origin_live_on_entry(origin1, point2); placeholder_origin(origin1)),
  !origin_live_on_entry(origin2, point2),
  !placeholder_origin(origin2).

otherwise origin2 would be considered dying here !

And the translation rules would be:

  • previous joins with origin_live_on_entry had an implicit union with a join to the placeholder relation, which now needs to be made explicit in the rules with an alternative predicate. That mechanically expands to the combinations of all alternatives (some rules like Opt rule 10 have 2 such alternative predicates, and therefore 4 datafrog expansions, for a whopping 62 line piece of code) (these expansions are done in this PR, in all 3 variants, and were all done using leapjoins with either a "filter" or "extend" leaper, depending on the WF-ness of the resulting leapjoin. Note that this is operationally very similar since placeholder_origin is a single-value relation, there's only a single unit tuple extend_with leapers can find for the join; very filter_with-like)
  • previous antijoins with origin_live_on_entry had an implicit antijoin with the placeholder relation, which now needs to be made explicit in the rules, with a new antijoin predicate. That mechanically expands to either a new leaper when leapjoins are used, or another intermediate relation when regular joins are used (neither of which is done in this PR yet).

The rustc UI test suite seems to behave similarly with and without this PR, so there may not be code which can exercise these subtleties, but at least we can talk about the theoretical aspects.

Does this seem correct to you all ? What do you think of the complexity this adds, versus the (hard to quantify, but I haven't really tried to do so for reals yet) gains ? (Maybe a macro based approach would be acceptable, or maybe more work in datapond to handle leapjoins and the most complicated rules could hide all of this under a proc macro veneer of simplicity 🌠 ).

For easier review/analysis, there's a commit for each variant (and from there one can go see the complete resulting file to have an idea of the damage):

Let's discuss !

lqd added 5 commits July 30, 2021 18:24
Also, add a descriptive message if the `assert_equal` helper fails its assertions.
…product of liveness

Also, number and comment the rules, because the expansions are very verbose and mistakes are easy to make here.

We simplified the rules by modeling the fact that placeholder origins are live at all points by ... materializing this as actual tuples in the `origin_live_on_entry` relation, even though liveness analysis does not computes that.

This was also done because soufflé provides an easy `;` alternative operator, while datafrog requires us to do the alternative expansions manually. (Also we were lazy)
We simplified the rules by modeling the fact that placeholder origins are live at all points by ... materializing this as actual tuples in the `origin_live_on_entry` relation, even though liveness analysis does not computes that.

This was also done because soufflé provides an easy `;` alternative operator, while datafrog requires us to do the alternative expansions manually. (Also we were lazy)
Also, number and comment some rules.

We simplified the rules by modeling the fact that placeholder origins are live at all points by ... materializing this as actual tuples in the `origin_live_on_entry` relation, even though liveness analysis does not computes that.

This was also done because soufflé provides an easy `;` alternative operator, while datafrog requires us to do the alternative expansions manually. (Also we were lazy).

Where possible `filter_with` leapers were added, and where WF-ness would not be possible, `extend_with` leapers were used. This should be similar here: the `placeholder_origin` relation being a single value relation, there is only a single unit tuple to extend a key with.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants