Title: Safe Non-blocking Synchronization in Ada 202x,
Abstract: The mutual-exclusion property of locks stands in the way to scalability of
parallel programs on many-core architectures. Locks do not allow progress
guarantees, because a task may fail inside a critical section and keep holding
a lock that blocks other tasks from accessing shared data. With non-blocking
synchronization, the drawbacks of locks are avoided by synchronizing access to
shared data by atomic read-modify-write operations. To incorporate non-blocking
synchronization in Ada~202x, programmers must be able to reason about the
behavior and performance of tasks in the absence of protected objects and
rendezvous. We therefore extend Ada's memory model by synchronized types, which
support the expression of memory ordering operations at a sufficient level of
detail. To mitigate the complexity associated with non-blocking
synchronization, we propose concurrent objects as a novel high-level language
construct. Entities of a concurrent object execute in parallel, due to a
fine-grained, optimistic synchronization mechanism. Synchronization is framed
by the semantics of concurrent entry execution. The programmer is only required
to label shared data accesses in the code of concurrent entries. Labels
constitute memory-ordering operations expressed through attributes. To the best
of our knowledge, this is the first approach to provide a non-blocking
synchronization construct as a first-class citizen of a high-level programming
language. We illustrate the use of concurrent objects by several examples.