[mega pr, do not merge] types: rewrite inference API to use a slab allocator for type bounds #228
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
The arrow module has a ton of `for_*` methods which duplicate the methods in the Constructible traits. Most of these are purely redundant and can be deleted. A couple provide some code reuse, and are demoted to be non-`pub`. Smoe variable names changed in the redundant code, so this will likely not appear as a code-move in the diff, even though it is one. You can just skim this commit.
Refactor only.
This eliminates an `unwrap`, cleans up a bit of code in named_node.rs, and moves every instance of `Type::from` into types/mod.rs, where it will be easy to modify or remove in a later commit. Also removes From<Arc<Final>> for Type, a somewhat-weird From impl which was introduced in #218. It is now superceded by Type::complete. In general I would like to remove From impls from Type because they have an inflexible API and because they have somewhat nonobvious behavior.
The type_name conversion methods use a private TypeConstructible trait which winds up taking more code to use than it saves by reducing reuse. (Though arguably the reuse makes the code more obviously internally consistent.) In future we won't be able to use this trait anyway because the Type constructor will need a type-inference context while the other constructors will not. So delete it now.
This looks like a purely noise-increasing change, but when we introduce type inference contexts, we will need the auxiliary type to hold an inference context (which will be unused except for sanity-checking that users are being consistent with their inference contexts).
apoelstra
force-pushed
the
2024-06--slab-inference
branch
from
80f427c
to
79cee92
Compare
This is a super noisy commit, but all it does is introduce the src/types/context.rs module with a dummy Context type, and make all the node construction APIs take this and make copies of handles of it. The next commit will actually _use_ the context in type inference. This one can therefore be mostly skimmed. The maybe-interesting parts are the conversion methods, which can be found by searching the diff for calls to `from_inner`.
This is again an API-only change.
This is again an "API only" change. Also fixes a couple code-cleanliness things in the benches/ crate.
The sum and product constructors don't obviously need to be passed a type context -- after all, the two child types already have a type context embedded in them. However, it turns out in practice we have a context available every single time we call these methods, and it's a little bit difficult to pull the context out of Types, since Types only contain a weak pointer to the context object, and in theory the context might have been dropped, leading to a panic. Since the user already has a context handle, just make them pass it in. Then we know it exists.
Our union-bound algorithm uses some features of Arc (notably: cheap clones and pointer equality) and therefore holds an Arc<T>. But in a later commit we will want to replace the Arcs with a different reference type, and to do so, we need to make this code more generic.
…ion-bound This introduces the BoundRef type, an opaque reference type which currently just holds an Arc<BoundMutex>, but which in a later commit will be tied to the type inference context and refer to data within the context. It currently preserves the get() and set() methods on BoundRef, which come from BoundMutex, but these will need to be replaced in a later commit, since eventually BoundRef by itself will not contain enough information to update its data. This is essentially an API-only change though it does move some data structures around.
Once our BoundRefs start requiring an inference context to access their data, we won't be able to call .set() and .get() on them individually. Remove these methods, and instead add them on Context. Doing this means that everywhere we currently call .get and .set, we need a context available. To achieve this, we add the context to Type, and swap the fmt::Debug/fmt::Display impls for Type and Bound so that Type is the primary one (since it has the context object available). The change to use BoundRef in the finalization code means we can change our occurs-check from directly using Arc::<Bound>::as_ptr to using a more "principled" OccursCheckId object yielded from the BoundRef. This in turn means that we no longer need to use Arc<Bound> anywhere, and can instead directly use Bound (which is cheap to clone and doesn't need to be wrapped in an Arc, except when we are using Arc to obtain a pointer-id for use in the occurs check). Converting Arc<Bound> to Bound in turn lets us remove a bunch of Arc::new and Arc::clone calls throughout. Again, "API only", but there's a lot going on here.
Pulls the unify and bind methods out of Type and BoundMutex and implement them on a new private LockedContext struct. This locks the entire inference context for the duration of a bind or unify operation, and because it only locks inside of non-recursive methods, it is impossible to deadlock. This is "API-only" in the sense that the actual type bounds continue to be represented by free-floating Arcs, but it has a semantic change in that binds and unifications now happen atomically (due to the continuously held lock on the context) which fixes a likely class of bugs wherein if you try to unify related variables from multiple threads at once, the old code probably would due weird things, due to the very local locking and total lack of other synchronization. The next commit will finally delete BoundMutex, move the bounds into the actual context object, and you will see the point of all these massive code lifts :).
…xt slab This completes the transition to using type contexts to keep track of (and allocate/mass-deallocate) type bounds :). There are three major improvements in this changeset: * We no longer leak memory when infinite type bounds are constructed. * It is no longer possible to create distinct programs where the variables are mixed up. (Ok, you can do this still, but you have to explicitly use the same type context for both programs, which is an obvious bug.) * Unification and binding happen atomically, so if you are doing type inference across multiple threads, crosstalk won't happen between them.
apoelstra
force-pushed
the
2024-06--slab-inference
branch
from
79cee92
to
b4a2672
Compare
This avoids passing `hint` through all the layers of recursion, but more importantly, constructs the actual error from a `Context` rather than from a `LockedContext`. In the next commit, we will need extra information to do this, and not want our context to be locked at the time.
After the previous commit, we still had a memory leak in the case of cyclic types, but for a very dumb reason: the Type structure was carrying a Context Arc, and Type was recursive. Instead, introduce a new private TypeInner type which is recursive and does not have direct access to the Context. Make Bound private as well, since it is mutually recursive with Context. I am not thrilled with this commit and may revisit it, but it fixes the leak and lets me get on with fuzzing before I go to bed.
apoelstra
force-pushed
the
2024-06--slab-inference
branch
from
56d98fa
to
46c8720
Compare
|
I will probably break this into more than 2 PRs, but I'll leave this open for now as the "source of truth" for the whole project. |
apoelstra
changed the title
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.
Our existing type inference engine assumes a "global" set of type bounds, which has two bad consequences: one is that if you are constructing multiple programs, there is no way to "firewall" their type bounds so that you cannot accidentally combine type variables from one program with type variables from another. You just need to be careful. The other consequence is that if you construct infinitely sized types, which are represented as a reference cycle, the existing inference engine will leak memory.
A third issue, though I am unsure whether it leads to actual bugs, is that the type inference engine can only lock data at the granularity of individual type bounds, meaning that multi-step parts of type inference are not done atomically, and if you try to construct a program in a multithreaded context, it is possible that strange/unexpected things will happen.
To avoid this, it is better that each program under construction has an independent "type inference context" which holds a slab allocator. When the context is dropped, which happens when the initial constructed context and all the program nodes that reference it are dropped, it deallocates all the type bounds in one shot, rather than chasing Arcs and failing to notice cycles.
This is a 2000-line diff but the vast majority of the changes are "API-only" stuff where I was moving types around and threading new parameters through dozens or hundreds of call sites. I did my best to break everything up into commits such that the big-diff commits don't do much of anything and the real changes happen in the small-diff ones to make review easier.
Builds on #227.
This does not fix #226 although it sets the stage for "checkpointing" the type inference context, which should allow a reasonably-efficient way to undo changes when things go wrong.