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

Unsynchronized data races #189

Open
wingo opened this issue Jul 13, 2022 · 1 comment
Open

Unsynchronized data races #189

wingo opened this issue Jul 13, 2022 · 1 comment

Comments

@wingo
Copy link

wingo commented Jul 13, 2022

memory.fill is currently specified as writing its bytes sequentially from lowest address to highest: https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-fill. This behavior is unobservable to the thread executing the instruction, and I would presume most implementations don't write a byte at a time. But with multiple threads, I understand the goal is to allow races. What do we guarantee in that case?

  1. Will a thread reading memory being concurrently filled via memory.fill see a linearly advancing fill?
  2. Will a thread reading memory being concurrently filled via memory.fill see either the old data or the new data? Could it see something else?

I am particularly interested in the last question: is seeing something else allowed.

@conrad-watt
Copy link
Collaborator

conrad-watt commented Jul 13, 2022

The intention is that implementations should have the freedom to perform the writes in whatever order suits them (reverse, blocks, or something weirder). It's convenient for a formal semantics to specify it in this recursive byte-by-byte way, but as you point out, because of the initial bound check, this isn't observable intra-thread.

If a thread carries out accesses that race with a memory.fill in another thread, the (edit: not yet fully documented) relaxed memory model specifies that each access will individually non-deterministically see either the old data or the new data, in order to maintain the property that the order of writing is not observable (edit: also, weird access reordering stuff make it hard to say something stronger).

We did discuss a while ago what we should do if something like memory.protect was added which could make the order of writing more "persistently" observable, and we determined that we'd have to change the spec to explicitly say that memory.fill writes its bytes in non-deterministic order (or something equivalent).

We should add a note to this effect if it's not present already. I'm currently trying to arrange something that will give me more time/resource to get the threads spec over the line, so hopefully I'll be able to do this soon myself.

EDIT: seeing your other issue, I've replied there too

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

2 participants