Relation to NaN non-determinism

[RalfJung]

This proposal emphasizes heavily that it introduces non-deterministic instructions. This makes it sound like non-determinism is a new concept that was otherwise not found in wasm. This is surprising to me since in my understanding, wasm already contains non-deterministic instructions. Specifically, the behavior of NaNs is explicitly documented as non-deterministic:

Otherwise the payload is picked non-deterministically among all arithmetic NaNs; that is, its most significant bit is 1 and all others are unspecified.

Am I misunderstanding something? If not, it might be worth clarifying that, and also clarifying whether these are "the same kind" of non-determinism or not.

[rossberg]

The text is perhaps somewhat confusing. What it's getting at is that this proposal introduces a new class of non-determinism that we did not have before, namely one that is more accurately understood as implementation-dependent behaviour. With NaNs before, the choice is always independently arbitrary and can differ on every execution; the spec didn't guarantee any semantics that could vary across implementation. With relaxed SIMD there are some guarantees that the behaviour is basically deterministic for a given "environment" (which is a rather hand-wavy notion, as you note in #153).

In other words, the spec now officially supports and blesses probing for and depending on "non-deterministic" behaviour. Of course, that is rather unfortunate, because it adds complexity to the specification and undermines portability, which is why it is called out.

[RalfJung]

In other words, the spec now officially supports and blesses probing for and depending on "non-deterministic" behaviour. Of course, that is rather unfortunate, because it adds complexity to the specification and undermines portability, which is why it is called out.

Okay, I see. Thanks for the clarification. The first example in the overview for this proposal ("given the same inputs, two calls to the same instruction can return different results") very much reads like the kind of non-determinism NaNs have, so I think it'd be good to clarify this. I guess it is too late to eschew "non-determinism" for some other term like "environment-dependent behavior"? (Or that idea was already considered and discarded.)

[rossberg]

Not too late to improve the explaner, but technically it still amounts to non-determinism, only of a more complicated form (vectors of sets of behaviours instead of just sets of behaviours, and the projection function is arbitrary).

[RalfJung]

vectors of sets of behaviours

I admit I didn't get that part of the overview at all.

Using a choice: () -> bool function as an example since it is easier to discuss:

To me what you describe sounds like: "When choice executes, check a write-once global cache (of type Option<bool>) for whether we already made a choice. If yes, use that choice. If no, make a non-deterministic choice, record the result in the cache, and use that for this operation."

Or, equivalently: initialization of the Abstract Machine is non-deterministic. When the AM is initialized, non-deterministically pick a bool and store it in the global state. This part of the state is immutable from now on. Whenever choice is executed, return the value stored in the global state.

So yes, this "amounts to non-determinism", in the sense that non-determinism is somehow involved. But summarizing that as "choice is non-deterministic" is rather misleading! It's not wrong, but it's leaving away some important aspects of choice. This operation described above is obviously very different from the normal non-deterministic choice, and using the same name for both is bound to cause confusion. (In Rust we'll probably call this "implementation-specific behavior" or something like that.)

But what does any of this have to do with vectors of sets of behaviors...?

[rossberg]

Yes, except that Wasm deliberately has no notion of "initialization of the abstract machine", and it's not at all clear what that would mean, i.e., when it would happen, or whether it could happen repeatedly, e.g., when code is persisted.

But what does any of this have to do with vectors of sets of behaviors...?

The choice function returns an index into a vector of allowed non-deterministic behaviours. And in fact, we have separate choice functions for different groups of operations, with varying index range. It's all pretty messy...

[RalfJung]

The choice function returns an index into a vector of allowed non-deterministic behaviours.

You mean this: IMPLEMENTATION_DEFINED_ONE_OF(0, INT32_MIN)? In my reading of the document, that's just listing the options that we are "non-deterministically" picking from, it doesn't clarify in any way when and how that choice happens.

IOW, the "vector" seems to be just the usual list that comes out of the non-determinism monad. Where are "vectors of sets of behaviors"?

Btw, the "modified spec" link at https://webassembly.github.io/relaxed-simd/ (found on the root README of this repo) is broken.

Yes, except that Wasm deliberately has no notion of "initialization of the abstract machine", and it's not at all clear what that would mean, i.e., when it would happen, or whether it could happen repeatedly, e.g., when code is persisted.

Well that relates to the question about "the environment" then. That very much sounds like such an initialization in disguise -- the AM is initialized when "the environment" is fixed.

[rossberg]

No, that's not what it is. It rather works along the lines of

IMPLEMENTATION_DEFINED_ONE_OF([
  NONDETERMINISTIC_ONE_OF(X1, Y1),
  NONDETERMINISTIC_ONE_OF(X2, Y2),
  NONDETERMINISTIC_ONE_OF(X3, Y3),
])

Thus a vector of sets of possibilities. I truly wish it was simpler, and that we could have gotten away with just plain sets, but SIMD champions argued this extra guarantee was important.

I agree that the question of "fixing" the environment is rather fuzzy. In the respective discussions the conclusion was that code mobility is not an issue Wasm needs to be concerned with yet (which I suspect may be naive). As far as the observable semantics is concerned, the "environment" hence is fixed upfront and forever for any given program -- you just can't tell in advance what it is.

[RalfJung]

No, that's not what it is. It rather works along the lines of

Oh I see, there are nested choices. That didn't become clear to me from reading the "overview", there's no NONDETERMINISTIC_ONE_OF there. Where can I find NONDETERMINISTIC_ONE_OF?

Is NONDETERMINISTIC_ONE_OF "truly non-deterministic at runtime" and IMPLEMENTATION_DEFINED_ONE_OF "depends on the environment"?

the "environment" hence is fixed upfront and forever for any given program -- you just can't tell in advance what it is.

In other words, it is fixed when the AM is initialized? ;)

Since obviously I can run the same program in different environments and then it will see different choices.

[rossberg]

Where can I find NONDETERMINISTIC_ONE_OF?

That just is the form of nondeterminism we already have in Wasm 1.0/2.0.

Neither operator exists in the actual spec, I believe that's just an explanatory device in the overview.

(I just had another look at the relaxed SIMD spec draft, and to be honest, what it specifies is still lacking. It defines the vectors of non-deterministic sets for numeric primitives, but fails to connect that to the execution of instructions in a formal manner.)

Is NONDETERMINISTIC_ONE_OF "truly non-deterministic at runtime" and IMPLEMENTATION_DEFINED_ONE_OF "depends on the environment"?

In reality, both may be implementation-dependent choices, but for the former there are zero guarantees of reproducability, while the latter choice is guaranteed to be fixed for each run (which is what causes all the headache).

In other words, it is fixed when the AM is initialized? ;)

Since obviously I can run the same program in different environments and then it will see different choices.

Sure, but initialisation is not an observable step, nor is the AM itself an observable entity. You can pretend the choice was made with the big bang. Semantically, it's more appropriate to think of it as (a set of) global constants/parameters (one for each relaxed operator) whose values are unknown.

AFAICS, there is no meaningful way to make it more precise without hardcoding assumptions about Wasm that may not work for all implementations (e.g., any specific notion of engine initialisation).

@ngzhian, @Maratyszcza, can one of you fix the spec build on this repo, such that it shows up on github.io?

[RalfJung]

That just is the form of nondeterminism we already have in Wasm 1.0/2.0.

Okay, so "normal" non-determinism then, I assume.

Neither operator exists in the actual spec, I believe that's just an explanatory device in the overview.

Ah, well that explains why I didn't find them.^^ Can you point me at a place in the spec where both of these kinds of choice appear so that I can see how this is phrased in the spec? I don't know my way around wasm and so far I wasn't able to find any part of the "relaxed SIMD" spec apart from the overview...

It seems that "swizzle" is an example of such a relaxed operation, and I found this, but I don't see where this says anything about the kinds of choices that are permitted, so maybe this is the wrong place... or maybe I just can't read those macros.

Is there a "diff" to the main spec somewhere?

I think it would be very helpful if this was presented the way you just did, with two different explicitly named "choice" functions. Instead of saying "This proposal introduces non-deterministic instructions", the introduction could then say something like "This proposal introduces instructions that make implementation-defined choices, complementing the existing concept of instructions that make non-deterministic choices. To clearly distinguish these two, we write them in pseudocode as IMPLEMENTATION_DEFINED_ONE_OF and NONDETERMINISTIC_ONE_OF, respectively."

[rossberg]

Can you point me at a place in the spec

Well, as I just mentioned, a proper definition of this appears to be still missing from the draft spec. All I see so far are a couple of informal sentences here, but we'll need more than that.