Problems for deferred loading

[RossTate]

In #220 (comment), @rossberg claimed that Java/C#'s linking was unsound due to their use of nominal types. Here I'll illustrate that the "unsoundness" is actually due to their use of and support for deferred loading. By deferred loading, I mean deferring loading/validating/compiling parts of a program to some time after the program has begun executing, say in order to achieve faster response time or to reduce resource consumption. There is a connection to mutual recursion in that support for deferred loading makes support for (sound) mutual recursion very easy, but I follow up on that specific point in #220 (comment). There is also a connection to nominal vs. structural typing, or more specifically type canonicalization, in that deferred loading does not work well with things like rtt.canon, which I'll illustrate here.

To elaborate on deferred loading, consider the following (Java) class:

package my.code;
import someone.else.Bar;

public class Foo { private Bar b; }

The question is, does class someone.else.Bar need to be loaded (e.g. fetched), compiled, and linked before we can compile my.code.Foo? In systems that support deferred loading, the answer is generally "no", at least supposing someone.else.Bar is at least a reference type (I won't go into the more complicated things with C#'s struct types).

This is perfectly sound. All code using Foo is guaranteed to respect the invariant that only Bar instances (and null) are ever assigned to the field b even without knowing what it means to be a Bar instance. We could add methods like Bar getb() { return b; } and void setb(Bar b) { this.b = b; } and still compile these methods before loading Bar. If this were Go, we could set up complex data structures with interior *Bar pointers to fields of Foo instances, without loading Bar, and be assured that—once Bar gets loaded and defined—those *Bar pointers will respect that definition.

The key for supporting deferred loading (of types) at the low level is to separate type declaration from type definition. That way a linker/loader can just "declare" the type my.code.Bar, without defining it, then pass that declared type as a type import for my.code.Foo, which can in turn use that imported type in its definition of my.code.Foo and its relevant code/methods. Or, more precisely, in its relevant code/methods that treat it abstractly. But eventually something will need to treat the type more concretely, by which point the linker/loader will need to actually load the code intended for my.code.Bar, compile it, and instantiate it in order to get a definition for the type my.code.Bar. When and how that happens is a matter of policy; the Java Language Specification indicates this must be done on demand, e.g. the exact time a field of my.code.Bar first gets access, but there are many other policies, e.g. load in parallel and link once available. In my opinion, a good design for WebAssembly would not standardize a policy but instead provide the means for programs to implement their own policy.

For example, one could compile my.code.Foo to a WebAssembly module that imports not just the type for someone.else.Bar, but also the type for my.code.Foo and the (linear) (not first-class) capability/obligation to define the type for my.code.Foo—this way the module could itself be loaded after some other module abstractly using the type my.code.Foo has already started executing. Then, if someone wanted to use this module in eager-loading setting, they could simplify specify a module that declares the types for both someone.else.Bar and my.code.Foo and passes the types and the definition-capabilities to the relevant modules—all of this would resolve and validate statically, so there's no loss of guarantees for the eager case. But if someone wanted to use this module in a deferred-loading setting, their loader system (written in, say, the JS API) could declare the two types, pass them and the appropriate definition-capability to the my.code.Foo module, and wait until later to load the module for someone.else.Bar and pass it the appropriate types and definition-capability. Of course, when that time comes, something could go wrong: the code for someone.else.Bar may turn out to be missing or have some error. In this case, the person would specify (again, in the JS API or the like) what to do—for Java, the appropriate thing to do would be to throw a NoClassDefFoundError at whatever point in the code prompted someone.else.Bar to be loaded. This is the "unsoundness" that @rossberg alluded to. But none of this makes WebAssembly unsound—it's just to-be-expected dynamic "errors" in someone's custom-written deferred-loading code.

Now, for this to work well, it is very important that type imports be treated abstractly. That way code behaves correctly regardless of whether the type is still undefined or of how it gets defined. This is where rtt.canon (and the like) becomes problematic—it looks past the type import and digs up the type definition in order to determine which rtt to return. What happens if, in the module for my.code.Foo, one asks for the rtt.canon of the imported type for someone.else.Bar that is still undefined? Or if one asks for the rtt.canon of the type definition of my.code.Foo, which is defined in terms of the still-undefined someone.else.Bar? We could make rtt.canon trap in these cases, but that still means that programs wanting to use deferred loading (of types) cannot utilize rtt.canon. On the other hand, instructions like rtt.fresh do respect type abstraction and can be used even when part of the relevant type is a type variable (unknowingly) representing a (presently) undefined typed.

I haven't gone into more advanced use cases, such as letting the module for my.code.Foo defer the compilation of a method like double getxofb() { return b.x; }—which accesses a field of Bar—until after (the relevant parts of) someone.else.Bar has been loaded. I believe staged modules, where imports/definitions/exports have stages associated with them so that the whole module does not have to compiled/instantiated all at one, would be a good fit for this (as, again, they are sound and do not force any particular loading policy), but I suggest deferring discussion of these more advanced use cases to a later time, understanding that they would be well served by the concepts above.

[rossberg]

In #220 (comment), @rossberg claimed that Java/C#'s linking was unsound due to their use of nominal types.

I did not claim that. I said that recursive linking with nominal types in Java/C# works because they accept unsafe linking. Deferred loading indeed is the key here: the recursive linking semantics relies on the ability to defer loading (and thus checking), plus, a sort of global name space for class names. In Wasm we have neither.

Moreover, the "unsoundness" (I didn't actually use that word, Java semantics is sound due to dynamic checks, it just isn't statically type-safe) I'm referring to is not the possibility of a NoClassDefFoundError, but the possibility of NoSuchMethodError and NoSuchFieldError exceptions, both of which are directly due to the lax linking semantics. Concretely, when you have classes A and B, and B uses a field or method from A, then you have no guarantee that this succeeds at runtime. Because you have no guarantee that the A you actually load has any resemblance to the A you compiled against -- that is not checked! B will successfully load A, access and call into A many times, and may still fail later during the same run when it hits an actual mismatching access.

Standard example:

// A.java
class A {
  public void lock() {}
  public void release() {}
};

// B.java
import java.lang.System;
class B {
  public static void main(String[] args) {
    A a = new A();
    System.out.println("1");
    a.lock();
    System.out.println("2");
    a.release();
    System.out.println("3");
  }
};

Compile A, compile B, run B. All fine. Now notice that you prefer the method name unlock over release for symmetry. Change A, recompile A, but forget to recompile B. Here is what you'll see when you run B again:

1
2
Exception in thread "main" java.lang.NoSuchMethodError: 'void A.release()'
	at B.main(B.java:8)

It's folklore knowledge that, as far as the class system is concerned, Java essentially is a dynamically-typed language. Hence we cannot expect its compilation model to map onto Wasm modules without casts, at least not without restricting the semantics.

[RossTate]

I did not claim that. ... "unsoundness" (I didn't actually use that word, Java semantics is sound due to dynamic checks, it just isn't statically type-safe)

Sorry, I often put quotes around formal terms I'm aware I'm using very handwavily, which in this case was a poor choice because it comes across as a direct quotation from the referenced comment. I chose that term because it's concise and because I recalled you using it in meetings to describe Java linking. But you're right that you did not use it in that specific comment.

I said that recursive linking with nominal types in Java/C# works because they accept unsafe linking.

I will respond to this in the appropriate thread shortly (where we are otherwise waiting for you to respond to our requests to improve your example). The short is that, as pointed above, the "unsoundness" issue has nothing to do with nominal types and is entirely due to support for deferred loading. Java could just as easily load everything eagerly and trap if there are any mismatches (while still using a nominal type system) rather than letting the program run as long as it can until a mismatch is necessarily problematic (e.g. a NoSuchMethodError or a NoSuchFieldError).

To keep this discussion focused, please refrain from discussing mutual recursion here (as I did above).

---

This post is about (lack of) support for deferred loading (specifically of type definitions). I illustrated how we could enable an application to implemented their own deferred loading policy (in, say, the JS API) by separating type declaration and type definition. But I also illustrated how this would be problematic for rtt.canon. Those are the topics of this thread. Do you have anything to add on topic (rather than on mutual recursion, which is the topic of #220)?

[rossberg]

The short is that, as pointed above, the "unsoundness" issue has nothing to do with nominal types and is entirely due to support for deferred loading. Java could just as easily load everything eagerly and trap if there are any mismatches (while still using a nominal type system) rather than letting the program run as long as it can until a mismatch is necessarily problematic (e.g. a NoSuchMethodError or a NoSuchFieldError).

No it can't, not without fundamental, presumably incompatible, changes to its type, class, loader, and compilation system. Its existing semantics of recursive linking deeply depends on deferred checks.

To keep this discussion focused, please refrain from discussing mutual recursion here (as I did above).

Hm, you create an issue in reply to a quote I made about recursive linking which you now say is unrelated and tell me to not reply to your misinterpretation of that quote? What is the point you want to make anyway?

[RossTate]

Quoting from WebAssembly/meetings#795:

• Keep conversations focused
  Threads have different purposes such as brainstorming, bikeshedding,
  consensus seeking, etc. Create new threads for new topics or new purposes
  of discussion.

I recognized that, although there is a relationship between deferred loading and mutual recursion, it would be worthwhile to discuss deferred loading separate from mutual recursion (and then reference that in the mutual recursion thread). I gave an introduction here to give context for the discussion, such as the connection to mutual recursion while also making it clear that elaborations on that connection would be conducted in the appropriate thread, and then made a proactive effort to make sure that everything past that introductory context is not on mutual recursion.

What is the point you want to make anyway?

Quoting from above:

This post is about (lack of) support for deferred loading (specifically of type definitions). I illustrated how we could enable an application to implemented their own deferred loading policy (in, say, the JS API) by separating type declaration and type definition. But I also illustrated how this would be problematic for rtt.canon. Those are the topics of this thread.

Do you have anything to add on topic? (Your comment above is on mutual recursion, and so I'll refrain from correcting it in order to keep this discussion focused on the topic of deferred loading.)

[sjrd]

No it can't, not without fundamental, presumably incompatible, changes to its type, class, loader, and compilation system. Its existing semantics of recursive linking deeply depends on deferred checks.

Perhaps if you want to preserve the liberty of dynamically loading classes through a class loader. But if you accept to get rid of class loaders, one can definitely statically, eagerly link a Java classpath while preserving its type system and class sytem. That's what all existing compilers from JVM languages to JS do. And they can statically report linking errors.

[rossberg]

@RossTate:

Do you have anything to add on topic?

Well, I'm at a loss what exactly the topic is. Clearly, a type-checking linking mechanism cannot support deferral without the use of casts. You don't even have a concrete type at hand before linking its defining module, so what would an RTT even be referring to? Once you actually need to access a class, and you'll need to load the module, which also gives you access to the concrete type and their RTTs if needed and allow you to perform a suitable downcast.

But you seem to be pondering over a rather different setting, and again I can't help the impression that it's based on various hypotheticals and assumptions that have little to do with how Wasm works today.

[rossberg]

@sjrd, I agree, if you only care about whole-program linking at a single point of control, then you can work around the limitation. However, Wasm's module system is supposed to support layering and incremental linking (see e.g. the module-linking proposal), and then the approach of inverting dependencies already falls apart.

[RossTate]

Clearly, a type-checking linking mechanism cannot support deferral without the use of casts. You don't even have a concrete type at hand before linking its defining module, so what would an RTT even be referring to?

Quoting from the OP's paragraph on rtts:

On the other hand, instructions like rtt.fresh do respect type abstraction and can be used even when part of the relevant type is a type variable (unknowingly) representing a (presently) undefined typed.

To clarify, rtt.fresh works even if the type you're creating a fresh rtt for is itself a type variable (unknowingly) representing a (presently) undefined typed.

---

Well, I'm at a loss what exactly the topic is.

Quoting from above (again):

This post is about (lack of) support for deferred loading (specifically of type definitions). I illustrated how we could enable an application to implemented their own deferred loading policy (in, say, the JS API) by separating type declaration and type definition. But I also illustrated how this would be problematic for rtt.canon. Those are the topics of this thread.

If it helps to offer more direction, one thing I would appreciate you contributing on the above topics is confirmation or denial that, whereas rtt.fresh can work with still-to-be-defined types, rtt.canon would not work well. Or, similarly, it would be useful for you to illustrate how you would support the deferred-loading example in the OP (ideally extended with the methods getb and setb) so that we could get insight into your plan for deferred loading.

[tlively]

@RossTate, I think it would help to make this discussion more concrete if you could share an example WebAssembly program demonstrating the split you have in mind between type declarations and definitions and how that split enables safe deferred loading.

[RossTate]

Sure thing. How advanced of an example do you think would be useful? Or do you have an example Java-ish class and deferred-loading policy whose compilation you would find illuminating? (Depending on what functionality it has, I might have to provide a sketch of staging.)

P.S. I'm off tomorrow, so I probably won't be able to provide a compilation until Friday.

[tlively]

Let's start simple and take it from there :) The class Foo you used in the OP along with the getb() and setb() methods and a separate module defining Bar to be loaded eagerly or lazily might be good. No rush, of course!

[RossTate]

Got it. That I could write it up real quick, so here's the "surface" code for Foo:

import Bar;
public class Foo {
    private Bar b;
    public Foo() { b = null; }
    public Bar getb() { return this.b; }
    public void setb(Bar b) { this.b = b; }
}

Here's the WebAssembly module for Foo (apologies for syntactic errors):

(module $Foo
    (type $Bar (import "Bar"))
    (global (import "__Bar_rtt") (rtt $Bar))
    (define-type $Foo (import "Foo")
        (struct
            (field $vtable (ref $FooVTable))
            (field $b (mut (ref null $Bar)))
        )
    )
    (global (import "__Foo_rtt") (rtt $Foo))
    (type $FooVTable
        (struct
            (field $getb (func (param $this (ref $Foo)) (result (ref null $Bar))))
            (field $setb (func (param $this (ref $Foo)) (param $b (ref null $Bar))))
        )
    )
    (func $Foo.getb (param $this (ref $Foo)) (result (ref null $Bar))
        (struct.get $b (local.get $this))
    )
    (func $Foo.setb (param $this (ref $Foo)) (param $b (ref null $Bar))
        (struct.set $b (local.get $this) (local.get $b))
    )
    (global $__Foo_vtable_rtt (rtt $FooVTable) (rtt.fresh $FooVTable))
    (global $__Foo_vtable (ref $FooVTable) (struct.new_with_rtt (global.get $__Foo_vtable_rtt) (ref.func $Foo.getb) (ref.func $Foo.setb)))
    (func (export "__new_Foo") (result (ref $Foo))
        (struct.new_with_rtt (global.get $__Foo_rtt) (global.get $__Foo_vtable) (ref.null $Bar))
    )
    ... ;; exports of the relevant field references for the methods $getb and $setb
)

The definition of Bar is not particularly important; what matters is that its module would roughly have the following shape:

(module $Bar
    (define-type $Bar (import "Bar") ...)
    (global (import "__Bar_rtt") (rtt $Bar))
    ...
)

If one were to link these statically, the glue module would look like the following:

(module $__glue
    (declare-type $Foo)
    (global $__Foo_rtt (rtt $Foo) (rtt.fresh $Foo))
    (declare-type $Bar)
    (global $__Bar_rtt (rtt $Bar) (rtt.fresh $Bar))
    (instance $Foo (import "Bar" (type $Bar)) (import "__Bar_rtt" (global.get $__Bar_rtt)) (import "Foo" (type $Foo)) (import "__Foo_rtt" (global.get $__Foo_rtt)))
    (instance $Bar (import "Bar" (type $Bar)) (import "__Bar_rtt" (global.get $__Bar_rtt)))
    ...
)

Important here is that declare-type and define-type are complementary. To validate $__glue, the type-checker ensures that each declare-type is given to (at most) one define-type (import).

For deferred loading, the JS API would have some WebAssembly.declareType() function that declares (but does not define) a type. The JS wrapper of that type is guarded by a boolean that makes sure that it is (dynamically) given to at most one definable-type import. Similarly there would be some WebAssembly.rttFresh(Type) function that generates a fresh rtt. A deferring loader for this example would call WebAssembly.declareType() twice to get jsBar and jsFoo, passes each of those to WebAssembly.rttFresh, and then passes jsBar and jsFoo and the generated rtts as imports to instantiate $Foo (without having loaded $Bar). When $Bar eventually gets loaded, the loader would then pass jsBar and its previously generated rtt as imports to instantiate $Bar.

I'm aware I'm sweeping a few things under the rug, but what remains should be all boilerplate or uninteresting for the discussion, and the example is already long as is.

[tlively]

I personally haven't had the bandwidth to read and understand this sample code yet, and I'm guessing that others are in the same boat. Perhaps a walk through of this example and discussion of its implications would be a good candidate for an upcoming meeting.

[RossTate]

Looks like I have enough time to make slides for this. I'll plan on just doing enough to give context on deferred loading, then focus on specifically deferred loading of types, giving this example using declare-type and define-type. Shouldn't take long (10 min?).