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 2 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
43 changes: 27 additions & 16 deletions IncompletelySpecifiedBehavior.md → Nondeterminism.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,26 +1,37 @@
# Incompletely Specified Behavior
# 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. Nondeterminism is only
Copy link
Member

Choose a reason for hiding this comment

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

Another probably unimportant note, it might be better to avoid saying "fully deterministic" because in a more general sense, there is or will be nondeterminism in wasm - stuff like calling a random number generator. Very nitpicky of course, as your intention is clear, so feel free to ignore.

Copy link
Member Author

Choose a reason for hiding this comment

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

Haha, good point, I forgot about random. I can reword.

specified as a compromise when there is no other practical way to achieve
[portable](Portability.md), near-native performance.
Copy link
Member

Choose a reason for hiding this comment

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

Drop "near-"? We want native performance!

Copy link
Member

Choose a reason for hiding this comment

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

I think "near-" is an acknowledgement that we are sandboxed and that we are providing a portability abstraction that discards certain unappetizing-but-nonetheless-expedient implementation details, and until we get hardware support there's always going to be some overhead. But ultimately it's a question of taste here.

Copy link
Member Author

Choose a reason for hiding this comment

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

Yeah, this is just the conservative "don't overpromise" engineer in me, but "native" is probably fine here, so I'll take out "near-".


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

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

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.

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 or is expected to admit multiple possible behaviors.
- [Races between threads](EssentialPostMVPFeatures.md#threads)
Copy link
Member

Choose a reason for hiding this comment

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

I'd instead say "no sequential consistency guarantee for programs which contain races"? This is a direct reference to Sequential Consistency for Race-Free Programs, which I would also link to.

I think thread scheduling is another source of non-determinism.

Copy link
Member Author

Choose a reason for hiding this comment

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

Sounds good. For symmetry, I'll leave the link to EssentialPostMVPFeatures.md#threads and we can add the link you gave to that section as a refinement in a separate PR.

Copy link
Member

Choose a reason for hiding this comment

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

I originally intended "race" here in the sense of "race condition" rather than "data race", following the distinction made here, because harmless data races aren't necessarily bugs, and race conditions can cause bugs without being data races.

When you say thread scheduling, do you mean resource starvation (#103), or just that observable things don't always happen in the same order? I think using the more general sense of "race condition" covers the latter.

Does this terminology work for you?

Copy link
Member

Choose a reason for hiding this comment

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

Let's discuss both race condition and data race, and drop thread scheduling.
@lukewagner : you want to do this in a separate PR? sgtm


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

- [Environment-dependent resource limits may be exhausted](AstSemantics.md)
Copy link
Member

Choose a reason for hiding this comment

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

I'm not sure why this links to AstSemantics.md.

Copy link
Member

Choose a reason for hiding this comment

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

The intro to AstSemantics.md is currently where the wording about resource exhaustion is. Perhaps that's not the best place for it, but that's where it is right now.

Copy link
Member Author

Choose a reason for hiding this comment

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

Pre-existing, but I'm guessing it's just for symmetry since everything else has a link and there isn't yet a section talking about resource limits. For now I'll take out the link and move it to the end of the list. We can add a section and link to it in another PR.


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


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