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.

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

Seeming contradiction in summary regarding the nature of non-determinism in this proposal #153

Open
RalfJung opened this issue Nov 4, 2023 · 0 comments

Comments

@RalfJung
Copy link

RalfJung commented Nov 4, 2023

Reading the summary for this proposal, I find myself confused. On the one hand, it says

The same instruction at (1) and (2), when given the same inputs, can return two different results.

This sounds like the normal kind of non-determinism we consider on PL theory, like a choice: () -> bool function that returns some arbitrary boolean value each time it is executed.

But then later, it says

Some operators are host-dependent, because the set of possible results may depend on properties of the host environment (such as hardware). Technically, each such operator produces a fixed-size list of sets of allowed values. For each execution of the operator in the same environment, only values from the set at the same position in the list are returned, i.e., each environment globally chooses a fixed projection for each operator.

which sounds very different! Now the choice cannot be made independently each time the code is executed, instead the choice is made once upfront when "the environment" is fixed. It remains unclear what exactly is part of "the environment".

So concretely, if within the same wasm module I run such an instruction twice in a row with the same inputs, is it allowed to return different results? (I don't care whether that's likely or unlikely, I only care about whether this is permitted by a correct implementation.)
And what exactly is part of "the environment" -- in particular, at which point during the lifetime of a wasm module can I assume that "the environment" is fixed and can no longer change (so that I can rely on operations now behaving deterministically)?

@RalfJung RalfJung changed the title Seeming contradiction in summary Seeming contradiction in summary regarding the nature of non-determinism in this proposal Nov 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant