Higher language features for weak memory models

Abstract

Modern parallel applications demand synchronization primitives that offer both progress guarantees and high performance. The programming language Ada currently lacks a formally defined memory consistency model and provides only lock-based synchronization via protected objects, which can lead to unbounded blocking and deadlocks under high contention. This thesis extends the Ada programming language with higher-level constructs for non-blocking synchronization. We modify the GCC precompiler to introduce three new syntactic constructs: an atomic block that maps a sequence of assignments to a Multi-Word Compare-And-Swap (MWCAS) operation, a concurrent keyword that declares a concurrent object backed by MWCAS instead of locks, and a Wait\_Free aspect that automatically wraps the concurrent object's procedures in a helping protocol, transforming a lock-free algorithm into a wait-free one. We validate our implementation on a concurrent red-black tree, comparing three variants: a blocking tree using Ada protected bodies, a lock-free tree using MWCAS for node recoloring, and a wait-free tree obtained by adding the Wait\_Free aspect. Benchmarks on an 8-core, 16-thread machine show that the blocking tree is fastest on a single thread, but degrades when increasing threads. Finally, we demonstrate that the wait-free guarantee is achieved at an acceptable overhead.