Repository navigation
Unsynchronized data races #189
Description
Activity
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.fillin 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.protectwas 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 thatmemory.fillwrites 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
memory.fillis 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?memory.fillsee a linearly advancing fill?memory.fillsee 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.