Safe Non-blocking Synchronization in Ada 202x
Johann Blieberger1 and Bernd Burgstaller2

arXiv:1803.10067v1 [cs.PL] 27 Mar 2018

1

Institute of Computer Engineering, Automation Systems Group, TU Wien, Austria
2
Department of Computer Science, Yonsei University, Korea

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-modifywrite 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 nonblocking synchronization construct as a first-class citizen of a high-level
programming language. We illustrate the use of concurrent objects by
several examples.

1

Introduction

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 [12]. 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 [11].) 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) [11].

2

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 mutualexclusion property of (highly-contended) locks stands in the way to scalability of
parallel programs on many-core architectures [15]. 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 [11].
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 [2].
To motivate the need for a strict memory model, consider the producerconsumer synchronization example in Fig. 1(a) (adopted from [17] and [5]). 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 6 of Task 2. (E.g., a store–store re-ordering of the assignments in
lines 2 and 3 of Task 1 will allow this result.) In Ada 2012, such re-orderings

1
2
3

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

1
2
3

2

-- Task 1:
Data := 1;
Flag := True ;

3
4
5
6

(a)

-- Task 2:
loop
R1 := Flag ;
exit when R1 ;
end loop ;
R2 := Data ;

1
2

Data : Integer w i t h Volatile ;
Flag : Boolean w i t h Atomic ;

(b)

Fig. 1: (a) Producer-consumer synchronization in pseudo-code: Task 1 writes the
Data variable and then signals Task 2 by setting the Flag variable. Task 2 is
spinning on the Flag variable (lines 2 to 5) and then reads the Data variable.
(b) Labeling to enforce sequential consistency in Ada 2012.

3

can be ruled out by labeling variables Data and Flag by aspect volatile. The
corresponding variable declarations are depicted in Fig. 1(b). (Note that by [8,
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 [8, C.6§16/3]. Updates of volatile
variables are thus required to be sequentially consistent, in the sense of Lamport’s
definition [13]: “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. Nonatomic 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. 1(b)
and [16] 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. 1, performance can be improved by
allowing a less strict memory order for variable Data (to be addressed in
Section 2).
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 [3,9,17].
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 [14]. It was later found to be
unsound with standard compiler optimizations [18]. The C++11 standard (cf.
[1,19]) 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 [10,
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-andswap, and instructions that provide high-level operations, such as translate-andtest 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 threadfunctionality provided through libraries [6].

4

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 stateof-the-art on memory models and introduce synchronized variables in Sec. 2. We
introduce attributes for specifying memory ordering operations in Sec. 3. We
specify concurrent objects in Sec. 4 and discuss task scheduling in the presence
of COs in Sec. 5. Sec. 6 contains two CO example implementations with varying
memory consistency semantics. We discuss our low-level API in Sec. 7. Sec. 8
contains our conclusions.
Due to space constraints, we have issued a technical report which contains additional programming examples and the rationale for the design of the proposed
non-blocking synchronization mechanisms. Although the paper is intended to
be comprehensive without the appendices, we felt the additional material might
nevertheless be useful. For the same reason of constrained space, the description
of our approach cannot be compared to the specification of Ada on RML-level.

2

The Memory Model

For reasons outlined in Sec. 1, 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
2

“Core” refers to the software’s view of a core, which may be an actual core or a
thread context of a multithreaded core [17].

5

distinguish between memory consistency and coherence. We cite from [17]: ‘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 [2]. 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 [3,9,17]. 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) [4]. 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 [2] 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 [8, 9.10§11].) The SC-for-DRF programming model
and two relaxations were formalized for C++11 [7]. They were later adopted for
C11, OpenCL 2.0, and for X10 [21] (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. 3.1).
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.

6

Beyond those, atomicity can only be ensured by locks. Nevertheless, computer
architectures provide memory fences (see e.g., [11]) 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 1.2 provides an example.)
In addition to synchronized variables, synchronized types and attribute
Synchronized Components 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., [11]). 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.
2.1

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 synchronizeswith relation becomes important. If operation X in one thread synchronizes-with
operation Y in another thread, then X happens-before Y. Note that the happensbefore 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.

7

We define different memory models. These memory models originated from
the DRF [4] and properly-labeled [9] hardware memory models. They were formalized for the memory model of C++ [7]. 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 1, 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.3 A thread issuing a read-acquire later
may read a different value than that written by the first thread.

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 1.
3
4
5

In global time!
Memory accesses other than accesses to synchronized variables
Before optimizations performed by the compiler and before reordering done by the
CPU.

8
memory order involved
threads
relaxed
1
release/acquire
2

sequentially
consistent

all

constraints for reordering memory accesses
(for compilers and CPUs)
no inter-thread constraints
(1) ordinary4 stores originally5 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)
(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)

Table 1: Memory Order and Constraints for Compilers and CPUs

3
3.1

Synchronization primitives
Synchronized Variables

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
X’Concurrent Write(Memory Order => Release) :=
Y’Concurrent Read(Memory Order => relaxed);
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

9

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
X: integer with Synchronized, Memory Order Write => Release;
Y: integer with Synchronized, Memory Order Read => Acquire;
...
X := Y;
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.
3.2

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,
Release, 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 =>
Acquire or Memory Order Failure => 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
Sequentially Consistent.
Again, aspects for variable specific default values for the attributes described
above may be specified when declaring a read-modify-write variable. The aspects
Memory Order Write Success,
and
are
Memory Order Read,
Memory Order Write Failure with allowed values as above.
3.3

Synchronization Loops

As presented below synchronization by synchronized variables is performed via
spin loops. We call these loops sync loops.

10

4

Concurrent Objects

4.1

Non-Blocking Synchronization

Besides the aspects and attributes proposed in Section 3 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.
4.2

Read-Modify-Write Synchronization

For concurrent objects with read-modify-write variables the attributes proposed
in Section 3 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 1.1.
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.6 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.

5

Scheduling and Dispatching

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
6

For the case that the compiler cannot figure out which statements are datadependent, we propose an additional Boolean aspect only execute on first try
to tag non-data-dependent statements.

11

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

6

Examples

Non-blocking Stack. Listing 1.1 shows an implementation of a non-blocking
stack using our proposed new syntax for concurrent objects.
1

s u b t y p e Data i s Integer ;

2
3
4
5
6
7
8
9

t y p e List ;
t y p e List_P i s a c c e s s List ;
t y p e List i s
record
D : Data ;
Next : List_P ;
end r e c o r d ;

10
11

Empty : e x c e p t i o n ;

12
13
14
15
16
17
18
19
20
21
22

c o n c u r r e n t Lock_Free_Stack
is
e n t r y Push ( D : Data ) ;
e n t r y Pop ( D : o u t Data ) ;
private
Head : List_P w i t h R ea d M o d i f y W r i te ,
Memory Order Read = > R el a x ed ,
Memory Order Write Success => R elea s e ,
Memory Order Write Failure => Relaxed;
end L o c k _ F r e e _ S t a c k;

23
24
25
26
27
28
29
30
31

c o n c u r r e n t body L o c k _ F r e e _ S t a c k i s
e n t r y Push ( D : Data )
u n t i l Head = Head ’ OLD i s
New_Node : List_P := new List ;
begin
New_Node . a l l := ( D = > D , Next = > Head ) ;
Head := New_Node ;
end Push ;

32
33
34
35
36
37
38
39
40
41
42
43
44

e n t r y Pop ( D : o u t Data )
u n t i l Head = Head ’ OLD i s
Old_Head : List_P ;
begin
Old_Head := Head ;
i f Old_Head /= n u l l t h e n
Head := Old_Head . Next ;
D := Old_head . D ;
else
r a i s e Empty ;
end i f ;
end Pop ;

12
45

end L o c k _ F r e e _ S t a c k;

Listing 1.1: Non-blocking Stack Implementation Using Proposed New Syntax
Implementation of entry Push (lines 25–31) behaves as follows. In Line 29 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 30) assigns the new value to
the head of the list. Since variable Head has aspect Read Modify Write (line 18),
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 31, 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 29. Line 27 is not re-executed as it is not data
dependent on Head.
Several memory order attributes apply to the RMW operation (Line 30)
which are given in lines 19–21: 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 27.
Implementation of entry Pop (lines 33–44) 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
sequentially consistent.
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 1.2 shows how release-acquire semantics can be implemented for general data structures with help of one synchronized Boolean.
1
2
3
4

generic
t y p e Data i s p r i v a t e ;
package Generic_Release_Acquire i s

13
5
6
7
8
9
10
11
12
13
14

c o n c u r r e n t RA
is
p r o c e d u r e Write ( d : Data ) ;
e n t r y Get ( D : o u t Data ) ;
private
Ready : Boolean := false w i t h S y n c h r o n i z e d ,
Memory Order Read = > Acq u i r e ,
Memory Order Write = > R e l e a s e ;
Da : Data ;
end RA ;

15
16

end G e n e r i c _ R e l e a s e _ A c q u i r e;

17
18

p a c k a g e body G e n e r i c _ R e l e a s e _ A c q u i r e i s

19
20

c o n c u r r e n t body RA i s

21
22
23
24
25
26

p r o c e d u r e Write ( D : Data ) i s
begin
Da := D ;
Ready := true ;
end Write :

27
28
29
30
31
32
33
34
35

e n t r y Get ( D : o u t Data )
when Ready i s
-- spin - lock until released , i . e . , Ready = true ;
-- only sync . v a r i a b l e s and c o n s t a n t s allowed in guard e x p r e s s i o n
begin
D := Da ;
end Get ;
end RA ;

36
37

end G e n e r i c _ R e l e a s e _ A c q u i r e;

Listing 1.2: Generic Release-Acquire Object

7

API

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 1.3 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.
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 5). 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.
1

package Memory_Model i s

2
3
4
5
6
7
8

type Memory_Order_Type i s (
Sequentially Consistent ,
R el a x ed ,
Acq u i r e ,
R e l e a s e );

14
9

s u b t y p e M e m o r y _ O r d e r _ S u c c e s s _ T y p e i s M e m o r y _ O r d e r _ T y p e;

10
11
12

subtype Memory_Order_Failure_Type i s Memory_Order_Type
r a n g e S e q u e n t i a l l y C o n s i s t e n t .. A c q u i r e ;

13
14
15
16
17
18
19
20
21
22
23

generic
type Some_Synchronized_Type i s p r i v a t e ;
w i t h f u n c t i o n Update r e t u r n S o m e _ S y n c h r o n i z e d _ T y p e;
R e a d _ M o d i f y _ W r i t e _ V a r i a b l e: i n o u t S o m e _ S y n c h r o n i z e d _ T y p e
with Read Modify Write ;
M emo r y Or d er S u cces s : M e m o r y _ O r d e r _ S u c c e s s _ T y p e :=
Sequentially Consistent ;
M e m o r y O r d e r F a i l u r e : M e m o r y _ O r d e r _ F a i l u r e _ T y p e :=
Sequentially Consistent ;
f u n c t i o n R e a d M o d i f y W r i t e r e t u r n Boolean ;

24
25

end M e m o r y _ M o d e l;

Listing 1.3: Package Memory Model

8

Conclusion and Future Work

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 ([8, 9.10§11]).
Although Ada 2012 provides the highly abstract protected object monitorconstruct 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 [20].
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 7).
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 [8, 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.

15

9

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.

References
1. Working Draft, Standard for Programming Language C++. ISO/IEC N4296, 2014.
2. S. V. Adve and H.-J. Boehm. Memory models: A case for rethinking parallel
languages and hardware. Commun. ACM, 53(8):90–101, Aug. 2010.
3. S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial.
Computer, 29(12):66–76, Dec. 1996.
4. S. V. Adve and M. D. Hill. Weak ordering—a new definition. In Proceedings of the
17th Annual International Symposium on Computer Architecture, ISCA ’90, pages
2–14, New York, NY, USA, 1990. ACM.
5. J. Barnes. Ada 2012 Rationale: The Language – the Standard Libraries. Springer
LNCS, 2013.
6. H.-J. Boehm. Threads cannot be implemented as a library. SIGPLAN Not.,
40(6):261–268, June 2005.
7. H.-J. Boehm and S. V. Adve. Foundations of the C++ concurrency memory model.
In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language
Design and Implementation, PLDI ’08, pages 68–78, New York, NY, USA, 2008.
ACM.
8. R. L. Brukardt, editor. Annotated Ada Reference Manual, ISO/IEC 8652:2012/Cor
1:2016. 2016.
9. K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta, and J. Hennessy.
Memory consistency and event ordering in scalable shared-memory multiprocessors. SIGARCH Comput. Archit. News, 18(2SI):15–26, May 1990.
10. L. Guerby. Ada 95 Rationale – The Language – The Standard Libraries. Springer,
1997.
11. M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2012.
12. C. A. R. Hoare. Monitors: An operating system structuring concept. Commun.
ACM, 17(10):549–557, Oct. 1974.
13. L. Lamport. How to make a multiprocessor computer that correctly executes
multiprocess programs. IEEE Trans. Comput., 28(9):690–691, Sept. 1979.
14. J. Manson, W. Pugh, and S. V. Adve. The Java memory model. In Proceedings
of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL ’05, pages 378–391, New York, NY, USA, 2005. ACM.
15. M. L. Scott. Shared-Memory Synchronization. Synthesis Lectures on Computer
Architecture. Morgan & Claypool Publishers, 2013.
16. H. Simpson. Four-slot fully asynchronous communication mechanism. Computers
and Digital Techniques, IEE Proceedings E, 137:17–30, 02 1990.
17. D. J. Sorin, M. D. Hill, and D. A. Wood. A Primer on Memory Consistency and
Cache Coherence. Number 16 in Synthesis Lectures on Computer Architecture.
Morgan & Claypool, 2011.

16
18. J. Ševčı́k and D. Aspinall. On validity of program transformations in the Java
memory model. In Proceedings of the 22nd European Conference on Object-Oriented
Programming, ECOOP ’08, pages 27–51, Berlin, Heidelberg, 2008. Springer-Verlag.
19. A. Williams. C++ Concurrency in Action. Manning Publ. Co., Shelter Island,
NY, 2012.
20. W. Xiong, S. Park, J. Zhang, Y. Zhou, and Z. Ma. Ad hoc synchronization considered harmful. In Proceedings of the 9th USENIX Conference on Operating Systems
Design and Implementation, OSDI’10, pages 163–176, Berkeley, CA, USA, 2010.
USENIX Association.
21. A. Zwinkau. A memory model for X10. In Proceedings of the 6th ACM SIGPLAN
Workshop on X10, X10 2016, pages 7–12, New York, NY, USA, 2016. ACM.

