https://blog.gopheracademy.com/advent-2017/go-execution-trac...
There might already be similar tools for Rust; I know less about what's available there.
(Go folks also added some tools for tracing across RPCs, which is less relevant to what you said but just kinda independently neat: https://medium.com/observability/debugging-latency-in-go-1-1...)
I prefer it for concurrency, but it's not a panacea. In particular, laziness is necessary for efficient immutable data structures, and immutable structures are a nice way to avoid some of the problems inherent in writing concurrent programs.
There are known algorithms/data structures where you either have to use immutability or laziness in order to get an efficient implementation.
Either you have a poor understanding of thread safety or Rust has solved the halting problem.
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.
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.
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.
What I really wish people would learn from Actors is that even if your programming language prevents trivial race conditions over shared memory or message passing primitives, none of that guarantees anything about the behavior of the system you are building once you start to compose those primitives. Gul Agha's dissertation was really eye-opening.
Languages like C++ and D treat this as a library design challenge, not a core language feature. Look at std::lock_guard, for example.
The thread safety is built using Send/Sync traits, which libraries for threading and synchronization primitives, atomics, etc. implement accordingly.
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.
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();
> 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.
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.
I wouldn't put it like that. You can (and almost certainly do) have data structures on the stack or heap that are not thread-safe (by which I mean they suffer from data races if accessed from multiple threads).
I'd say that Rust enforces that stuff that's available to multiple threads be thread-safe. That covers global variables (which are always assumed to be available to multiple threads; maybe this is what you mean by "doesn't even have a concept of a single-threaded program"). It also covers stuff passed to another thread in other ways (passed to the thread at construction time, sent over a channel, etc).
Rust describes thread safety with two traits: "Sync" (a type for which it is safe to share references between threads) and "Send" (a type that can safely be transferred across thread boundaries). The book talks more about these here: https://doc.rust-lang.org/book/ch16-04-extensible-concurrenc...
The neat thing is these are automatically implemented when doing so is safe[1], and the compiler requires them at the key spots. You don't need to rely on some half-trusted comment or other manual annotation declaring something as thread-safe or audit all the using code if you want to make something no longer thread-safe; code just won't compile if it's expecting something to be thread-safe that isn't.
The compiler tells you what the problem is, and in most cases, fixing it is simple: wrap something in a Mutex, replace a Rc with Arc (non-atomic reference count with an atomic one), replace a RefCell with a Mutex or RwLock. If it compiles and doesn't say "unsafe", there's no data race.
This is what people mean when they say Rust has "fearless concurrency". I'm not aware of any other language that guarantees lack of data races without giving up mutability or shared state.
(There are limits to the fearlessness, of course. You can still have data races by doing something dumb in code marked "unsafe". And Rust doesn't protect you against deadlocks at all, so you need to consider lock ordering and such as you would in most other languages. You can still have contention problems because your locking is too coarse. etc.)
[1] when you're doing something unsafe you might need to manually declare something as Send and/or Sync because the compiler can't figure that on its own that doing so is safe. I've encountered this when doing FFI; another case would be when implementing synchronization primitives. Most code shouldn't have to deal with this.
The borrow checker basically doesn't even have a concept of a single-threaded program. Everything you write in Rust is required to be thread-safe. This makes Rust appear more difficult, but it's just front-loading the effort required to make the whole program thread-safe (which to me felt nearly impossible for non-trivial C programs). From there you can sprinkle Rayon all over the place, send async work over channels, etc.
The piece I'm missing is "Amdahl's-law-aware" profiler that would show not just where any code spends time, but only where the unparallelized bottlenecks spend time.