Now that I think about it, this must be the case, right? You have to get `synchronized` right in Java or else you won't get what you expect.
Now that I think about it, this must be the case, right? You have to get `synchronized` right in Java or else you won't get what you expect.
(I didn't find this integirty of runtime specified in the JMM spec, hopefully it's in the other specs).
In the JMM terminology, the "you're in the clear" term is "well-formed execution". If you break the rules, you're not in "well-formed execution" land any more, and things may fly out of your orifices, but a specific type of C/C++ style dragon won't maybe fly out of your nose.
So there's a weak kind of memory safety, your app data in may still be garbled, possibly in an attacker-controlled way, but the attacker probably won't get remote code execution.
[NB: Data Races are a subset of Race Conditions. Race Conditions are sometimes just a fact about the world and you need to write programs that cope with this, but they are not necessarily Data Races, if you copy all the files from folder A to folder B, and then delete folder A, somebody meanwhile adding a file to folder A which you then delete despite not having copied it would be a Race Condition, but it is not a Data Race. ]
The reason you want Data Race Freedom is that it's easy for a programming language to offer Sequential Consistency if you have Data Race Freedom, this guarantee is called SC/DRF.
Why do we want Sequential Consistency? Sequential Consistency is when programs behave as if stuff happened in some sequence. The disk reader gets a block from disk and then the encryptor applies AES/GCM to the block and then the network writer sends the encrypted block to the client. It turns out humans value this very much when trying to reason about any non-trivial program. Get rid of Sequential Consistency and the programmers are just confused and can't solve bugs.
So, we want SC/DRF and in most languages you get that by being very careful to obey the rules to avoid Data Races. If you screw up, you don't have Sequential Consistency. In most languages you lose more than that (in C or C++ you immediately have Undefined Behaviour, game over, all bets are off), but even just losing Sequential Consistency is very bad news.
Safe Rust promises DRF and thus SC. So instead of being very careful you can just write safe Rust.
Hmm. Maybe I don't understand what you're getting at here. It seems like you're suggesting something like a[b] = x could race in safe Rust because we don't know b in advance and maybe it ends up being the same in two threads ?
But Rust's borrow checker won't allow both threads to have the same mutable array a so this is ruled out. You're going to have to either give them immutable references to a, which then can't be modified and so there's no data race, or else they need different arrays.
This is boringly easy to get right in theory, Rust just has to do a lot of work to make it usable while still delivering excellent runtime performance.
Well, you could always require the programmer to supply a proof that the program is gonna be fine, before you compile anything.
(That means your programming language won't be Turing complete, but you can still code up anything you want in practice. Including Turing machines.)
The likes of Agda and Coq work in this way.
I do want to nail down the terminology, so help me with this scenario: Two simultaneous relaxed atomic writes to the same variable from different threads. To my understanding, this is not a data race (since this is allowed, while data races are never allowed), but it is concurrent. Do I have that right?
If your program tries to actually act on this data then yeah, you have successfully made your own life unnecessarily exciting and debugging your program may be difficult. I think it's fair to say you've only yourself to blame though since you had to explicitly choose this.