wasmtime icon indicating copy to clipboard operation
wasmtime copied to clipboard

Wasmtime(gc): Add support for supertypes and finality

Open fitzgen opened this issue 1 year ago • 2 comments

This is the final type system change for Wasm GC: the ability to explicitly declare supertypes and finality. A final type may not be a supertype of another type. A concrete heap type matches another concrete heap type if its concrete type is a subtype (potentially transitively) of the other heap type's concrete type.

Next, I'll begin support for allocating GC structs and arrays at runtime.

I've also implemented O(1) subtype checking in the types registry:

In a type system with single inheritance, the subtyping relationships between all types form a set of trees. The root of each tree is a type that has no supertype; each node's immediate children are the types that directly subtype that node.

For example, consider these types:

class Base {}
class A subtypes Base {}
class B subtypes Base {}
class C subtypes A {}
class D subtypes A {}
class E subtypes C {}

These types produce the following tree:

           Base
          /    \
         A      B
        / \
       C   D
      /
     E

Note the following properties:

  1. If sub is a subtype of sup (either directly or transitively) then sup must be on the path from sub up to the root of sub's tree.

  2. Additionally, sup must be the ith node down from the root in that path, where i is the length of the path from sup to its tree's root.

Therefore, if we maintain a vector containing the path to the root for each type, then we can simply check if sup is at index supertypes(sup).len() within supertypes(sub).

fitzgen avatar May 10 '24 23:05 fitzgen

Subscribe to Label Action

cc @saulecabrera

This issue or pull request has been labeled: "wasmtime:api", "winch"

Thus the following users have been cc'd because of the following labels:

  • saulecabrera: winch

To subscribe or unsubscribe from this label, edit the .github/subscribe-to-label.json configuration file.

Learn more.

github-actions[bot] avatar May 11 '24 02:05 github-actions[bot]

Therefore, if we maintain a vector containing the path to the root for each type, then we can simply check if sup is at index supertypes(sup).len() within supertypes(sub).

This means that the storage for the vecs in each tree is, in total, in O(N log N), right?

I think there's a cheaper O(N) storage per tree way to do it, that still offers O(1) subtype checking:

  • Store nodes of the tree in a vec where all descendents of a node occur after that node and before any non-descendent node.
  • Each node stores the index of its last descendent. If it has none, then the index will be its own index.
  • To test whether sub is a subtype of sup:
    • Look up trees and indexes of both types.
    • If they live in different trees, then there is no subtype relationship.
    • Otherwise, look up sup's node. If sup_index < sub_index && sub_index <= sup_last_descendent then we have a subtype.

EDIT: And I guess if the types are already stored in some other structure(s), there's actually no need for a separate vector for this information; the primary representation of the type can just have those extra fields for: tree ID, index in tree, max descendent index.

There's a good chance I've misunderstood something (e.g. how the trees are updated?), but if there's nothing else special about these trees then maybe this optimisation is applicable! 🙏

jeffparsons avatar May 12 '24 01:05 jeffparsons

@jeffparsons, thanks for digging in here! Always appreciate a second pair of eyes.

This means that the storage for the vecs in each tree is, in total, in O(N log N), right?

It is indeed a time-space tradeoff, but as-implemented it can actually be even worse than O(n log n): consider a chain where each type is a subtype of its predecessor: a; b <: a; c <: b; d <: c; .... The ith type's supertype array will be of length i - 1, and this forms the classic "triangle" shape that indicates O(n * n) behavior. This particular case could be resolved (although the implementation would be a bit awkward in the presence of type canonicalization across modules) by defining the supertype arrays in sub-to-supertype order and then using a subslice of a subtype's supertype's vector, when one is present, instead of allocating a new vector. Then I think we would be at O(n log n) in general again.

However, implementations are allowed to define their own limits on the maximum depth a subtyping chain may have. And for JS embeddings, it is additionally tightened from "some implementation limit" to 63; for maximum cross-engine compatibility, we've always matched the JS embedding limits.

https://webassembly.github.io/gc/js-api/index.html#limits

Anyways, the point is that this limit provides bounds on the total memory overhead associated with these supertype vectors, preventing worst-case scenarios.

Finally, my understanding is that it is pretty much expected that engines implement subtyping checks with this technique, FWIW. For example, here is SpiderMonkey's docs about doing this same thing: https://searchfox.org/mozilla-central/rev/ee2ad260c25310a9fbf96031de05bbc0e94394cc/js/src/wasm/WasmTypeDef.h#480-541

This is a good reminder to double check that we are actually enforcing the subtyping depth limits in validation, though :-p

I think there's a cheaper O(N) storage per tree way to do it, that still offers O(1) subtype checking:

If I understand correctly, this is storing the entry and exit indices of a depth-first traversal of the tree and then subtype checking checks that (a) we are looking at the same tree and (b) that the subtype's index (doesn't matter if we check entry vs exit index) is within the supertype's range, correct?

This would indeed work very nicely in the context of a single Wasm module and a static set of types.

But, as you alluded to, things get problematic when we consider updates. GC objects can be passed between modules, and a non-final type from module A can be subtyped by another type in module B and then an instance of that subtype can be passed from B to A, and A might want to do subtyping checks on this instance even though it never defined the exact type of that instance. This necessitates canonicalizing types across modules. So, even though from a single Wasm module's perspective the type set is static, from an engine perspective we are constantly dynamically adding and removing types from the same deduplicated, canonicalized types registry as modules are loaded or unloaded (or when the host defines/drops types via the public Wasmtime API). And therefore our type hierarchies and their trees aren't static, and must support having subtrees grafted on and pruned away at any moment. That means we would need to recompute potentially all those depth-first traversal indices on every mutation, an O(n) operation for each new type definition, which is already too expensive on its own, but also leads to O(n * n) behavior when defining n new types.

So I don't think this approach is something we can use in this case, unfortunately.

fitzgen avatar May 13 '24 17:05 fitzgen