Obviously no language can prevent race conditions. Race conditions are usually a flaw of protocol or api design. The whole point of 'fearless concurrency' is that you won't crash because of shared state.
To stay on topic: https://docs.adacore.com/spark2014-docs/html/ug/en/source/co... and https://blog.adacore.com/gnat-community-2020-is-here are worth a read.
Additionally:
> The Ada concurrency model is based on the notion of task, a unit of concurrency that represents an independent thread of control. All, the tasks and the mechanisms for inter-task communication and synchronization, are introduced at language level in order to allow building safer programs. As an illustration, Ada 95 introduced protected objects to allow controlling how data is accessed, thus eliminating race conditions. Additionally, in 1997, Burns et al. introduced the Ravenscar profile, a subset of the Ada programming language that allows high integrity applications to be analyzed for their timing properties by pursuing three main goals: (1) ensuring predictable execution, (2) simplifying the runtime support, and (3) eliminating constructs with high overhead. The limitations imposed by the Ravenscar profile have an inevitable impact in the complexity of correctness analyses, e.g. tasks can only communicate through shared objects (tasks entries are not allowed, so the rendezvous mechanism cannot be used), tasks are assumed to be non-terminating, and tasks and protected objects cannot be dynamically allocated.
> Along the same lines, SPARK, a language that subsets Ada to enable the formal verification of programs, eliminates race conditions by forcing any global object referenced from a task to be marked as Part Of that task, or be a synchronized object.
I think I have a comment about Ada's concurrency where I get into it in more detail (IIRC).
Then Pascal/Algol syntax is not cool, so you always get a bit of push back on a world that now breaths curly brackets.
However NVidia has recently chosen Ada/SPARK for their security critical firmware, so there's that.
Community building.
That said, Nim is very much inspired by Ada for the future safety features, in particular Z3 integration to enable Spark-like use-cases
- https://nim-lang.org/docs/drnim.html
AFAIK Ada was also inspired by Rust for memory-related safety. I find the cross-pollination between languages fascinating.
WHat's the multithreading story of Ada like? I didn't find that much code or article or papers when I was searching for multithreading runtime in other languages.
Actually, it is the pointer support in the SPARK variant of Ada that was inspired by Rust's ownership/borrower semantic. Originally, SPARK didn't allow any pointer usage, but with the new ownership/borrower semantics, SPARK allows limited usage of Ada pointers.
As for more literature about using Ada's tasking features, I recommend the wonderful books and papers by Alan Burns and/or Andy Wellings, such as "Concurrent and Real-Time Programming In Ada (3rd Edition)." AdaCore has an old presentation on using Ravenscar with multi-core processors (https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/ev...). There are more articles on the internet on Ada Ravenscar tasking profile and full Ada tasking.
Recently AdaCore announced they are adding support for CUDA applications in SPARK (https://developer.nvidia.com/gtc/2020/video/s21122-vid)
It requires the use of unsafe on the Rust side, and you better code it very carefully.
And that's... a problem. Because a lot of code that actually wants concurrency in the same memory space is code that also wants high performance. And Rust serves these applications well in other areas, where "Just as fast as C" is true.
But Rust isn't as fast as "C" here. It's demonstrably slower. Is that a good thing? I honestly don't know.
It's just a hard problem. But you can't eliminate the idea of "shared locked memory" by fiat. It's a real requirement, and Rust has little to say about it in its standard library or (IIRC, though I'd have to go check) its memory model and locking primitives. It's sort of a no-mans land of "super unsafe outside the box" code. And that's a pity.
> It's a real requirement, and Rust has little to say about it in its standard library
So, I don't know much about concurrency, but you're looking for like, a Mutex, right? They're in the standard library and used all the time.
https://doc.rust-lang.org/stable/std/sync/struct.Mutex.html
And RwLock, a variant on Mutex that allows either one writer or multiple concurrent readers:
https://doc.rust-lang.org/stable/std/sync/struct.RwLock.html
That isn't how Rust works. There are mutexes, condvars, atomics, etc. in the standard library. You don't need the unsafe keyword; go nuts with them.