flambda2-types: New n-way join algorithm

[bclement-ocp]

The existing join algorithm suffers from several drawbacks:

• It can be slow due to the use of a quadratic algorithm, taking up to 60% of the total compilation time in -O3 mode in pathological cases (lambda_to_flambda_primitives.ml). See also Improve join performance #3300.

• It is inefficient as it computes the join of all types appearing in any joined environment prior to filtering out the types that are not needed, instead of first computing the types whose join will be needed.

• It is sensitive to the names of local variables that only exist in some of the joined environments but not in the target environment.

• It relies on a global binding time of variables across all joined environments and the target environment that does not exist, as figured in Revert "Ensure consistent variable binding times (#3217)" #3278. Subsequently, it can lose aliasing information, and breaks typing env invariants by recording the same variable as defined multiple times (with dubious semantics).

This patch implements a new join algorithm, based on a n-way join of types. The new algorithm is:

• Faster, as it avoids quadratic complexity (outside of complex nesting of env extensions). Compared to the existing join algorithm (with advanced meet), on my machine, the new join algorithm is 30x faster on the pathological lambda_to_flambda_primitives.ml, taking only around 10% of the total compilation time and speeding up the compilation of the file by 3.5x. On camlinternalFormat.ml, the new join is about 2.5-3x faster, reducing the time spent in the join from 20% to less than 10% and speeding up the total compilation time by about 20%.

• More efficient, as it only computes a join if it can possibly result in a more precise type, i.e. if the variable has been assigned a new type in all joined environments (otherwise the existing type in the target environment is already the most precise).

• Independent of the names of local variables.

• Only depends on a consistent binding time order of the shared variables (defined in both the target environment and all joined environments), which is respected. Since the result is independent of the binding times of local / existential variables, the typing env invariants are respected.

Reviewing guide

The actual changes in this PR are in the Meet_and_join_new and Join_env modules, as well as Join_levels (which is now just a small wrapper over Join_env). The changes in both modules are mostly independent: changes in Meet_and_join_new make the join of types a n-way join, while the Join_env module implements the new join algorithm for environments, and in particular takes care of joining aliases. The main thing to know to relate these two modules is that the join of (canonical) alias types should go through Join_env.n_way_join_simple, which will return an appropriate alias (creating a local variable if required) in the target env.

(As an aside: I think the organization of the Join_env module is roughly right, but am not too satisfied with the names of things and happily take suggestions)

The rest of the changes are temporary, and mostly intended for further debugging of the PR. They should not need to be reviewed, and will be removed before merging the PR. In particular, the Meet_new_and_join_old and Join_levels_old modules are (almost) identical copies of the Meet_and_join_new and Join_levels modules from main. They are used in conjunction with the environment variable FLAMBDA2_JOIN_ALGORITHM=checked to compare the results of the new and old join algorithm. This comparison uses the auxiliary Equal_types_for_debug module to print out the result of joins that are different when computed using the new and old join algorithms. When visually inspecting such differences, I recommend also setting FLAMBDA2_JOIN_DEBUG_IGNORE_NAMES=cse_param -- the new join is better at preserving equations between cse_param variables and this creates noise.

From my own inspection, the main differences between the old and new join is that the new join is better at preserving aliases (so sometimes the new join will have an alias where the old join will have duplicated the type), and it is also better at preserving the alloc_mode of blocks (the old join considers the alloc mode of Bottom blocks, while the new join ignores them -- which I think is correct).

Symbol projections

I am not sure I understand how symbol projections are supposed to be joined. The old join seems to preserve symbol projections as long as they are present in one of the joined envs (and the variable is still accessible in the target env), which might make sense from the point of view of Simplify but seems dubious from the point of view of the typing env. The new join preserve symbol projections if they are present in all of the joined envs (up to demotions) because that is what seems sensible for a join, but I am not sure if this is the intended semantics. I don't really understand how symbol projections are created/used; maybe @mshinwell can clarify.

Basic meet

The PR is currently only compatible with the new (advanced) meet, which will always be used when joining environments. Before merging the PR, we should decide how we want to proceed w.r.t. the basic meet. If it goes away, there is nothing to do; if we still keep it for a bit, we can either keep the Join_levels_old module for the basic meet; force the join to go through the advanced meet (even if the basic meet is otherwise used); or adapt the n-way join code for the basic meet as a last resort.

[bclement-ocp]

(Looking at the failures — we should probably detect Bottom prior to "Cannot add alias between two consts: 1, 0")

[bclement-ocp]

(Looking at the failures — we should probably detect Bottom prior to "Cannot add alias between two consts: 1, 0")

Yup, this one seems ultimately unrelated — we have an invariant asserting that we do not add aliases between two constants that we check before the code that deals with aliases between constants. Will fix in a separate PR.

The other is a real bug in the n-way join — I was misled to the semantics of the "other" field for row-like by the code for the meet, and do not deal properly with the join of a tag that is known on one side and "other" in an other side. Fix incoming.

[bclement-ocp]

I forgot to mention in the PR description that there is a subtle case with env extensions where we can lose equations.

Consider that we are performing the join between x : (tagged_imm (= a)) and x : (tagged_imm (= b)). We will create a new existential variable ab with type the join of the types of a and b and set x : (tagged_imm (= ab)).

If we later have an env extension with b : (= a) on the right, we will include ab : (= a) in the joined extension. But if we process the env extension first, we will not have the equation ab : (= a) in the joined extension.

I don't think we are likely to hit this case frequently in practice, so it's probably fine, but ideally we'd want to process env extensions after the non-extension types to avoid this corner case.

[bclement-ocp]

Note: the new join implements a variation of @lthls's suggestion in #472 and fixes #472 even though it does not use the join_depth parameter from #474.

[lthls]

I've gone through joined_env.ml, which should be the most complex part of the PR. I'm posting my review notes on this file, and will move on to the rest of the PR.

[bclement-ocp]

Rebased on top of #3689 and added proper -flambda2-join-algorithm flag.

This makes the review of Meet_and_n_way_join a bit more annoying, especially for meet_disjunction and meet_row_like, since it's no longer in the same file. Sorry :(

[bclement-ocp]

Rebased after removing the new meet. I added a separate commit that introduces meet_and_n_way_join.ml as a copy of meet_and_join.ml, which should help with the review of the Meet_and_n_way_join module by doing the review commit by commit (the only other commit touching the meet_and_n_way_join.ml file should be the one called "flambda2-types: New n-way join algorithm").