You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Merge #305: types: use GhostCell in place of mutexes in union-bound and type context
060455a types: use GhostCell in union_bound rather than mutexes (Andrew Poelstra)
671a836 types: replace LockedContext with a mutex guard around ContextInner (Andrew Poelstra)
9212b39 types: introduce helper type to hold token alongside slab (Andrew Poelstra)
7dce5f0 types: use GhostToken for type context identity (Andrew Poelstra)
79bebd9 satisfy: add inference context to the Satisfier trait (Andrew Poelstra)
e18ffc0 policy: add (broken, ignored) unit test showing a problem with asm (Andrew Poelstra)
7e5df30 human_encoding: pass context object as argument to Node::to_witness_node (Andrew Poelstra)
a5aa6a2 node: add inference prameter to RedeemNode::to_construct_node (Andrew Poelstra)
a534de4 node: take context object as parameter to CommitNode::unfinalize_types (Andrew Poelstra)
dec28f3 node: take context as argument to all ConstructNode constructors (Andrew Poelstra)
65aab33 node: thread invariant 'brand lifetime through freeking everything (Andrew Poelstra)
fe8dc67 types: introduce 'Incomplete' type to represent incomplete type bounds (Andrew Poelstra)
c473b17 types: move innards of Context into a ContextInner type (Andrew Poelstra)
e2d1c4c types: remove Default from Context (Andrew Poelstra)
5411440 add ghost-cell dependency (Andrew Poelstra)
c7bfcbf add simple RedeemNode benchmark (Andrew Poelstra)
Pull request description:
I recently learned about the [GhostCell](https://crates.io/crates/ghost-cell) crate, and its associated paper from ICFP 2021. There are a couple of similar projects from that era, notably `qcell` which predates the published version of ghostcell by a bit, but none of these are used much, as evidenced by the "Dependents" tab on crates.io.
I learned about them from a blog post about ["generativity"](https://arhan.sh/blog/the-generativity-pattern-in-rust/) which has a pattern that makes GhostCells a little more ergonomic-looking at the cost of using macros. (I don't think this is worthwhile and I didn't use them).
But the macro syntax isn't really the point. The key quote from the blog post is this
>The fundamental purpose of the generativity pattern is not necessarily to improve performance, but to statically require that individual values come from or refer to the same source. The performance benefits are a symptom of this requirement.
Anyway, GhostCells are extremely powerful and I don't know why they are not more popular. In effect, they allow synchronizing a single zero-sized token, and gating access to an arbitrarily-sized set of otherwise-disconnected objects on them. So if you have a `&mut Token` you can get mutable access to all of your objects.
This is exactly the situation we have with our type inference context and our union bound algorithm: we have a `Context` object which has a `Mutex` controlling access to a slab of allocated bounds, and then we have a whole pile of `UbElements` which are connected in a forest structure that the Rust compiler doesn't really understand, but where we morally have exclusive access exactly when we have exclusive access to the slab. `GhostCell` lets us tell the compiler this.
This PR
* Eliminates all the mutexes in the type checker except the one in the `Context` object that holds the slab
* Fixes multiple bugs related to inconsistent contexts, including one in the policy module which made it impossible to actually use the asm fragment functionality
* Adds an invariant lifetime `'brand` which acts as a tag on all `Type`s, `ConstructNode`s and `WitnessNode`s which prevent them being combined if they come from different type inference contexts
* Requires the user to do node construction inside a closure which is passed to `Context::with_context`, rather than constructing a context object which then sorta leaks into the ether by being contained in an `Arc` carried by each node
The latter item sounds like a big ergonomic hit, but in practice it's not a big deal because it doesn't affect `CommitNode` or `RedeemNode`.
The use of a lifetime rather than a marker type means that while every type context has a "distinct type" for `Type`, `Arrow`, `ConstructNode`, etc., the distinction is erased after typechecking. So compilation speed and program size will not be adversely affected. But conversely, the compiler error messages are pretty unclear when you use this incorrectly.
ACKs for top commit:
canndrew:
ACK 060455a
Tree-SHA512: 2f7fd1eb729ef90aaa47cb24de2f6c70d70899ef0fd152f105469673648cdec73a63f31cc753e700e759d5949dab00452fefd686f1bb3405b7b9f2d909278f86
0 commit comments