Clarification for ref.test instruction

[konsoletyper]

According to spec, type system is nominal. At least, spec for ref.test (found in document/core/exec/instructions.rst) claims following:

8. If the :ref:`reference type <syntax-reftype>` :math:`\X{rt}_2` :ref:`matches <match-reftype>` :math:`\X{rt}_1`, then:

Whereas match-reftype leads to match-heaptype, which in turn leads to match-deftype, which claims following:

* Either :math:`\deftype_1` and :math:`\deftype_2` are equal when :ref:`closed <type-closure>` 
  under context :math:`C`.

* Or:

  * Let the :ref:`sub type <syntax-subtype>` :math:`\TSUB~\TFINAL^?~\heaptype^\ast~\comptype` 
     be the result of :ref:`unrolling <aux-unroll-deftype>` :math:`\deftype_1`.

  * Then there must exist a :ref:`heap type <syntax-heaptype>` :math:`\heaptype_i` in :math:`\heaptype^\ast`
     that :ref:`matches <match-heaptype>` :math:`\deftype_2`.

However, explanation states that dynamic casts are made structurally. Also, I found tests that approves this (namely, this one).

I also saw match-comptype section in matching.rst, but it's never referred from exec/instruction.rst (but rather in validation sections that describe how subtyping is validated).

I tried to use ref.test with my Java-to-Wasm compiler in order to reduce binary size, in favour of functions that check type hierarchy of class objects, and it looks like both Chrome and Firefox behave not like spec states (or at least how I understand it), but how tests describe. I.e. given following declarations

(; 000002d6 ;)    (type (; 46 ;) $org.teavm.vm.SwitchTest$Superclass (sub (; 1 ;) $java.lang.Object 
(; 000002d6 ;)      (struct 
(; 000002d8 ;)        (field (; 0 ;) $class (mut (ref null (; 6 ;) $java.lang.Class)))
(; 000002db ;)        (field (; 1 ;) $monitor (mut eqref))
(; 000002dd ;)        (field (; 2 ;) $x (mut i32))
                    )
                  ))

(; 00000509 ;)    (type (; 72 ;) $org.teavm.vm.SwitchTest$SubclassB (sub (; 46 ;) $org.teavm.vm.SwitchTest$Superclass 
(; 00000509 ;)      (struct 
(; 0000050b ;)        (field (; 0 ;) $class (mut (ref null (; 6 ;) $java.lang.Class)))
(; 0000050e ;)        (field (; 1 ;) $monitor (mut eqref))
(; 00000510 ;)        (field (; 2 ;) $x (mut i32))
                    )
                  ))

(; 00000863 ;)    (type (; 170 ;) $org.teavm.vm.SwitchTest$SubclassA (sub (; 46 ;) $org.teavm.vm.SwitchTest$Superclass 
(; 00000863 ;)      (struct 
(; 00000865 ;)        (field (; 0 ;) $class (mut (ref null (; 6 ;) $java.lang.Class)))
(; 00000868 ;)        (field (; 1 ;) $monitor (mut eqref))
(; 0000086a ;)        (field (; 2 ;) $x (mut i32))
                    )
                  ))

and following code

(; 00001124 ;)                      ref.test (ref (; 170 ;) $org.teavm.vm.SwitchTest$SubclassA

where I know that at the stack top is $org.teavm.vm.SwitchTest$SubclassB, I get 1 at the top after execution of this instruction.

So my question is: is it a mistake in spec or bug in two separate WebAssembly implementations? And how would I work around it? Note that using ref.test instead of checking attached class objects (where possible) significantly reduces binary size. If it was something like TypeScript, I'd turned structural types into nonimal using following trick:

interface Superclass {
  readonly __typeMarker__: string
}
interface SubclassA {
  readonly __typeMarker__: "A"
}
interface SubclassB {
  readonly __typeMarker__: "B"
}

but in case of WebAssembly, if I add a such field, it would also be matched structurally, making this trick impossible.

[fgmccabe]

WebAssembly's type system is not nominal. It is, in fact, based on an iso-recursive structural typing.

[konsoletyper]

@fgmccabe Yes, but on the early stages of engineering my compiler I also read overview without deep diving into spec (except for binary format sections) and did not generate recursive types, supertypes, etc, and such modules simply failed to validate, because

(struct 
  (field (mut i32))
  (field (mut i32))
)

simply did not match

(struct 
  (field (mut i32))
)

even at validation level

[rossberg]

Wasm requires subtyping to be pre-declared (the correctness of which is validated with the match-comptype relation), but that does not imply that it is nominally typed: two types are equivalent if they have the same structure and have declared supertypes that also both have the same structure (which is what the spec quote specifies).

The primary purpose of type hierarchies and casts in Wasm is to escape the limitations of Wasm's static type system, rather than to (directly) encode source-level casts. The latter is highly language-dependent, so no single type system built into Wasm would be able to suite more than one specific languages (for example, considering the details of subtyping on arrays, generics, multiple inheritance, interfaces, nominality, etc). A language with a dynamic type mechanism is expected to implement that itself when compiling to Wasm, just like it would have to when compiling to native code. Sometimes Wasm's casts can provide certain shortcuts, but they cannot possibly cover the generality of a languages-specific system.

[konsoletyper]

two types are equivalent if they have the same structure and have declared supertypes that also both have the same structure (which is what the spec quote specifies).

ok then. But then I simply don't understand how the spec reflects that. Once more:

Let the sub type sub final? heaptype* comptype be the result of unrolling deftype_1
Then there must exist a heap type heaptype_i in heaptype* that matches deftype_2

For me reads as follows: deftype_2 either presents among supertypes (denoted at heaptype*) or we can apply recursively some of parents of deftype_2. Or did I miss something?

The primary purpose of type hierarchies and casts in Wasm is to escape the limitations of Wasm's static type system, rather than to (directly) encode source-level casts.

I understand that. For example, there's no way to encode Java interfaces, so I have slow/bit casts anyway. But for classes it seemed obvious to rely on Wasm ref.test for performance reasons (I used the same trick in JavaScript backend). Also, I thought WebAssembly claims performance and binary size among its priorities, but it turns out that I have to insert my own null checks, my own casts, my own runtime type tags, in addition to existing ones, just to implement virtual calls, catch and re-throw exceptions in every try/catch handler, etc. So according to my experiments, minified JavaScript still wins in its binary size (though, not dramatically, as it is with WebAssembly without GC spec).

[rossberg]

For me reads as follows: deftype_2 either presents among supertypes (denoted at heaptype*) or we can apply recursively some of parents of deftype_2.

Yes. But "be present" here means "is structurally the same". Which in turn means that all their supertypes are structurally the same, because they are part of the type's structure.

I thought WebAssembly claims performance and binary size among its priorities.

The former but certainly not the latter. Wasm is a low-level assembly language. As such, it will almost necessarily require more code than a high-level language like JavaScript with expressive (but complex) features. Even more so when compiling high-level language constructs that happen to be directly similar to something in the latter.

[konsoletyper]

But "be present" here means "is structurally the same"

Ah, I finally found this. It was the thing I did not notice initially:

 when :ref:`closed <type-closure>`   under context :math:`C`

where "closed" means "references substituted by defined types". Then it makes sense.

certainly not the latter

Strange. I think I saw size among priorities when first met WebAssembly in 2017. For example, this LEB encoding instead of word-aligned instructions like in ARM certainly slows down loading, so I thought it's due to goal "small binary size". Anyway, it's not only the size, but also performance. If I were emitting machine code, I could have optimized my casts with speculative runtime magic, but in case of WebAssembly I have to always emit slow path code. But I believe v8 and Spidermonkey engineers have implemented this magic under the hood (or at least are going to), so I would rely on native WebAssembly features when possible.

As such, it will almost necessarily require more code than a high-level language like JavaScript with expressive (but complex) features

Strange. JavaScript certainly a bit more high level, but WebAssembly is also high level enough to hide stack, registers, irreducible CFGs, memory protection, etc, under the hood and it operates even in terms of structures that are garbage collected. Also, JavaScript has much more verbose encoding compared to WebAssembly. To me it was surprising that JavaScript wins in terms of binary size. I'll dig a bit deeper eventually and perhaps even present report, but for now it seems that one thing that influences the size is need to set types to locals. In JavaScript I can simply join all variables with non-interfering live ranges into single JavaScript, but in WebAssembly I also have to take care of types, so this optimization is often not possible.

[rossberg]

To clarify, I didn't imply that size is not a consideration, but that it isn't a priority. Certainly not the same as safety, performance, portability, and language neutrality. Where not in conflict with other goals, we still try to minimise size of representations, of course.

In the early days of Wasm we considered adding a layer of custom compression to the binary format — essentially a way to define per-module instruction macros. But that never came to fruition, because it wasn't clear whether it would be significantly better than plain zipping, without a lot of work for both producers and consumers.

Some aspects of Wasm are somewhat more high-level than a real machine language. Usually, that's for safety or portability reasons. Yet the overall goal is to be a virtual ISA, as low-level as possible, in order to achieve lightweight runtimes, direct mappings to machine code, and language neutrality. Wasm certainly is nowhere close to the level of semantic complexity of a Java or JavaScript, nor should it be.

[tlively]

Note that using ref.test instead of checking attached class objects (where possible) significantly reduces binary size. If it was something like TypeScript, I'd turned structural types into nonimal using following trick...

The analogous trick in WebAssembly is to put the structurally identical types into the same recursion group, which forces them to be separate types. This only works when the compiler sees the whole program and knows what types to put into the same rec group, though.

[konsoletyper]

Oh, thanks for the tip, I'll try this. However, I still don't understand why this trick would work, as well as the whole thing with there recursive groups, rolling/unrolling, etc.

[konsoletyper]

Thanks, that helped! I tried this and now tests pass even with optimization to casts. However, this makes problem for another optimization for binary size I made: calculate usages of types and place most frequently used ones first. Grouping structures in mutually recursive group makes impact of such optimization a bit less. Still, enabling this grouping together with reliance on WebAssembly test/cast instructions size by a very small amount. For example, with Java regex tests sizes are following:

1. Original (slow casts, no structure grouping): 198302 bytes
2. Optimized (native casts, grouping enabled): 198113 bytes
3. Invalid (native casts, grouping disabled, some tests fail): 195444 bytes

Unfortunately, I can't make any benchmarks right now.

[tlively]

Have you looked into using wasm-opt to optimize your modules? There's a guide to optimizing WasmGC modules here: https://github.com/WebAssembly/binaryen/wiki/GC-Optimization-Guidebook.

[konsoletyper]

@tlively I tried, but got validation error from wasm-opt.

[tlively]

Please file bugs if you haven't already!