undefined | Better HN

0 pointsoconnor6633y ago0 comments

There's a tricky distinction here. I'm pretty sure Java does provide data race freedom, in the specific sense that a data race is "Undefined Behavior caused by a write overlapping with another read or write". The Java standard says that the JVM isn't allowed to trigger this sort of undefined behavior. (Maybe some people say it's technically still a data race? I'm not sure of the right formal definition, but anyway the important thing is that in Java the UB doesn't happen here.) However, what happens when you do that can still be extremely tricky, and I think the Java compiler is still allowed to reorder reads and writes in ways that'll be extremely confusing if you have code that looks like a data race. It won't give an attacker arbitrary code execution, but it's very likely still a bug.

0 comments

tialaramex3y ago

Data Race Freedom is, unsurprisingly, Freedom from Data Races. A Data Race is any time when there's concurrent modification of a memory value, on modern hardware with multiple simultaneous execution contexts those modifications could in some sense happen at the same moment.

[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.

jonathanstrange3y ago

AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general, that is theoretically not possible. What you get is a guarantee that your program is not in an undefined state. There are still plenty of ways to shoot yourself in the foot with incorrect synchronization.

tialaramex3y ago

> AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general

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.

eru3y ago

> AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general, that is theoretically not possible.

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.

oconnor663OP3y ago

> A Data Race is any time when there's concurrent modification of a memory value

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?

tialaramex3y ago

Well spotted. This is arguably a hole, albeit a deliberate one. In practice the main reason people do this is collecting some sort of metric, whose exact value is unimportant and which anyway isn't contemplated by the machine.

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.

oconnor663OP3y ago

As an interesting example of doing something meaningful with relaxed arithmetic, Arc uses a relaxed fetch_add to increment the refcount: https://doc.rust-lang.org/src/alloc/sync.rs.html#1331-1343. Decrementing, however, uses acquire-release. Apparently shared_ptr in C++ is similar.

1 more reply

j / k navigate · click thread line to collapse

0 comments

tialaramex3y ago

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.

Safe Rust promises DRF and thus SC. So instead of being very careful you can just write safe Rust.

jonathanstrange3y ago

tialaramex3y ago

> AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general

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.

eru3y ago

> AFAIK, you still have to be very careful since data races based on data dependencies can never be excluded in general, that is theoretically not possible.

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.

oconnor663OP3y ago

> A Data Race is any time when there's concurrent modification of a memory value

tialaramex3y ago

oconnor663OP3y ago

1 more reply

j / k navigate · click thread line to collapse