---
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.
author:
- Johann Blieberger and Bernd Burgstaller
title: 'Safe Non-blocking Synchronization in Ada 202x'
---

[Introduction\[sec:intro\]]{}

Mutual exclusion locks are the most common technique to synchronize multiple tasks to access shared data. Ada’s protected objects (POs) implement the monitor-lock concept [@Hoare:monitors]. Method-level locking requires a task to acquire an exclusive lock to execute a PO’s entry or procedure. (Protected functions allow concurrent read-access in the style of a readers–writers lock [@Herlihy:2012].) Entries and procedures of a PO thus effectively execute one after another, which makes it straight-forward for programmers to reason about updates to the shared data encapsulated by a PO. Informally, sequential consistency ensures that method calls act as if they occurred in a sequential, total order that is consistent with the program order of each participating task. I.e., for any concurrent execution, the method calls to POs can be ordered sequentially such that they (1) are consistent with program order, and (2) meet each PO’s specification (pre-condition, side-effect, post-condition) [@Herlihy:2012].

Although the sequential consistency semantics of mutual exclusion locks facilitate reasoning about programs, they nevertheless introduce potential concurrency bugs such as dead-lock, live-lock and priority inversion. The mutual-exclusion property of (highly-contended) locks stands in the way to scalability of parallel programs on many-core architectures [@Scott:Sync]. Locks do not allow progress guarantees, because a task may fail inside a critical section (e.g., by entering an endless loop), preventing other tasks from accessing shared data.

Given the disadvantages of mutual exclusion locks, it is thus desirable to give up on method-level locking and allow method calls to overlap in time. Synchronization is then performed on a finer granularity within a method’s code, via atomic [*read-modify-write*]{} (RMW) operations. In the absence of mutual exclusion locks, the possibility of task-failure inside a critical section is eliminated, because critical sections are reduced to single atomic operations. These atomic operations are provided either by the CPU’s instruction set architecture (ISA), or the language run-time (with the help of the CPU’s ISA). It thus becomes possible to provide progress guarantees, which are unattainable with locks. In particular, a method is [*non-blocking*]{}, if a task’s pending invocation is never required to wait for another task’s pending invocation to complete [@Herlihy:2012].

[ll@l]{}

    -- Initial values:
    Flag := False;
    Data := 0;

\

– Task 1: Data := 1; |\[l:t1:store:1\]| Flag := True; |\[l:t1:store:2\]|

&

– Task 2: loop|\[l:spin:1\]| R1 := Flag; exit when R1; end loop; |\[l:spin:2\]| R2 := Data; |\[l:read\]|

&

Data : Integer with Volatile; Flag : Boolean with Atomic;

\
&

Non-blocking synchronization techniques are notoriously difficult to implement and the design of non-blocking data structures is an area of active research. To enable non-blocking synchronization, a programming language must provide a strict memory model. The purpose of a memory model is to define the set of values a read operation in a program is allowed to return [@Boehm:mem:survey].

To motivate the need for a strict memory model, consider the producer-consumer synchronization example in Fig. \[fig:mem:example\](a) (adopted from [@Hill:CSprimer] and [@Barnes:RationaleAda2012]). The programmer’s intention is to communicate the value of variable [Data]{} from Task 1 to Task 2. Without explicitly requesting a sequentially consistent execution, a compiler or CPU may break the programmer’s intended synchronization via the [Flag]{} variable by re-ordering memory operations that will result in reading [R2 = 0]{} in Line \[l:read\] of Task 2. (E.g., a store–store re-ordering of the assignments in lines \[l:t1:store:1\] and \[l:t1:store:2\] of Task 1 will allow this result.) In Ada 2012, such re-orderings can be ruled out by labeling variables [Data]{} and [Flag]{} by aspect [volatile]{}. The corresponding variable declarations are depicted in Fig. \[fig:mem:example\](b). (Note that by [@Ada2012LRM C.6§8/3] aspect [atomic]{} implies aspect [volatile]{}, but not vice versa.)

The intention for volatile variables in Ada 2012 was to guarantee that all tasks agree on the same order of updates [@Ada2012LRM C.6§16/3]. Updates of volatile variables are thus required to be sequentially consistent, in the sense of Lamport’s definition [@Lamport:SC]: “[*With sequential consistency (SC), any execution has a total order over all memory writes and reads, with each read reading from the most recent write to the same location*]{}”.

However, the Ada 2012 aspect [volatile]{} has the following shortcomings:

1.  Ensuring SC for multiple tasks without atomic access is impossible. Non-atomic volatile variables therefore should not be provided by the language. Otherwise, the responsibility shifts from the programming language implementation to the programmer to ensure SC by pairing an atomic (implied volatile) variable with each non-atomic volatile variable (see, e.g., Fig. \[fig:mem:example\](b) and [@Simpson1990] for examples). (Note that a programming language implementation may ensure atomicity by a mutual exclusion lock if no hardware primitives for atomic access to a particular type of shared data are available.)

2.  Requiring SC on all shared variables is costly in terms of performance on contemporary multi-core CPUs. In Fig. \[fig:mem:example\], performance can be improved by allowing a less strict memory order for variable [Data]{} (to be addressed in Section \[sec:mm\]).

3.  Although Ada provides the highly abstract PO monitor-construct for blocking synchronization, there is currently no programming primitive available to match this abstraction level for non-blocking synchronization.

Contemporary CPU architectures relax SC for the sake of performance [@Adve:SMC:tutorial; @Hennessy:acquire:release; @Hill:CSprimer]. It is a challenge for programming language designers to provide safe, efficient and user-friendly non-blocking synchronization features. The original memory model for Java contained problems and had to be revised [@Manson:JMM]. It was later found to be unsound with standard compiler optimizations [@Sevcik:JVM:CC:problems]. The C++11 standard (cf.[@c++11; @will:c++]) has already specified a strict memory model for concurrent and parallel computing. We think that C++11 was not entirely successful both in terms of safety and in terms of being user-friendly. In contrast, we are convinced that these challenges can be met in the upcoming Ada 202x standard.

It has been felt since Ada 95 that it might be advantageous to have language support for synchronization based on atomic variables. For example, we cite [@Ada95rat C.1]: [*“A need to access specific machine instructions arises sometimes from other considerations as well. Examples include instructions that perform compound operations atomically on shared memory, such as test-and-set and compare-and-swap, and instructions that provide high-level operations, such as translate-and-test and vector arithmetic.”*]{}

Ada is already well-positioned to provide a strict memory model in conjunction with support for non-blocking synchronization, because it provides tasks as first-class citizens. This rules out inconsistencies that may result from thread-functionality provided through libraries [@Boehm:thread:library].

To provide safe and efficient non-blocking synchronization for Ada 202x, this paper makes the following contributions:

1.  We extend Ada’s memory model by introducing synchronized types, which allow the expression of memory ordering operations consistently and at a sufficient level of detail. Memory ordering operations are expressed through aspects and attributes. Language support for spin loop synchronization via [synchronized]{} variables is proposed.

2.  We propose [*concurrent objects*]{} (COs) as a high-level language construct to express non-blocking synchronization. COs are meant to encapsulate the intricacies of non-blocking synchronization as POs do for blocking synchronization. Contrary to POs, the entries and procedures of COs execute in parallel, due to a fine-grained, optimistic synchronization mechanism.

3.  We provide an alternative, low-level API on synchronized types, which provides programmers with full control over the implementation of non-blocking synchronization semantics. Our main purpose with the low-level API is to provoke a discussion on the trade-off between abstraction versus flexibility.

4.  We illustrate the use of concurrent objects and the alternative, low-level API by several examples.

The remainder of this paper is organized as follows. We summarize the state-of-the-art on memory models and introduce synchronized variables in Sec. \[sec:mm\]. We introduce attributes for specifying memory ordering operations in Sec. \[aspects\]. We specify concurrent objects in Sec. \[nbPO\] and discuss task scheduling in the presence of COs in Sec. \[sched\]. Sec. \[sec:examples\] contains two CO example implementations with varying memory consistency semantics. We discuss our low-level API in Sec. \[API\_sec\]. Sec. \[sec:concl\] contains our conclusions.

This paper is an extension of work that appeared at the Ada-Europe 2018 conference [@BB:2018]. Additional material is confined to two appendices: Appendix \[sec:rationale\] states the design-decisions of our proposed non-blocking synchronization mechanisms. Appendix \[app:examples\] contains further examples.

[The Memory Model\[sec:mm\]]{}

For reasons outlined in Sec. \[sec:intro\], we do not consider the Ada 2012 atomic and volatile types here. Rather, we introduce [*[synchronized]{}*]{} types and variables. Synchronized types provide atomic access. We propose aspects and attributes for specifying a particular memory model to be employed for reading/writing [synchronized]{} variables.

Modern multi-core computer architectures are equipped with a memory hierarchy that consist of main memory, caches and registers. It is important to distinguish between memory consistency and coherence. We cite from [@Hill:CSprimer]: [*‘For a shared memory machine, the memory consistency model defines the architecturally visible behavior of its memory system. Consistency definitions provide rules about loads and stores (or memory reads and writes) and how they act upon memory. As part of supporting a memory consistency model, many machines also provide cache coherence protocols that ensure that multiple cached copies of data are kept up-to-date.’*]{}

The purpose of a memory consistency model (or memory model, for short) is to define the set of values a read operation is allowed to return [@Boehm:mem:survey]. To facilitate programmers’ intuition, it would be ideal if all read/write operations of a program’s tasks are sequentially consistent. However, the hardware memory models provided by contemporary CPU architectures relax SC for the sake of performance [@Adve:SMC:tutorial; @Hennessy:acquire:release; @Hill:CSprimer]. Enforcing SC on such architectures may incur a noticeable performance penalty. The workable middle-ground between intuition (SC) and performance (relaxed hardware memory models) has been established with SC for data race-free programs (SC-for-DRF) [@Hill:DRF:SC]. Informally, a program has a data race if two tasks access the same memory location, at least one of them is a write, and there are no intervening synchronization operations that would order the accesses. “SC-for-DRF” requires programmers to ensure that programs are free of data races under SC. In turn, the relaxed memory model of a SC-for-DRF CPU guarantees SC for all executions of such a program.

It has been acknowledged in the literature [@Boehm:mem:survey] that Ada 83 was perhaps the first widely-use high-level programming language to provide first-class support for shared-memory programming. The approach taken with Ada 83 and later language revisions was to require legal programs to be without synchronization errors, which is the approach taken with SC-for-DRF. In contrast, for the Java memory model it was perceived that even programs with synchronization errors shall have defined semantics for reasons of safety and security of Java’s sand-boxed execution environment. (We do not consider this approach in the remainder of this paper, because it does not align with Ada’s current approach to regard the semantics of programs with synchronization errors as undefined, i.e., 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 fence (in program order) must be committed to the memory hierarchy before any operation after the fence. Then, for data to be transferred from one thread to another it is not necessary to be atomic anymore. I.e., it is sufficient that (1) the signaling variable is atomic, and that (2) all write operations are committed to the memory hierarchy before setting the signaling variable. On the receiver’s side, it must be ensured that (3) the signaling variable is read atomically, and that (4) memory loads for the data occur after reading the signaling variable (Listing \[genRA\] provides an example.)

In addition to [synchronized]{} variables, [synchronized]{} types and attribute are convenient means for enhancing the usefulness of [synchronized]{} variables.

The general idea of our proposed approach is to define [*non-blocking*]{} [concurrent]{} objects similar to protected objects (cf. e.g., [@Herlihy:2012]). However, entries of [concurrent]{} objects will not block on guards; they will spin loop until the guard evaluates to true. In addition, functions, procedures, and entries of [concurrent]{} objects are allowed to execute and to modify the encapsulated data in parallel. Private entries for [concurrent]{} objects are also supported. It is their responsibility that the data provides a consistent view to the users of the [concurrent]{} object. [Concurrent]{} objects will use [synchronized]{} types for synchronizing data access. Several memory models are provided for doing this efficiently. It is the responsibility of the programmer to ensure that the entries of a [concurrent]{} object are free from data races (DRF). For such programs, the non-blocking semantics of a [concurrent]{} object will provide SC in the same way as protected objects do for blocking synchronization.

[Synchronizing memory operations and enforcing ordering]{}

For defining ordering relations on memory operations, it is useful to introduce some other useful relations.

The [*synchronizes-with*]{} relation can be achieved only by use of atomic types. Even if monitors or protected objects are used for synchronization, the runtime implements them employing atomic types. The general idea is to equip read and write operations on an atomic variable with information that will enforce an ordering on the read and write operations. Our proposal is to use attributes for specifying this ordering information. Details can be found below.

The [*happens-before*]{} relation is the basic relation for ordering operations in programs. In a program consisting of only one single thread, happens-before is straightforward. For inter-thread happens-before relations the synchronizes-with relation becomes important. If operation [X]{} in one thread synchronizes-with operation [Y]{} in another thread, then [X]{} happens-before [Y]{}. Note that the happens-before relation is transitive, i.e., if [X]{} happens-before [Y]{} and [Y]{} happens-before [Z]{}, then [X]{} happens-before [Z]{}. This is true even if [X]{}, [Y]{}, and [Z]{} are part of different threads.

We define different memory models. These memory models originated from the DRF [@Hill:DRF:SC] and properly-labeled [@Hennessy:acquire:release] hardware memory models. They were formalized for the memory model of C++ [@Boehm:cpp:mem]. The “sequentially consistent” and “acquire-release” memory models provide SC for DRF. The models can have varying costs on different computer architectures. The “acquire-release” memory model is a relaxation of the “sequentially consistent” memory model. As described in Table \[MMcompcpu\], it requires concessions from the programmer to weaken SC in turn for more flexibility for the CPU to re-order memory operations.

Sequentially Consistent Ordering

:   is the most stringent model and the easiest one for programmers to work with. In this case all threads see the same, total order of operations. This means, a sequentially consistent write to a [synchronized]{} variable synchronizes-with a sequentially-consistent read of the same variable.

Relaxed Ordering

:   does not obey synchronizes-with relationships, but operations on the same [synchronized]{} variable within a single thread still obey happens-before relationships. This means that although one thread may write a [synchronized]{} variable, at a later point in time another thread may read an earlier value of this variable.

Acquire-Release Ordering

:   when compared to relaxed ordering introduces some synchronization. In fact, a read operation on [synchronized]{} variables can then be labeled by [*acquire*]{}, a write operation can be labeled by [*release*]{}. Synchronization between release and acquire is pairwise between the thread that issues the release and that acquire operation of a thread that does the first read-acquire after the release.[^1] A thread issuing a read-acquire later may read a different value than that written by the first thread.

  ------------------------ ------------------ -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  [**memory order**]{}      [**involved**]{}  [**constraints for reordering memory accesses**]{}
                            [**threads**]{}   [**(for compilers and CPUs)**]{}
  relaxed                          1          no inter-thread constraints
  release/acquire                  2          \(1) ordinary stores originally before [release]{} (in program order) will happen before the release fence (after compiler optimizations and CPU reordering)(2) ordinary loads originally after [acquire]{} (in program order) will take place after the acquire fence (after compiler optimizations and CPU reordering)
  sequentiallyconsistent          all         \(1) all memory accesses originally before the [sequentially\_consistent]{} one (in program order) will happen before the fence (after compiler optimizations and CPU reordering)(2) all memory accesses originally after the [sequentially\_consistent]{} one (in program order) will happen after the fence (after compiler optimizations and CPU reordering)
  ------------------------ ------------------ -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

  : Memory Order and Constraints for Compilers and CPUs[]{data-label="MMcompcpu"}

\
 \

It is important to note, that the semantics of the models above have to be enforced by the compiler (for programs which are DRF). I.e., the compiler “knows” the relaxed memory model of the hardware and inserts memory fences in the machine-code such that the memory model of the high-level programming language is enforced. Compiler optimizations must ensure that reordering of operations is performed in such a way that the semantics of the memory model are not violated. The same applies to CPUs, i.e., reordering of instructions is done with respect to the CPU’s relaxed hardware memory model, constrained by the ordering semantics of fences inserted by the compiler. The constraints enforced by the memory model are summarized in Table \[MMcompcpu\].

[Synchronization primitives]{}\[aspects\]

[[Synchronized]{} Variables\[sec:sync:var\]]{} [Synchronized]{} variables can be used as atomic variables in Ada 2012, the only exception being that they are declared inside the lexical scope (data part) of a [concurrent]{} object. In this case aspects and attributes used in the implementation of the [concurrent]{} object’s operations (functions, procedures, and entries) are employed for specifying behavior according to the memory model. Variables are labeled by the boolean aspect [[Synchronized]{}]{}.

Read accesses to [synchronized]{} variables in the implementation of the [concurrent]{} object’s operations may be labeled with the attribute [Concurrent\_Read]{}, write accesses with the attribute [Concurrent\_Write]{}. Both attributes have a parameter [Memory\_Order]{} to specify the memory order of the access. (If the operations are not labeled, the default values given below apply.) In case of read accesses, values allowed for parameter [Memory\_Order]{} are [Sequentially\_Consistent]{}, [Acquire]{}, and [Relaxed]{}. The default value is [Sequentially\_Consistent]{}. For write accesses the values allowed are [Sequentially\_Consistent]{}, [Release]{}, and [Relaxed]{}. The default value is again [Sequentially\_Consistent]{}.

For example, assigning the value of [synchronized]{} variable [Y]{} to [synchronized]{} variable [X]{} is given like In addition we propose aspects for specifying variable specific default values for the attributes described above. In more detail, when declaring [synchronized]{} variables the default values for read and write accesses can be specified via aspects [Memory\_Order\_Read]{} and [Memory\_Order\_Write]{}. The allowed values are the same as those given above for read and write accesses. If these memory model aspects are given when declaring a [synchronized]{} variable, the attributes [Concurrent\_Read]{} and [Concurrent\_Write]{} need not be given for actual read and write accesses of this variable. However, these attributes may be used to temporarily over-write the default values specified for the variable by the aspects. For example\
\
\
…\
;\
does the same as the example above but without spoiling the assignment statement.

Aspect [Synchronized\_Components]{} relates to aspect [Synchronized]{} in the same way as [Atomic\_Components]{} relates to [Atomic]{} in Ada 2012.

[Read-Modify-Write Variables]{} If a variable inside the data part of a [concurrent]{} object is labeled by the aspect [Read\_Modify\_Write]{}, this implies that the variable is [synchronized]{}. Write access to a read-modify-write variable in the implementation of the protected object’s operations is a read-modify-write access. The read-modify-write access is done via the attribute [Concurrent\_Exchange]{}. The two parameters of this attribute are [Memory\_Order\_Success]{} and [Memory\_Order\_Failure]{}. The first specifies the memory order for a successful write, the second one the memory order if the write access fails (and a new value is assigned to the variable).

[Memory\_Order\_Success]{} is one of [Sequentially\_Consistent]{}, [Acquire]{},, and [Relaxed]{}.

[Memory\_Order\_Failure]{} may be one of [Sequentially\_Consistent]{}, [Acquire]{}, and [Relaxed]{}. The default value for both is [Sequentially\_Consistent]{}. For the same read-modify-write access the memory order specified for failure must not be stricter than that specified for success. So, if [Memory\_Order\_Failure =&gt; Acquire]{} or [Memory\_Order\_Failure =&gt; Sequentially\_Consistent]{} is specified, these have also be given for success.

For read access to a read-modify-write variable, attribute [Concurrent\_Read]{} has to be used. The parameter [Memory\_Order]{} has to be given. Its value is one of [Sequentially\_Consistent]{}, [Acquire]{}, [Relaxed]{}. The default value is.

Again, aspects for variable specific default values for the attributes described above may be specified when declaring a read-modify-write variable. The aspects are [Memory\_Order\_Read]{}, [Memory\_Order\_Write\_Success]{}, and with allowed values as above.

[Synchronization Loops]{} As presented below synchronization by [synchronized]{} variables is performed via spin loops. We call these loops [*sync loops*]{}.

[[Concurrent]{} Objects]{}\[nbPO\]

[Non-Blocking Synchronization]{}

Besides the aspects and attributes proposed in Section \[aspects\] that have to be used for implementing [concurrent]{} objects, [concurrent]{} objects are different from protected objects in the following way. All operations of [concurrent]{} objects can be executed in parallel. [Synchronized]{} variables have to be used for synchronizing the executing operations. Entries have Boolean-valued guards. The Boolean expressions for such guards may contain only [synchronized]{} variables declared in the data part of the protected object and constants. Calling an entry results either in immediate execution of the entry’s body if the guard evaluates to [true]{}, or in spin-looping until eventually the guard evaluates to [true]{}. We call such a spin loop [*sync loop*]{}.

[Read-Modify-Write Synchronization]{}

For [concurrent]{} objects with read-modify-write variables the attributes proposed in Section \[aspects\] apply. All operations of [concurrent]{} objects can be executed in parallel. Read-modify-write variables have to be used for synchronizing the executing operations. The guards of entries have to be of the form [X = X’OLD]{} where [X]{} denotes a read-modify-write variable of the [concurrent]{} object. The attribute [OLD]{} is well-known from postconditions. An example in our context can be found in Listing \[lfsada\].

If during the execution of an entry a read-modify-write operation is reached, that operation might succeed immediately, in which case execution proceeds after the operation in the normal way. If the operation fails, the whole execution of the entry is restarted ([*implicit sync loop*]{}). In particular, only the statements being data-dependent on the read-modify-write variable are re-executed. Statements not being data-dependent on the read-modify-write variables are executed only on the first try.[^2] Precluding non-data-dependent statements from re-execution is not only a matter of efficiency, it sometimes makes sense semantically, e.g., for adding heap management to an implementation.

[Scheduling and Dispatching]{}\[sched\]

We propose a new state for Ada tasks to facilitate correct scheduling and dispatching for threads synchronizing via [synchronized]{} or read-modify-write types. If a thread is in a sync loop, the thread state changes to “in\_sync\_loop”. Note that sync loops can only happen inside [concurrent]{} objects. Thus they can be spotted easily by the compiler and cannot be confused with “normal” loops. Note also that for the state change it makes sense not to take place during the first iteration of the sync loop, because the synchronization may succeed immediately. For read-modify-write loops, iteration from the third iteration on may be a good choice; for spin loops, an iteration from the second iteration on may be a good choice.

In this way the runtime can guarantee that not all available CPUs (cores) are occupied by threads in state “in\_sync\_loop”. Thus we can be sure that at least one thread makes progress and finally all [synchronized]{} or read-modify-write variables are released (if the program’s synchronization structure is correct and the program does not deadlock).

After leaving a sync loop, the thread state changes back to “runable”.

[Examples]{}\[sec:examples\]

[Non-blocking Stack.]{}\[lfs\] Listing \[lfsada\] shows an implementation of a non-blocking stack using our proposed new syntax for [concurrent]{} objects. Implementation of entry [Push]{} (lines \[lfs:pushb\]–\[lfs:pushe\]) behaves as follows. In Line \[lfs:newb\] a new element is inserted at the head of the list. Pointer [Next]{} of this element is set to the current head. The next statement (Line \[lfs:rmwo\]) assigns the new value to the head of the list. Since variable [Head]{} has aspect [Read\_Modify\_Write]{} (line \[lfs:rmw\]), this is done with RMW semantics, i.e., if the value of [Head]{} has not been changed (since the execution of [Push]{} has started) by a different thread executing [Push]{} or [Pop]{} (i.e., [Head = Head’OLD]{}), then the RMW operation succeeds and execution proceeds at Line \[lfs:pushe\], i.e., [Push]{} returns. If the value of [Head]{} has been changed ([Head /= Head’OLD]{}), then the RMW operation fails and entry [Push]{} is re-executed starting from Line \[lfs:newb\]. Line \[lfs:new\] is not re-executed as it is not data dependent on [Head]{}.

Several memory order attributes apply to the RMW operation (Line \[lfs:rmwo\]) which are given in lines \[lfs:mmb\]–\[lfs:mme\]: In case of a successful execution of the RMW, the value of [Head]{} is released such that other threads can read its value via memory order acquire. In the failure case the new value of [Head]{} is assigned to the “local copy” of [Head]{} (i.e., [Head’OLD]{}) via relaxed memory order. “Relaxed” is enough because RMW semantics will detect if the value of [Head]{} has been changed by a different thread anyway. The same applies to “Relaxed” in Line \[lfs:new\].

Implementation of entry [Pop]{} (lines \[lfs:popb\]–\[lfs:pope\]) follows along the same lines.

Memory management needs special consideration: In our case it is enough to use a [synchronized]{} counter that counts the number of threads inside [Pop]{}. If the counter equals $1$, memory can be freed. Ada’s storage pools are a perfect means for doing this without spoiling the code.

This example also shows how easy it is to migrate from a (working) blocking to a (working) non-blocking implementation of a program. Assume that a working implementation with a protected object exists, then one has to follow these steps:

1.  Replace keyword [protected]{} by keyword [concurrent]{}.

2.  Replace protected operations by DRF [concurrent]{} operations, thereby adding appropriate guards to the [concurrent]{} entries.

3.  Test the non-blocking program which now has default memory order.

4.  Carefully relax the memory ordering requirements: Add memory order aspects and/or attributes [Acquire]{}, [Release]{}, and/or [Relaxed]{} to improve performance but without violating memory consistency.

[Generic Release-Acquire Object.]{} Listing \[genRA\] shows how release-acquire semantics can be implemented for general data structures with help of one synchronized Boolean.

[API]{}\[API\_sec\]As already pointed out, we feel that providing concurrent objects as first-class citizens is the right way to enhance Ada with non-blocking synchronization on an adequate memory model. On the other hand, if the programmer needs synchronization on a lower level than [concurrent]{} objects provide, an API-based approach (generic function [Read\_Modify\_Write]{} in package [Memory\_Model]{}) would be a viable alternative. Listing \[packmm\] shows such a predefined package [Memory\_Model]{}. It contains the specification of generic function [Read\_Modify\_Write]{}, which allows to use the read-modify-write operation of the underlying computer hardware[^3]. Exposing sync loops to the programmer makes it necessary to introduce a new aspect [sync\_loop]{} to let the runtime perform the state change to “in\_sync\_loop” (cf. Section \[sched\]). Because nobody can force the programmer to use this aspect correctly, the information transferred to the runtime may be false or incomplete, giving rise to concurrency defects such as deadlocks, livelocks, and other problems.

[Conclusion and Future Work\[sec:concl\]]{}

We have presented an approach for providing safe non-blocking synchronization in Ada 202x. Our novel approach is based on introducing concurrent objects for encapsulating non-blocking data structures on a high abstraction level. In addition, we have presented [synchronized]{} and read-modify-write types which support the expression of memory ordering operations at a sufficient level of detail. Concurrent objects provide SC for programs without data races. This SC-for-DRF memory model is well-aligned with Ada’s semantics for blocking synchronization via protected objects, which requires legal programs to be without synchronization errors ([@Ada2012LRM 9.10§11]).

Although Ada 2012 provides the highly abstract protected object monitor-construct for blocking synchronization, there was previously no programming primitive available to match this abstraction level for non-blocking synchronization. The proposed memory model in conjunction with our concurrent object construct for non-blocking synchronization may bar users from having to invent ad-hoc synchronization solutions, which have been found error-prone with blocking synchronization already [@AdHocSync].

Until now, all previous approaches are based on APIs. We have listed a number of advantages that support our approach of making non-blocking data structures first class language citizens. In contrast, our approach for Ada 202x encapsulates non-blocking synchronization inside [concurrent]{} objects. This safe approach makes the code easy to understand. Note that [concurrent]{} objects are not orthogonal to objects in the sense of OOP (tagged types in Ada). However, this can be achieved by employing the proposed API approach (cf. Section \[API\_sec\]). In addition, it is not difficult to migrate code from blocking to non-blocking synchronization. Adding memory management via storage pools integrates well with our modular approach and does not clutter the code.

A lot of work remains to be done. To name only a few issues: Non-blocking barriers (in the sense of [@Ada2012LRM D.10.1]) would be useful; details have to be elaborated. Fully integrating concurrent objects into scheduling and dispatching models and integrating with the features for parallel programming planned for Ada 202x have to be done carefully.

Acknowledgments
===============

This research was supported by the Austrian Science Fund (FWF) project I 1035N23, and by the Next-Generation Information Computing Development Program through the National Research Foundation of Korea (NRF), funded by the Ministry of Science, ICT & Future Planning under grant NRF2015M3C4A7065522.

[Rationale and comparison with C++11\[sec:rationale\]]{}

We state the rationale for our proposed language features and compare them to the C++ memory model. This section thus requires modest familiarity with the C++11 standard [@c++11].

C++11’s [compare\_exchange\_weak]{} and [compare\_exchange\_strong]{}
---------------------------------------------------------------------

We felt that [compare\_exchange\_weak]{} and [compare\_exchange\_strong]{} are not needed on language level. These are hardware-related details which the compiler knows and should anticipate without intervention of the programmer.

In particular, [compare\_exchange\_weak]{} means that sometimes a RMW operation fails although the value of the RMW variable has not been changed by a different thread. In this case re-executing the whole implicit sync loop is not necessary, only the RMW operation has to be redone. We assume that the compiler produces machine code for this “inner” loop. Because this is only the case on very peculiar CPUs, it is obvious that the compiler and not the programmer should take care of this.

In addition, migrating Ada programs will be facilitated by assigning this job to the compiler.

C++11’s [consume]{} memory ordering
-----------------------------------

C++ introduced [memory\_order\_consume]{} specifically for supporting read-copy update (RCU) used in the Linux Kernel (cf. [@preshing:consume]). However, it turned out that [memory\_order\_consume]{} as defined in the C++ standard [@c++11] is not implemented by compilers. Instead, all compilers map it to [memory\_order\_acquire]{}. The major reason for this is that the data dependency as defined in [@c++11] is difficult to implement (cf., e.g., [@N4036:14]). There is, however, ongoing work within ISOCPP to make [memory\_order\_consume]{} viable for implementation (cf., e.g., [@P0462R1:17; @P0190R4:17]). In particular,  [@P0190R4:17] proposes to restrict [memory\_order\_consume]{} to data dependence chains starting with pointers because this represents the major usage scenario in the Linux kernel.

For Ada 202x it seems reasonable not to include [memory\_order\_consume]{} in the standard. Instead, compilers are encouraged to exploit features provided by the hardware for gaining performance on weakly-ordered CPUs. The programmer uses [memory\_order\_release]{} and [memory\_order\_acquire]{} for synchronization and the compiler improves the performance of the program if the hardware is weakly-ordered and it (the compiler) is willing to perform data dependency analysis. In addition, a compiler switch might be a way for letting the programmer decide whether she is willing to bare the optimization load (increased compile time).

In addition, migrating Ada programs will be facilitated by not having to replace [memory\_order\_acquire]{} with [memory\_order\_consume]{} and vice versa depending on the employed hardware.

C++11’s [acquire\_release]{} memory ordering
--------------------------------------------

C++11 defines [acquire\_release]{} memory ordering because some of C++11’s RMW operations contain both a read and a write operation, e.g., [i++]{} for [i]{} being an atomic integer variable. Because Ada’s syntax does not contain such operators, [acquire\_release]{} memory ordering is not needed on language level. Compiling [i := i+1]{} ([i]{} being an atomic integer variable), an Ada compiler is able to employ suitable memory fences to ensure the memory model aspects given by the programmer together with the original statement.

[Further Examples]{}\[app:examples\]

[Peterson’s Algorithm.]{} Listing \[peterson\] shows an implementation of Peterson’s algorithm, a method for lock-free synchronizing two tasks, under the sequentially consistent memory model.

Listing \[peterson\_ra\_new\] shows an implementation of Peterson’s algorithm under the release-acquire memory model with default memory model specified in the declarative part.

Listing \[peterson\_ra\] shows an implementation of Peterson’s algorithm under the release-acquire memory model with memory model explicitly specified at statements.

[Filter Algorithm.]{} The filter algorithm is a non-blocking method for synchronizing $n$ processes, which is starvation and deadlock free ([@Herlihy:2012]). Listing \[filter\] is an implementation using our proposed approach. In particular, notice the use of a private entry family.

[API-based non-blocking stack.]{} Here we present how a non-blocking stack can be implemented via the API proposed in Sec. \[API\_sec\].

[^1]: In global time!

[^2]: For the case that the compiler cannot figure out which statements are data-dependent, we propose an additional Boolean aspect [only\_execute\_on\_first\_try]{} to tag non-data-dependent statements.

[^3]: An example for employing function [Read\_Modify\_Write]{} is given in the Appendix in Listing \[lfsapi\]. It shows an implementation of a lock free stack using generic function [Read\_Modify\_Write]{} of package [Memory\_Model]{}.
