[dart2wasm] take advantage of unrecoverable soundness bugs for faster type checking

[yjbanov]

The current implementation of dart2wasm's type checks can take up to 95% of CPU time in some important Flutter use-cases, such as the semantics tree. For example, the Semantics.compileChildren benchmark takes 4473ms to run with type checks, and 240ms with the --omit-type-checks flag enabled.

Omitting type checks entirely is not practical as there will be code whose logic would break without them, such as is checks. For those, optimizing them as much as possible is a good strategy (e.g. https://github.com/dart-lang/sdk/issues/51635).

However, some type checks lead to unrecoverable program bugs, such as:

• Explicit as type casts.
• Implicit downcast due to covariant.
• Implicit downcast from dynamic to any other type.

The result of failing these type checks is a TypeError. Most Dart programs never catch these errors, which makes them fatal. These programs are designed under the assumption that TypeError will never happen. For this category of errors it would be reasonable to relax the type check requirement and do the minimum needed for the program to execute soundly in the absence of type checks, but execute unsoundly, perhaps with an error not compliant with the TypeError exception, such as a wasm trap, or simply "keep on trucking" pretending that the type check passed.

[osa1]

Similar issue: #50833.

[osa1]

This is almost exactly what --omit-type-checks is doing today, the only difference is it's not omitting type checks in as.

[lrhn]

Is there any chance we can optimize type checks to not be so expensive? The VM seems to manage it.

That would be better than not actually implementing the Dart language.

[yjbanov]

not actually implementing the Dart language

Let's not allow the perfect to become the enemy of the good. dart2js does not implement numerics correctly, and people use it to create useful programs.

[lrhn]

And the VM implements type checking correctly, and people use it to write efficient programs, even AoT compiled ones. Let's not implement the wrong behavior unless we need to.

I don't know how WASM encodes type information, but if it's so inefficient that it's unusable in practice, maybe we should have put own representation as well, even if it's just a class ID integer on all Dart class instances.

[osa1]

@lrhn We're also working on improving the type checks. We have some plans in #51635 but so far we've done no work to optimize them, --omit-type-checks allowed us to focus on other things so far (such as the standard library performance improvements).

maybe we should have put own representation as well, even if it's just a class ID integer on all Dart class instances

We already do this, and simple cases like x is Y where Y doesn't have generic arguments is a just a sequence of class ID comparisons (x.classID == Y_classId, also comparing subtypes of Y).

[osa1]

This is almost exactly what --omit-type-checks is doing today, the only difference is it's not omitting type checks in as.

I just realized that we actually omit type checks in as as well: https://github.com/dart-lang/sdk/blob/d02097bd1e13da895b17f87ade6e3489c0520400/pkg/dart2wasm/lib/code_generator.dart#L2754-L2757

[sigmundch]

cc @rakudrama

It's fair to say at this point that, if we could, we would remove the "omit-implicit-checks" mode from dart2js. We especially regret how pervasive it is and how hard it is to move away from it. This may be a surprise to Lasse, but we too would like to have a single language semantics 🙂!

One of the ways our customers feel the pain the most is in diagnosing issues. Consider a recent migration to sound null-safety. Checks that were successful with null later failed with sound semantics. But because of the omit-implicit-checks, it was unnoticed at first and caused bizarre downstream unsoundness issues instead.

The cost of removing this mode is too high right now, but we should study how far we can take it. I don't know, to be honest, how the data looks like today on dart2js (especially since we did so much work improving performance of the RTI a few years back), but I'd like to assess it. I also wonder what is the effect on code-size if we had a better closed-world understanding of which checks can be elided.

That aside, we are working to make it less bad. One of the lessons we learned is that a global flag was too coarse-grain. It's too easy to mix good and bad cases together. We think that a large number of the checks we want to eliminate come from our runtime in the SDK and framework code, where we can assure through internal invariants that a check is not needed. This led us to push for a finer-grain approach, where we select to omit checks (and casts) only with an explicit scoped annotation to opt-in. See also: this related comment

That means we should at least understand how many of the typing costs are coming from user code vs framework code to better gauge if this is viable.

@yjbanov - in the benchmark you mentioned above, how many of the expensive as checks come from Flutter's framework vs the benchmark code, for example?

[yjbanov]

@sigmundch

The benchmark is a macrobenchmark. It runs the full framework and exercises production Material 3 widgets, pumping real frames. The run time numbers I quote are chunks of real frame time. So 4473us is indeed 26% of the frame budget. Reducing it to 240us, or 1.4% of the frame budget, has noticeable impact.

This benchmark is easy to run locally:

• From the flutter/flutter repo
• cd dev/benchmarks/macrobenchmarks
• flutter run -d chrome --profile -t lib/web_benchmarks.dart
• Click on bench_material3_scroll_semantics

Also, any other "material3" benchmark can be treated as "macro".

@lrhn

I agree with what you are saying. It's just that we're trying to make more nuanced decision, and I feel like "not actually implementing the Dart language" lacks the nuance. The nuance is that --omit-type-checks does not omit all type checks in the world. It implements is checks and all static type checks, which are likely the vast majority of type checks. The ones it doesn't implement are runtime checks that either pass or crash the program, and so it looks like we have some wiggle room.

[lrhn]

From a language specification perspective there is no wiggle room. Omitting specified checks is just not implementing the language correctly, which means not implementing that language, just a similar one.

It might be useful, even preferable, to implement that other language instead, with the argument that it is the same as Dart for all reasonable programs, and it's more efficient for those reasonable programs.

After all, the type checks are for your own protection, so why not allow a user to ask for performance instead of safety?

The reason it works when compiled to JavaScript is that it's targeting an untyped language. The worst that can happen is a JavaScript error. On the VM, the worst that can happen is an arbitrary code execution security exploit. (Unlikely, but it can crash with a segmentation result, and that should always be considered a potential security issue.)

I don't know where WASM is on the security spectrum. It's probably isolated, since it's running random user code in a browser, so possibly the only thing that can happen is an unexpected Dart error, or a WASM crash.

I'd still prefer to implement the mandatory type checks, and then optimize them if necessary, rather than turning off type soundness.

I do get it, if omitting type checks is currently necessary to get usable performance, then we should implement the best possible type check omitter. And that probably means omitting only casts, not checks that have two live continuations. Meaning:

• implicit downcasts from dynamic
• as casts, in expressions and patterns
• ! casts, ditto
• covariant parameter checks, from declaration or generics
• maybe contravariant return checks, but that's so easy to get wrong, that it probably warrants a runtime check. Also rare.
• maybe an is- or patter- check, where the other branch always throws immediately.

And we can use more unsafeCasts in the platform libraries or patch files, or introduce a similar "omitableCast" that only does nothing in "omit type checks" mode (but we could just use as then).

As an example of what not to remove: the is Future<T> checks in await.

That's all reasonable as an initial implementation strategy, until we have a performance full implementation. But I really, really don't want it to become a permanent fixture, and reason to not optimize type checks.

If the language is too complicated to do type checks efficiently at runtime, maybe we need to change the language and type system. Not just close our eyes and pretend the checks are not there.

[kripken]

Looking at this from the perspective of the Wasm GC spec process and the Binaryen optimizer, is there something we can do in either of those to help here?

I'm also curious how this compares to the overhead of AOT type checks. I can understand that the VM can JIT to avoid many type checks, but I'd expect AOT builds to do a similar amount of them as in wasm, in principle - is that wrong? Or are the AOT checks just much faster than wasm for some reason?

[mkustermann]

I'm also curious how this compares to the overhead of AOT type checks. I can understand that the VM can JIT to avoid many type checks, but I'd expect AOT builds to do a similar amount of them as in wasm, in principle - is that wrong? Or are the AOT checks just much faster than wasm for some reason?

Since we haven't spent much time optimizing dart2wasm type checks, it's simple too early to conclude anything, compare against AOT or suggest we should omit them entirely. => We should first optimize them.

We do have a different representation of types in the object layout in the VM compared to wasm, so even after optimizing the type checks in wasm, there'll be some differences between VM and wasm (some operations may be faster and some slower than the VM).

On a very low level, the VM has obviously the advantage of compiling directly to machine code - so one isn't constrained by wasm types (e.g. can have a struct with variable-length data that follows it) or accesses (e.g. can omit bounds checks if it's guaranteed to succeed). But this probably doesn't make a huge difference.