> 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).
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` 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
[2] https://onlinelibrary.wiley.com/doi/full/10.1002/cpe.3746
[3] E.g. 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.