SPIR-V should have fine-grain execution semantics

[pizlonator]

JavaScript, WebAssembly, and WHLSL all have specifications that are at the level of granularity of a reference implementation of the language.

JavaScript's spec is written in a formalish style where each operation in the language is defined to have imperative steps like a computer program would have. Although it's not really code, it's structured like a program and it's detailed enough that it's rare for two English-speaking programmers to disagree on the meaning of the spec. Take section 7.1.5 in https://www.ecma-international.org/publications/files/ECMA-ST/Ecma-262.pdf as an example. This doesn't just merely describe what the outcome should be or place constraints on how it's computed - it tells you exactly what steps you should take to compute it. Of course, implementors can choose to take some other steps, so long as they can prove that the steps they took and the steps prescribed by the spec exhibit indistinguishable behavior. Having this level of detail is important because it prevents implementation divergence, like what happened in GLSL.

WebAssembly's spec is also at the level of detail of a computer program. In fact, the spec resulted from basically translating an OCaml program to English and formal rules. That OCaml program was "the spec" for a while, before all of the details were decided. So, even more so than the JavaScript spec, the WebAssembly spec is a computer program written in a mix of formal rules and English. Consider the level of specificity in WebAssembly's T.load instruction (where T is type, so could be i32 for example) on page 67 of this document: https://webassembly.github.io/spec/core/_download/WebAssembly.pdf

These specs are written to be as close to a computer program as possible while also retaining maximum human readability. The point of this is that when an implementor does their thing, then they can reason objectively about whether their implementation behaves indistinguishably from the specification. If the specification is not program-like, then I don't think it's possible to answer these questions objectively.

We believe that a majority of the problems with GLSL stemmed from underspecification. Anytime a spec falls short of what JavaScript and WebAssembly are doing, it becomes possible for someone to implement something incompatible but then claim that the spec allows it.

WHLSL is striving to have the level of granularity that JavaScript and WebAssembly have, and it's trying to follow WebAssembly's example concerning the style (like WebAssembly, we use formal semantics to aid reasoning about how operations work).

Here are two other examples of specifying an instruction in a way that makes it unambiguous how security properties are ensured:

• https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-6.html#jvms-6.5.iaload (note that this spec has more verbiage in a separate verification section - the part I linked is just the execution semantics).
• Section III.4.7 (about ldelem) in https://www.ecma-international.org/publications/files/ECMA-ST/ECMA-335.pdf

I think that SPIR-V should aim to have this level of specificity so that if we do end up using it as the input format, then we won't have to worry about incompatibilities being allowed by the spec.

[dneto0]

After the last community group meeting I started looking at what formal semantics was available for JavaScript. I'd want to use a formalism that's checkable. The JavaScript spec has prose that looks like pseudo-code, but I'd prefer a checkable artifact.

I found "KJS: A Complete Formal Semantics of JavaScript" https://daejunpark.github.io/p346-park.pdf .

Question for @pizlonator : In your opinion is that good work, and a good model to follow? On the face of it, the K framework looks promising because can yield checkable artifacts and emulators. It also appears to accommodate indeterminate behaviour (choice), as would be required for GPU execution.

That said, specificity and formality of a specification is not enough:

• Sometimes the spec can be very specific and wrong: modf is specified incorrectly WSL#272

• Also, you have to decide where to bottom-out: semantics of standard library functions? WSL#273