Is it spec-compliant to const-fold and -propagate non-deterministic instructions?

[fitzgen]

Forgive me if I just missed the relevant bits¹, but reading through the spec, it isn't 100% clear to me whether constant folding and propagation through non-deterministic instructions is spec-compliant.

The "risk" here is that Wasm could observe whether these optimizations happened or not if

• the wasm is compiled on a machine that has native support for fma (for example)
• the wasm is evaluated on a machine that does not

Or alternatively, maybe the compiler's compile-time evaluation of the fma is in software, but runtime-evaluated fmas use the hardware, and these two implementations have different behavior (that are each individually spec-compliant).

Basically: is it spec-compliant if two instances of the same instruction make different choices of how to evaluate a non-deterministic instruction?

I see https://github.com/WebAssembly/relaxed-simd/blob/main/document/core/exec/numerics.rst#relaxed-operations which seems to suggest the answer is "no, the above optimizations are not spec-compliant" because it says that operations are "fixed to one particular choice by the execution environment". However, looking at the semantics of fma in particular there is no spec machinery there that fixes these choices across the whole execution environment, as far as I can tell.

Thanks in advance for the clarification!

Footnotes

1. It was kind of hard to look through the spec for this stuff, because for whatever reason, the built and rendered version of the modified spec isn't available anymore (if it ever was?) and so I was browsing through the spec sources on github's UI. Might be something one of the champions is interested in fixing, at least until this proposal is merged into the main spec and we can view the relevant, rendered bits there. ↩

[rossberg]

That is not allowed, unless constant folding is guaranteed to implement the same semantics as execution on the host machine. This is a consequence of the new form of non-determinism introduced by this proposal which essentially codifies implementation-dependent behaviour, and guarantees that to be consistent across all executions of the same class of instruction.

That specifically means that offline tools like Binaryen cannot correctly (i.e., in a semantics-preserving manner) perform such optimisations, since they do not know the target architecture's behaviour.

I don't remember if that issue was discussed specifically, but it is a (simpler) instance of the general phasing problem that was discussed, the more hypothetical scenario of code mobility: if a Wasm program is partially executed on one machine, and then hibernated and later resumed on another machine/engine, then that would only be legal if the implementations made sure they both implement the exact same behaviour. In practice, that might be impossible to achieve.

My impression is that we still do not properly understand the implications of this fundamental change to Wasm and its effect on portability and the meaning of program execution. It is too loose to constrain implementations sufficiently, but too strict to prevent user code from making problematic global assumptions.

[fitzgen]

@rossberg thanks!

That is not allowed, unless constant folding is guaranteed to implement the same semantics as execution on the host machine. This is a consequence of the new form of non-determinism introduced by this proposal which essentially codifies implementation-dependent behaviour, and guarantees that to be consistent across all executions of the same class of instruction.

Can you share where in the spec this consistency guarantee for the new form of non-determinism is codified?

[primoly]

The way I read it fma is deterministic (ignoring NaNs). It is only allowed to round at the end (fused). Note how it doesn’t have a relaxed prefix.

There is however an other instruction relaxedmadd_N which can be fused or unfused. I believe the host-dependent non-determinism appears here: [ \fadd_N(\fmul_N(z_1, z_2), z_3), \fma_N(z_1, z_2, z_3) ]. I think { … } means pick whatever you like (set non-determinism) and [ … ] means pick whatever the first time, but then always make that same choice (list non-determinism).

I don’t know if the “make the same choice” then applies to other instructions as well, but I would guess so. For instance if you went the fused route on relaxedmadd_N, I think you would then also have to pick the fused result on relaxednmadd_N for example.

[rossberg]

@fitzgen, it essentially is in this paragraph, which specifically says:

For each execution of the operator in the same environment, only values from the set at the same position in the list are returned, i.e., each environment globally chooses a fixed projection for each operator.

[Unfortunately, the spec isn't auto-rendered on this repo, so I can only link to the source. @dtig, could somebody fix that?]

This all is super hand-wavy, since it's never specified what an "environment" is or what "globally" means. But the intention clearly is that it at least extends over a given program, i.e., a complete set of interoperating modules. Consequently, any correct transformation of code in one of these modules must ensure that it preserves this property across the entire program.

(I have some ideas for rewriting this spec by making the global semantic parameters hiding in this explicit. However, the problem remains that there is no obvious way to delimit the boundaries of "global". For example, what if the same closed program is executed twice independently but in the "same engine instance", do we guarantee the same choices? I think not, nor can we even specify that.)

[fitzgen]

Gotcha. So it is intended, but not formally spec'd yet.

In that case, I can look into adding some spec test like

(func (export "test") (param v128 v128)
  local.get 0
  local.get 1
  relaxed_whatever
  v128.const ...
  v128.const ...
  relaxed_whatever
  v128.eq
)

;; Pass in the same values as dynamic arguments that are static constants
;; inside the function and assert the non-deterministic results are the
;; same.
(assert_return (invoke "test" (v128.const ...) (v128.const ...)) (i32.const 1))

[rossberg]

Sounds good!

[fitzgen]

Added a test in #156, would appreciate a review and merge!