4 ms·

Freedom from data races is far too weak a condition to be useful. Consider the following example: you have a single global mutex, and every read/write to memor

Freedom from data races is far too weak a condition to be useful. Consider the following example: you have a single global mutex, and every read/write to memory is bracketed by a lock/unlock of that mutex. The resulting code, while horribly inefficient, is technically free of data races, but that does not really give you anything interesting in terms of thread safety. Any useful definition of thread safety requires that you can reason about program behavior in the presence of concurrency. One such approach is the idea of interference-freedom introduced by Owicki and Gries [1]. Somewhat simplified, assuming that you have a thread A with precondition P and postcondition Q, i.e. the Hoare triple { P } A { Q }, a thread B does not interfere with thread A if the parallel execution of A and B, given the same precondition P we can still prove Q ({ P } A || B { Q }), for any interleaving of A and B. Obviously, proving such a property is undecidable in the general case. In practice, we therefore limit ourselves to simpler models that are easier to reason about by constraining how threads can interact with one another (e.g. transactions, actor model), but even then, you can still end up with situations that are undecidable in the general case. [1] https://dl.acm.org/citation.cfm?id=2697004 https://dl.acm.org/citation.cfm?id=2697004

wtracy 8y ago
I suspect the answer is, Rust ignores the general case, and simply doesn't let you do anything that's not provably correct.
- fooker 8y ago
  You can't use that argument and have turing completeness at the same time.
  - pornel 8y ago
    Yes, you can. You can emulate a Turing machine (except with a finite memory, of course) in safe Rust, but given that the Turing machine is entirely serial by design, I don't see how is that even relevant. In practice, Rust has `unsafe {}` escape hatch that allows building of abstractions (like mutexes) for the safe majority of Rust using contained bits of as-safe-as-C code where necessary.
Groxx 8y ago
>Any useful definition of thread safety requires that you can reason about program behavior in the presence of concurrency. Theoretically yeah, but there's a lot of practical gain to be had even with that example. Other languages won't tell you if you forgot to use the mutex somewhere.
- fooker 8y ago
  > Other languages won't tell you if you forgot to use the mutex somewhere. Languages like C++ and D treat this as a library design challenge, not a core language feature. Look at std::lock_guard, for example.
  - pornel 8y ago
    The Rust language doesn't know anything about locking, or even threads. The thread safety is built using Send/Sync traits, which libraries for threading and synchronization primitives, atomics, etc. implement accordingly.
- rbehrends 8y ago
  Okay. First, I was talking about useful definitions of thread safety. That was language-agnostic, not related to Rust. And if absence of data races were all that Rust guaranteed, then Rust indeed wouldn't be much of a help. What Rust actually does is require you to be (fairly) explicit about threads interacting with each other, which is a much stronger type of guarantee [1]. Rust comes with a default setting derived from the general shared-xor-mutable principle that threads don't mess with each other's data without permission, which makes it easier to reason about thread interaction. Second, the OP was comparing Rust to actor languages. Actor languages also don't have data races and don't require mutexes (because the memory spaces of actors are disjoint and actors themselves are sequential). In fact, actor languages provide even stronger guarantees, as actors can only interact with each other at well-defined points. "Fearless concurrency" hails back to the 1970s. It is not a new invention, nor is it unique to Rust. It is great that Rust supports it, but I really wish people would stop talking about it being novel and unique. [1] Which is not to say that Rust's choices don't come with tradeoffs, but then, in the area of concurrency, you cannot realistically avoid tradeoffs. In Rust's case, as with actors, the primary tradeoff is performance for safety.
scottlamb 8y ago
The way you say "useful" brings to mind Inigo Montoya in Princess Bride: "you keep using that word. I do not think it means what you think it means." Are there any practical / commonly used programming languages in which you can prove thread safety with that approach for significant programs? You mention it can be undecidable even with constraints like the actor model (Erlang). Maybe you just mean edge cases not encountered in real systems, but I'm guessing it's not practical. Why do you say it's useful? I see accidental data races a lot more than any other kind of race condition; I'd guesstimate that avoiding them gets you 90+% of the way to thread safety. Yes, you can release and reacquire the mutex in inappropriate spots (i.e., ones during which invariants are broken), but in a typical program there are a lot fewer mutexes acquisitions/releases than data accesses in general, so it's a lot more practical to audit for this. I feel a lot better with a program that has no data races than one which has no guarantees at all (most languages). Likewise, deadlocks are also a concern, but I'd say there are relatively few spots in your code where you have to be concerned about them. (For starters, they only occur with multiple contended resources (usually mutexes), whereas data race problems can and do happen with zero or one mutexes all the time) And the behavior when they happen is more consistent and far less subtle. The latter is similar reasoning to how people say that a panic is less worrisome than undefined behavior.
- rbehrends 8y ago
  > The way you say "useful" brings to mind Inigo Montoya in Princess Bride: "you keep using that word. I do not think it means what you think it means." Concurrency and parallelism has been what I've been working on for several decades. I have, inter alia, implemented concurrency mechanisms with strong safety guarantees for more than one language (among them two relying on shared memory [1, 2]), so yes, I think I have a pretty good idea what I'm talking about. > I see accidental data races a lot more than any other kind of race condition; And I didn't say otherwise. Freedom from data races (with the caveat that there are also benign data races that you sometimes want to exploit and that you want language mechanisms for) is more or less a necessary byproduct of most schemes to reason about concurrency; but on its own, its woefully inadequate for the reasons that I talked about. > I'd guesstimate that avoiding them gets you 90+% of the way to thread safety. If this were the case, then you'd practically never have any problem with thread safety in actor languages; that is not the case. A simple and extremely common pattern where freedom from data races falls short is the following: if (obj->condition()) obj->action(); If `obj` were just a monitor (i.e. an object that guarantees atomicity for individual operations), the code still wouldn't be thread-safe. What you generally want is thread safety at the transactional level, not at the level of individual operations. Any genuinely thread-safe language requires mechanisms that operate at the transactional level (though, obviously, not necessarily literal transactions in the DB sense), i.e. sequences of operations that you want to be atomic or non-atomic only in a controllable fashion. (Though, at the same time, it is also necessary that any such mechanism provides escape hatches for when it would impede concurrency [3].) > Are there any practical / commonly used programming languages in which you can prove thread safety with that approach for significant programs? First, I am not saying that being able to formally prove properties is a necessary element of concurrency (though there are systems that do exactly that, but that's beyond the scope of what I mentioned). But even when you're reasoning about program behavior informally, that relies on the same principles. Your code assumes some precondition and wants to arrive at a postcondition and you have to be sure that other threads don't muck up what your code is trying to accomplish. The larger point is that with just the absence of data races, we still have a combinatorial explosion of ways that threads could interact with one another: most useful concurrency schemes (including Rust's) function by cutting down on that combinatorial explosion and limiting ways in which threads can interact with one another (and thus, possibly, in undesirable ways). [1] https://link.springer.com/chapter/10.1007/11424529_17 https://link.springer.com/chapter/10.1007/11424529_17 [2] https://onlinelibrary.wiley.com/doi/full/10.1002/cpe.3746 https://onlinelibrary.wiley.com/doi/full/10.1002/cpe.3746 [3] E.g. https://dl.acm.org/citation.cfm?doid=1297027.1297042; https://dl.acm.org/citation.cfm?doid=1297027.1297042; while the paper is about software transactional memory, the mechanism extends to critical regions in general.

wtracy 8y ago

I suspect the answer is, Rust ignores the general case, and simply doesn't let you do anything that's not provably correct.

fooker 8y ago
You can't use that argument and have turing completeness at the same time.
- pornel 8y ago
  Yes, you can. You can emulate a Turing machine (except with a finite memory, of course) in safe Rust, but given that the Turing machine is entirely serial by design, I don't see how is that even relevant. In practice, Rust has `unsafe {}` escape hatch that allows building of abstractions (like mutexes) for the safe majority of Rust using contained bits of as-safe-as-C code where necessary.

Groxx 8y ago

>Any useful definition of thread safety requires that you can reason about program behavior in the presence of concurrency. Theoretically yeah, but there's a lot of practical gain to be had even with that example. Other languages won't tell you if you forgot to use the mutex somewhere.

fooker 8y ago
> Other languages won't tell you if you forgot to use the mutex somewhere. Languages like C++ and D treat this as a library design challenge, not a core language feature. Look at std::lock_guard, for example.
- pornel 8y ago
  The Rust language doesn't know anything about locking, or even threads. The thread safety is built using Send/Sync traits, which libraries for threading and synchronization primitives, atomics, etc. implement accordingly.
rbehrends 8y ago
Okay. First, I was talking about useful definitions of thread safety. That was language-agnostic, not related to Rust. And if absence of data races were all that Rust guaranteed, then Rust indeed wouldn't be much of a help. What Rust actually does is require you to be (fairly) explicit about threads interacting with each other, which is a much stronger type of guarantee [1]. Rust comes with a default setting derived from the general shared-xor-mutable principle that threads don't mess with each other's data without permission, which makes it easier to reason about thread interaction. Second, the OP was comparing Rust to actor languages. Actor languages also don't have data races and don't require mutexes (because the memory spaces of actors are disjoint and actors themselves are sequential). In fact, actor languages provide even stronger guarantees, as actors can only interact with each other at well-defined points. "Fearless concurrency" hails back to the 1970s. It is not a new invention, nor is it unique to Rust. It is great that Rust supports it, but I really wish people would stop talking about it being novel and unique. [1] Which is not to say that Rust's choices don't come with tradeoffs, but then, in the area of concurrency, you cannot realistically avoid tradeoffs. In Rust's case, as with actors, the primary tradeoff is performance for safety.

scottlamb 8y ago

The way you say "useful" brings to mind Inigo Montoya in Princess Bride: "you keep using that word. I do not think it means what you think it means." Are there any practical / commonly used programming languages in which you can prove thread safety with that approach for significant programs? You mention it can be undecidable even with constraints like the actor model (Erlang). Maybe you just mean edge cases not encountered in real systems, but I'm guessing it's not practical. Why do you say it's useful? I see accidental data races a lot more than any other kind of race condition; I'd guesstimate that avoiding them gets you 90+% of the way to thread safety. Yes, you can release and reacquire the mutex in inappropriate spots (i.e., ones during which invariants are broken), but in a typical program there are a lot fewer mutexes acquisitions/releases than data accesses in general, so it's a lot more practical to audit for this. I feel a lot better with a program that has no data races than one which has no guarantees at all (most languages). Likewise, deadlocks are also a concern, but I'd say there are relatively few spots in your code where you have to be concerned about them. (For starters, they only occur with multiple contended resources (usually mutexes), whereas data race problems can and do happen with zero or one mutexes all the time) And the behavior when they happen is more consistent and far less subtle. The latter is similar reasoning to how people say that a panic is less worrisome than undefined behavior.

rbehrends 8y ago
> The way you say "useful" brings to mind Inigo Montoya in Princess Bride: "you keep using that word. I do not think it means what you think it means." Concurrency and parallelism has been what I've been working on for several decades. I have, inter alia, implemented concurrency mechanisms with strong safety guarantees for more than one language (among them two relying on shared memory [1, 2]), so yes, I think I have a pretty good idea what I'm talking about. > I see accidental data races a lot more than any other kind of race condition; And I didn't say otherwise. Freedom from data races (with the caveat that there are also benign data races that you sometimes want to exploit and that you want language mechanisms for) is more or less a necessary byproduct of most schemes to reason about concurrency; but on its own, its woefully inadequate for the reasons that I talked about. > I'd guesstimate that avoiding them gets you 90+% of the way to thread safety. If this were the case, then you'd practically never have any problem with thread safety in actor languages; that is not the case. A simple and extremely common pattern where freedom from data races falls short is the following: if (obj->condition()) obj->action(); If `obj` were just a monitor (i.e. an object that guarantees atomicity for individual operations), the code still wouldn't be thread-safe. What you generally want is thread safety at the transactional level, not at the level of individual operations. Any genuinely thread-safe language requires mechanisms that operate at the transactional level (though, obviously, not necessarily literal transactions in the DB sense), i.e. sequences of operations that you want to be atomic or non-atomic only in a controllable fashion. (Though, at the same time, it is also necessary that any such mechanism provides escape hatches for when it would impede concurrency [3].) > Are there any practical / commonly used programming languages in which you can prove thread safety with that approach for significant programs? First, I am not saying that being able to formally prove properties is a necessary element of concurrency (though there are systems that do exactly that, but that's beyond the scope of what I mentioned). But even when you're reasoning about program behavior informally, that relies on the same principles. Your code assumes some precondition and wants to arrive at a postcondition and you have to be sure that other threads don't muck up what your code is trying to accomplish. The larger point is that with just the absence of data races, we still have a combinatorial explosion of ways that threads could interact with one another: most useful concurrency schemes (including Rust's) function by cutting down on that combinatorial explosion and limiting ways in which threads can interact with one another (and thus, possibly, in undesirable ways). [1] https://link.springer.com/chapter/10.1007/11424529_17 https://link.springer.com/chapter/10.1007/11424529_17 [2] https://onlinelibrary.wiley.com/doi/full/10.1002/cpe.3746 https://onlinelibrary.wiley.com/doi/full/10.1002/cpe.3746 [3] E.g. https://dl.acm.org/citation.cfm?doid=1297027.1297042; https://dl.acm.org/citation.cfm?doid=1297027.1297042; while the paper is about software transactional memory, the mechanism extends to critical regions in general.