WebAssembly / design

WebAssembly Design Documents
http://webassembly.org
Apache License 2.0
11.37k stars 691 forks source link

Partially out-of-bound writes #1490

Open sparker-arm opened 8 months ago

sparker-arm commented 8 months ago

The semantics of partially OOB writes was clarified in #1025. This has proved problematic for runtimes running on Arm, where there is no such guarantee in the architecture. I think all now browsers implement the spec properly, but I'm not sure if any of the wasm-specific non-browser runtimes do.

I could see that having deterministic memory contents is a nice property, but I'm not sure of what the real advantages are, could someone enlighten me?

And do you think there's any room to relax the spec in this regard, possibly even through an extension like relaxed-simd?

sparker-arm commented 8 months ago

given that many different kind of store instructions could trap, the instruction decoder for that could be quite unwieldy.

Indeed.

Another option is to use metadata to encode the original (bytecode) PC and then replay the bytecode in an interpreter or JIT a stub.

I'm not sure how this would work, without still having to decode the instruction to figure out what data needs to be stored where?

Storing zeros removes the need to decide out what to store, but we'd still need to decode to find out the start address of the unaligned access. (Though this is trivial for half-word stores).

To avoid any decoding, would it be feasible to generate a side-table to describe each machine-level store?

sparker-arm commented 8 months ago

It also looks like partial writes are a potential problem for POWER too.

From Power ISA Version 3.1B, Book II, Chapter 2

Any other Load or Store instruction may be partially executed and then aborted after having accessed a portion of the storage operand..

When an instruction is aborted after being partially executed, the contents of the instruction pointer indicate that the instruction has not been executed, however, the contents of some registers may have been altered and some bytes within the storage operand may have been accessed.

titzer commented 8 months ago

@sparker-arm

I'm not sure how this would work, without still having to decode the instruction to figure out what data needs to be stored where?

Right, I meant that there'd be enough metadata to go back to executing the instruction in the interpreter, which means both the bytecode PC and the bytecode's inputs (value stack operands), which constitute the address and value stored. If that were compressed, it basically amounts to a sidetable as you describe.

Thanks for the additional context for POWER. The upshot of that seems to be basically the same as ARM.

cfallin commented 3 months ago

I've gone ahead and implemented the load-before-store idea in Wasmtime and measured a 2% perf impact on Apple aarch64 hardware (which doesn't see torn stores, but is what I have at hand). It would still be useful to continue discussing the spec change options above, but if it remains as-is, it seems we could implement "precise post-trap memory state" for those who need it with reasonable-ish overhead.

ebeasant-arm commented 1 month ago

Hi all: I've been following this one for a while now, and it seems to me to be a real challenge!

I'm trying to understand the rationale for mandating the behaviour in the WebAssembly specification came about - regardless on whether there are implementation that depend on the behaviour. What follows is some observations, questions and some reasoning - seeking understanding, clarity and little more depth, if possible!

Partially OOB store behaviour - introduction of the required behaviour to the spec:

Following up how the mandated behaviour was introduced to the specification, I'm not sure of the history, but it feels like there is a case of 'Inception' going on:

https://github.com/WebAssembly/spec/issues/438 , https://github.com/WebAssembly/spec/pull/439 , https://github.com/WebAssembly/design/pull/1025

These seem to form a sort of loop: The bug in the tests raised the change which then caused the 'uncontroversial clarification', which then ended up in the specification.

However, I would hazard that that the uncontroversial clarification is anything but uncontroversial, given the amount of debate this has generated, and that at least three target architectures cannot efficiently implement it?

Architecture vs. implementation & probabilistic behaviours

In terms of the (specifically) architectural specs in question, the behaviour in point is architecturally permitted - Whether the behaviour occurs or not isn't just about the particular implementation of the Architecture: The behaviour that is problematic is also likely to be probabilistic dependent on current system state. I'm not sure it's reliable to assert that anything (at least Arm based) either does or does not behave in a given way - more that it just hasn't been observed to behave in that way, yet.

I also believe that Architecturally, x86 has some complicated cases in which it may be permitted to have similar behaviour (unaligned writes are not guaranteed atomicity, for example) - this is something that we probably need chapter and verse on from Book 1 or 3 of the x86 spec...

Architectural litmus test tools like Hurd7 help to check for permitted behaviours across all the mentioned architectures - Notably, however, this particular case is also a challenge to represent in Hurd7 syntax at this moment in time, though as I understand it, it is being worked on. This could be potentially used to check the permitted an actual (it also generates sample code for execution on targets) behaviours across the architectures - but note the probabilistic effect is still also in play for on target tests.

Ways forward?

Given the apparent history of the introduction of this behaviour to the specification, and the impact on performance that other schemes for approaching it have been demonstrated to have:

Is it not reasonable on the balance of the design principals of WebAssembly to revert this tightening of requirements in the face of mounting evidence contrary to the assertion that introduced it? (convoluted sentence there, but the problem is convoluted!)

If the answer is that 'it can't be reverted because all use cases rely on the behaviour', then perhaps It does belong. If it is 'is can't be reverted because some use cases rely on it', maybe profiles are the answer? If it is 'it can't be reverted because its part of the published specification' then that's probably a question for the governance process?

Challenges, and some questions:

There are evidently issues when dealing with uses of WebAssembly (Some Cryptocurrency/Smart Contracts) that require deterministic behaviours to remain externally visible after a trap has occurred.

As I understand it The WebAssembly core specification defines the behaviour from the design point of view of internal consistency and determinism. At the point of trap, this viewpoint is no longer present, and the rules that apply to it cease to apply - hence it is valid to suggest a 'fix up' of the state for a failed trap on partially out of bounds, but this solution raises the question for me:

The requirement for deterministic state in the case of partially OOB writes is from that same external frame of reference, not internal. So does it belong in the core specification? Is it in fact a form of interface contract instead?

Hoping that some of this leads to clarity and a good way forwards, many thanks to all on here for the discussion and hard work!

rossberg commented 1 month ago

@ebeasant-arm:

As I understand it The WebAssembly core specification defines the behaviour from the design point of view of internal consistency and determinism. At the point of trap, this viewpoint is no longer present, and the rules that apply to it cease to apply - hence it is valid to suggest a 'fix up' of the state for a failed trap on partially out of bounds

I may be misreading what you mean here, but to clarify: the core spec specifies the observable behaviour of external invocations of Wasm functions in a given "store". And it specifies and guarantees precisely the state that a Wasm store is in after a trap — a trap only aborts the current computation, it does not invalidate the store it ran in.

That means that future external invocations of Wasm functions in the same context that previously trapped still have well-defined behaviour. This is absolutely crucial. Currently, this also is deterministic wrt to partially OOB traps. That could be relaxed, but at least in the deterministic profile it definitely needs to remain so.

sparker-arm commented 1 week ago

That could be relaxed, but at least in the deterministic profile it definitely needs to remain so.

Do you have a view on how profiles would be implemented? Could this be a runtime parameter that is passed during module instantiation?

rossberg commented 1 week ago

@sparker-arm, profiles are not chosen or configured dynamically or on a per-application basis. Profiles are a means to support the diversity of (disjoint) ecosystems that want to include Wasm but cannot support certain features. As such, a profile is selected globally by an ecosystem that supports Wasm. For example, a Wasm infrastructure for embedded devices might not be able to support GC or SIMD. Ecosystems like blockchains running Wasm code need determinism. All applications build for such an ecosystem are then bound by this system-wide choice of profile.

sparker-arm commented 1 week ago

Right, sorry, I only now realise that you have a proposal for them! I will take a look.

sparker-arm commented 1 week ago

@rossberg So, what's the status of the proposal? I see you have a PR open to add the deterministic profile.

Is the suggestion here to add a deterministic marker to the currently defined semantics of OOB stores?

rossberg commented 1 week ago

The deterministic profile already was integrated into the relaxed SIMD proposal.

As for the OOB issue at hand, at least in the deterministic profile, the semantics has to remain as strict as it is right now. There has not been a resolution whether to relax it in general.

sparker-arm commented 1 week ago

Okay, thanks for the clarification.