|
|
|
|
|
by Groxx
92 days ago
|
|
A data race implies getting results that are not allowed by the single-threaded semantics of the API - corruption, basically. It sounds like that's not possible because the API is strictly single threaded, and any data you receive is copied (I think?) so it can't be mutated afterward. Which also means it's not shared memory - you are not sharing ownership of it, you're exclusively using copies. You're describing a logical race, something unintended but allowed due to interleaving behavior, not a data one. Logical races are a heck of a lot harder to prevent without going fully proof-oriented. |
|
To phrase my point here a bit differently, the distinction between a data race and a logical race is purely the scope of the expected consistency. In the standard multi-threaded case as well, if you read a single word from the memory it will definitely be consistent — you'll get the result of either one write or another, never half of the word from one write and half from the other. But values in real programs are usually bigger than a single word, and once you read two words from the memory it becomes possible (ignoring for the sake of argument the facilities modern memory provides for reading larger memory ranges atomically; feel free to replace ‘word’ with your atomic unit of choice) to get one word from one write and one word from another. As words these are consistent — they're both valid words and they both come from an intentional write — but put together they may not form a coherent value of the higher-level type you meant to read. This is how you get ‘corrupted’ data: the notion of corruption comes not from the memory semantics but from the semantics of the type that the memory is being used to represent. This applies exactly the same to Mem: each word is, as you say, consistent, but if you try to read a value by doing two reads, the resulting value may be ‘corrupt’ (formed by the interleaving of two writes) depending on what other threads are doing with Mem at the time.