-
Notifications
You must be signed in to change notification settings - Fork 696
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Change 'incompletely specified behavior' phrasing to 'limited local nondeterminism' #141
Changes from 4 commits
95d112a
e5496a8
5a7008c
c6b5be0
b1b824b
40a6bf5
def4391
2546267
225ce8b
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,30 +1,42 @@ | ||
# Incompletely Specified Behavior | ||
# Nondeterminism in WebAssembly | ||
|
||
WebAssembly is a [portable](Portability.md) sandboxed platform. Applications | ||
can't access data outside the sandbox without going through appropriate APIs, or | ||
otherwise escape the sandbox, even if the behavior inside the sandbox should | ||
ever be unspecified in any way. | ||
WebAssembly is a [portable](Portability.md) sandboxed platform with limited, | ||
local, nondeterminism. | ||
* *Limited*: non-deterministic execution can only occur in a small number of | ||
well-defined cases (described below) and, in those cases, the implementation | ||
may select from a limited set of possible behaviors. | ||
* *Local*: when non-deterministic execution occurs, the effect is local, | ||
there is no "spooky action at a distance". | ||
|
||
WebAssembly always maintains valid callstacks. Return addresses are stored on the trusted stack and can't be clobbered by the application. And, WebAssembly ensures that calls and branches always have valid destinations. | ||
The limited, local, non-deterministic model implies: | ||
* Applications can't access data outside the sandbox without going through | ||
appropriate APIs, or otherwise escape the sandbox. | ||
* WebAssembly always maintains valid, trusted callstacks; stray pointer writes | ||
cannot corrupt return addresses or spilled variables on the stack. | ||
* Calls and branches always have valid destinations ensuring | ||
[Control Flow Integrity](http://research.microsoft.com/apps/pubs/default.aspx?id=64250). | ||
* WebAssembly has no [nasal demons](https://en.wikipedia.org/w/index.php?title=Nasal_demons). | ||
|
||
Beyond that, WebAssembly minimizes observable differences between implementations, to reduce the risk of applications becoming dependent on any particular implementation's behavior. However, occasionally compromises are made due to performance concerns, listed below. | ||
Ideally, WebAssembly would be fully deterministic (except where nondeterminism | ||
was essential to the API, like random number generators, date/time functions or | ||
input events). Nondeterminism is only specified as a compromise when there is no | ||
other practical way to achieve [portable](Portability.md) native performance. | ||
|
||
In particular, WebAssembly has no [nasal demons](https://en.wikipedia.org/w/index.php?title=Nasal_demons), since they are an extreme on the spectrum of observable differences, and since they make it difficult to reason about what state an application might be in. WebAssembly prefers to [trap](AstSemantics.md) when feasible, and otherwise it permits a specific set of possible conforming behaviors. | ||
The following is a list of the places where the WebAssembly specification | ||
currently admits nondeterminism: | ||
|
||
The following is a list of the places where the WebAssembly specification currently admits or is expected to admit multiple possible behaviors. | ||
- [No sequential consistency guarantee for programs which contain races](EssentialPostMVPFeatures.md#threads) | ||
|
||
- [Out of bounds heap accesses](AstSemantics.md#accessing-the-heap) | ||
|
||
- [Environment-dependent resource limits may be exhausted](AstSemantics.md) | ||
- [Out of bounds heap accesses may want some flexibility](AstSemantics.md#out-of-bounds) | ||
|
||
- [NaN bit patterns](AstSemantics.md#floating-point-operations) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add denormal handling: unspecified if we go full IEEE 754 (for scalar and/or vector), or if we DAZ/FTZ. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this should be a separate conversation/PR (outside the scope of this PR). Also, fwiw, I'd been assuming we'd just (1) initially define DAZ/FTZ, (2) later, only if there is a pressing need, offer more control. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Would you mind filing a separate issue so that we can have a discussion about this? Thanks. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. #148. |
||
|
||
- [Races between threads](EssentialPostMVPFeatures.md#threads) | ||
|
||
- [Fixed-width SIMD may want some flexibility](EssentialPostMVPFeatures.md#fixed-width-simd) | ||
- In SIMD.js, floating point values may or may not have subnormals flushed to zero. | ||
- In SIMD.js, operations ending in "Approximation" return approximations that may vary between platforms. | ||
|
||
- Environment-dependent resource limits may be exhausted | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Missing period. |
||
|
||
## Note for users of C, C++, and similar languages | ||
|
||
Some operations which have fully defined behavior in WebAssembly itself may nonetheless have undefined behavior at the source code level. For example, while unaligned memory access is fully defined in WebAssembly, C and C++ compilers make no guarantee that a (non-packed) unaligned memory access at the source level is harmlessly translated into an unaligned memory access in WebAssembly. And in practice, popular C and C++ compilers do optimize on the assumption that alignment rules are followed, meaning that they don't always preserve program behavior otherwise. | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Capitalize "limited" and "local" above, since they're at the start of sentences.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done