3 ms·
The pseudocode isn't UB because of the locks, but my argument is that it shouldn't be UB even if the locks were gone. In that case, there is a simultaneous read
by tomp 5y ago
The pseudocode isn't UB because of the locks, but my argument is that it shouldn't be UB even if the locks were gone. In that case, there is a simultaneous read/increment, but it's still obviously linearizable exactly the same way as with locks, so it still shouldn't be UB. (Or, if the memory fence caused by atomic increment instruction makes it non-UB, then just imagine overwriting a flag without any fences instead.) In Rust it's not even possible to write such code.
Another example is Figure 5 in this paper [1] (referenced from Bohem's paper above):
x = y = 0
// thread 1: // thread 2:
a = x; c = y;
b = x; x = c;
if (a == b)
y = 1;
My point is that the assumption that a == b is invalid if x is a global variable. That's not a valid assumption for the compiler to make, ever, unless it can prove that x isn't accessed from different threads (as a human would have to, to manually perform the optimisation).
I haven't been tracking OCaml's progress too closely (multicore is just taking too long), but hopefully it's going in this direction... if you've any relevant references / descriptions of their memory model, let me know!
https://www.ccs.neu.edu/home/wahl/Teaching/Software-Model-Checking/2016-Spring/Papers/memory-models.pdf https://www.ccs.neu.edu/home/wahl/Teaching/Software-Model-Ch...
- tialaramex 5y ago> In Rust it's not even possible to write such code. What does "such code" mean though? Rust won't let you say that your mutable variables are just shared between threads, because that's unsafe. But if you say OK, I want atomic data types (and so they lack tearing and other things you were bothered about) then you can clone an Arc of them, and write code to manipulate the atomics whose consequences are just as under specified. It's just that now you have to spell out that this is what you wanted, writing e.g. std::sync::atomic::Ordering::Relaxed If you later complain to me that this code surprised you because the memory ordering wasn't what you expected, I will point at that symbol. If you wanted some specific ordering then "Relaxed" was wrong. > My point is that the assumption that a == b is invalid if x is a global variable. No it isn't? This is an important optimisation, which you would prefer to sacrifice rather than just writing what you mean in the first place. > if you've any relevant references / descriptions of their memory model, let me know! https://kcsrk.info/papers/pldi18-memory.pdf https://kcsrk.info/papers/pldi18-memory.pdf
- steveklabnik 5y agoYou don't need an Arc with atomics https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=fc20109626a8eb28d34a412924c1974d https://play.rust-lang.org/?version=stable&mode=debug&editio...
- tialaramex 5y agoSure, however now your atomic has 'static lifetime so it lives forever and that's sort of cheating. The reference counter means nobody in particular needs to be in charge of cleaning up, whoever has it last will drop it. Call it personal preference. Also, is the broken kinda of look of your blog an aesthetic choice or a bug? Is "![Today%20is%20my%20first" really what that ought to display under the title ? I feel like it probably isn't.
- steveklabnik 5y agoI don't see how 'static is cheating, that's the semantic you want: to be able to live as long as the various threads. If you used scoped threads you wouldn't need 'static, but those are less general, so I didn't get into it. No, it's just buggy. :( Thanks for mentioning though, that bug is not one I had seen just yet.