-
Notifications
You must be signed in to change notification settings - Fork 1
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
Frontend Holes #107
Open
stephenverderame
wants to merge
34
commits into
main
Choose a base branch
from
frontend_hole
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Frontend Holes #107
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This refactors the code to prepare for the frontend's initialization algorithm that determines where to make uninitialized mutables usable.
The initialization algorithm has 2 parts. The first part places initializations at the latest possible points. This change begins work on this algorithm by introducing the init_synth module which contains functions to generate initializer sets of each uninitialized mutable variable. An initializer set is a set of hole locations that collectively dominate the uses of the mutable they initialize.
Finished phase 1 of the initialization algorithm that places initializations of uninitialized variables as late as possible.
To prepare for the second phase of the frontend initialization algorithm, which hoists the initialization points to better locations, if any exist, we first minimize the initialization set by removing hole locations that are collectively strict dominated by a subset of the initialization set. That is to say, the mutable must already be initialized at the program point, and so it can be removed without affecting correctness.
This change enables writes to variables that don't have select quotients to occur withen the branches of an if. This is done by introducing a more flexible SpliceTerm type expression that can either match like a regular term or replace itself with a child, provided all its children can unify with eachother. Further, we allow phi nodes to unify with constraints that aren't selects by making the phi node constraints to be a SpliceTerm. The coding pattern this change enables is a bit strange to write manually, but can be easily generated by the frontend by putting holes in both branches of an if. Finally, this change also introduces some utilities needed for phase 2 of the initialization algorithm.
This implements a mostly working hoist algorithm to improve upon the placement of initializations of variables. At a high-level, we hoist an initialization point to a set of collectively dominating holes if we must initialize less dependencies at those holes. To take into account sharing of dependencies between other variables, a given variable is only considered to initialize `1/n` of a node where `n` is the number of other initializations at the hole that also depend on the same node.
This allows variable initialization to consider sharing initializations with static definitions of a hole.
Adds tests and fixes bugs they caught. Also catches undefined node errors in specs.
This change introduces VarName and ClassName newtypes to better distinguish between the different unification type names such as variable names, class names without the class identifier, and class names with the class identifier. Many places in the code still use Strings to represent variables, however, every class name should now be represented with the ClassName newtype. This change also fixes semantic versioning checking.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is quite a large PR, and I've been working sporadically on this for quite some time, so I don't think I even know everything that changed off the top of my head right now. I do want to write a blog post or two going through some things in more detail.
Generally, I assumed that the explicator only explicates within a funclet, so the frontend still errors if it can't determine types for anything that might cross a funclet boundary. The previous type deduction algorithm is still in use, just with some new features.
The frontend also does a little bit of (polynomial time) synthesis itself now to determine when to make a mutable variable usable if the user never explicitly writes to it. Unless the program is ill-formed, the solution will always be valid, but not necessarily globally optimal, However, the solution has a property that can be thought of as local optimality.
Otherwise, the frontend type deduction should only make unambiguous decisions that can't be wrong, requiring type annotations if something can't be deduced. In all cases, the user should be able to specify what they want with type annotations.
?
Hole. It's not clear to me whether this is something we'd want in the long run or just want to fold it into the???
. Basically, this corresponds to the assembly?
and roughly the semantics of this can be thought of as?
is an expression that can take the value of any variable that reaches it. Where "reaches" here is defined to consider that references can't cross funclet boundaries and how variables are consumed. So in Sketch,?
is basically{| v_1 | v_2 | ... | v_n |}
wherev_1, ..., v_n
are variables that reach?
. Note?
cannot dereference references. As a consequence of how renaming is used for shadowing variables, a hole can use a shadowed variable right now.???
hole. This can be used as an expression or statement and allows for arbitrary codegen by the explicator. Like?
, it effectively uses every variable that reaches it.???
as an expression will generate assembly corresponding to an allocation of a temporary, a big hole, then a use of the temporary. I'm not sure if this is better or worse for the explicator than just a big hole and a small hole.ReachingDefs
pass that calculates reaching defs and ensures that all definitions reach their uses.???
holes which correspond to the "optimized latest possible point". That is we start initializing mutables at the latest possible point and then hoist the initializations as high as possible such that the new initialization set is strictly better than the previous one.UninitCheck
pass that is similar toReachingDefs
but ensures that variables are initialized at every use they are needed to beusable
.if
. Previously, it would break if anything other than the spec's result of theif
was stored to in a branch of theif
. In other words, it was assumed that frontend PHI nodes always correspond to anif
in the spec, which isn't always true. For example, we could write the same value to a variable in both branches of anif
._
variable name. This is a regular variable, except that the name_
can only be used in a variable definition. Due to renaming, the assembly will see this as_%n
for some integern
.n
represents some integer.%n
is a suffix for AST-level SSA renaming to support things like scoping and shadowing..n
is a suffix for IR level SSA renaming, which considers writing a new "definition"._v_ref
is for the underlying reference of the mutable variable namedv
(as mutable variables in the frontend have value semantics).!
is used to prepend meta-variable names in type unification to gen a new intermediate variable.$
is used to prepend all spec variable names (class names) in type unification._hn
is for the implicit definition(s) of a???
hole when it's used as an expression._fn
is for AST-level temporaries created by flattening._tn
is for assembly-level temporaries created by lowering._t_v1_v2_..._vn
is a tuple of variablesv1
tovn
. So for example_c%0_ref.0
is the original definition of the backing reference of some user mutable variablec
.FileCheck
like script for testing test outputstorage
,map_read
, andcopy_dst
. (The type name suffix::gds
whereg
stands for GPU,s
is for source (copy_dst
), andd
is for destination (map_read
). This isn't ideal, but deduction of these might not be possible in cases with holes where it becomes unknown all the ways a variable is used.