Skip to content
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.

Sign up for GitHub

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

Merged
merged 9 commits into from
Jun 11, 2015
Merged

Change 'incompletely specified behavior' phrasing to 'limited local nondeterminism' #141

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
95d112a
Change 'incompletely specified behavior' phrasing to 'limited local n…
lukewagner Jun 10, 2015
e5496a8
Remove spaces
lukewagner Jun 10, 2015
5a7008c
Well, not *fully* deterministic
lukewagner Jun 10, 2015
c6b5be0
Update for comments
lukewagner Jun 11, 2015
b1b824b
Add period.
lukewagner Jun 11, 2015
40a6bf5
Refine description of thread nondeterminism
lukewagner Jun 11, 2015
def4391
Merge branch 'master' of https://github.com/WebAssembly/design into r…
lukewagner Jun 11, 2015
2546267
Tweak to remove seq-cst mention (irrelevant to goal of doc) and menti…
lukewagner Jun 11, 2015
225ce8b
order -> sequence
lukewagner Jun 11, 2015
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 0 additions & 36 deletions IncompletelySpecifiedBehavior.md
View file
Open in desktop

This file was deleted.

53 changes: 53 additions & 0 deletions Nondeterminism.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
# Nondeterminism in WebAssembly

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".
Copy link
Member

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done


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).

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.

The following is a list of the places where the WebAssembly specification
currently admits nondeterminism:

- [When threads are added as a feature](EssentialPostMVPFeatures.md#threads),
even without shared memory, nondeterminism will be visible through the
ordering of API calls. Shared memory will allow further nondeterminism via
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know if this is too pedantic, but it's also visible between API calls and WebAssembly program termination.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True true, we must never forget termination.

load/store operations which,
[following the C++ definition](http://www.hboehm.info/c++mm/sc_proof.html),
only provide sequentially consistent views of memory in the absence of races.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By "races" here, I assume you mean "data races" as is used in that link.

I think this is still incomplete. The first bullet covers non-determinism in API ordering, and this bullet covers non-determinism in not getting sequentially consistency. However, a sequentially-consistent interleaving of actions can produce observable behavior differences other than API ordering.

I'd like to again propose for consideration the "race condition" terminology as being a more broad term meaning "anything where the non-deterministic ordering is observable", which is exactly what we want and doesn't get bogged down in memory model semantics.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

However, a sequentially-consistent interleaving of actions can produce observable behavior differences other than API ordering.

Like what (other than program termination)?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, I guess the distinction here is: w/ threads but no shared memory, you have nondeterminism at the API call/termination level. W/ shared memory, you get nondeterminism at the load ops. Is that what you were going after?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we cover those two points, I agree it's not really necessary to mention seq cst; it's just as nondeterministic as non-seq-cst. However, I do like talking about what is nondeterministic; vaguely refering to race conditions doesn't seem to do this, though I'd be happy to see proposed alternatives.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, further investigation reveals a clause I didn't spot at first in the link above, which is that it only applies to "programs which [...] do not use atomic operations". Our shared memory is going to have atomic operations, so then it's not immediately clear where we stand there.


- [Out of bounds heap accesses *may* want some flexibility](AstSemantics.md#out-of-bounds)

- [NaN bit patterns](AstSemantics.md#floating-point-operations)
Copy link
Member

Choose a reason for hiding this comment

The 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.

Copy link
Member Author

Choose a reason for hiding this comment

The 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.

Copy link
Member

Choose a reason for hiding this comment

The 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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#148.


- [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.

## 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.

On WebAssembly, the primary invariants are always maintained. Demons can't actually fly out your nose, as that would constitute an escape from the sandbox. And, callstacks can't become corrupted.

Other than that, programs which invoke undefined behavior at the source language level may be compiled into WebAssembly programs which do anything else, including corrupting the contents of the application heap, calling APIs with arbitrary parameters, hanging, trapping, or consuming arbitrary amounts of resources (within the limits).

[Tools are being developed and ported](Tooling.md) to help developers find and fix bugs in their code.
2 changes: 1 addition & 1 deletion Portability.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ efficiently on a variety of operating systems and instruction set architectures,
[on the Web](Web.md) and [off the Web](NonWeb.md).

Execution environments which, despite
[allowed implementation variants](IncompletelySpecifiedBehavior.md), don't offer
[limited, local, non-determinism](Nondeterminism.md), don't offer
the following characteristics may be able to execute WebAssembly modules
nonetheless. In some cases they may have to emulate behavior that the host
hardware or operating system don't offer so that WebAssembly modules execute
Expand Down