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