as an [*erroneous execution*]{}, by [@Ada2012LRM 9.10§11].) The SC-for-DRF programming model and two relaxations were formalized for C++11 [@Boehm:cpp:mem]. They were later adopted for C11, OpenCL 2.0, and for X10 [@Zwinkau:x10:mem] (without the relaxations).

On the programming language level to guarantee DRF, means for synchronization (ordering operations) have to be provided. Ada’s POs are well-suited for this purpose. For non-blocking synchronization, atomic operations can be used to enforce an ordering between the memory accesses of two tasks. It is one goal of this paper to add language features to Ada such that atomic operations can be employed with DRF programs. To avoid ambiguity, we propose [synchronized]{} variables and types, which support the expression of memory ordering operations at a sufficient level of detail (see Sec. \[sec:sync:var\]).

The purpose of [synchronized]{} variables is that they can be used to safely transfer information (i.e., the value of the variables) from one task to another. ISAs provide atomic load/store instructions only for a limited set of primitive types. Beyond those, atomicity can only be ensured by locks. Nevertheless, computer architectures provide memory fences (see e.g., [@Herlihy:2012]) to provide means for ordering memory operations. A memory fence requires that all memory operations before the 