Concurrency
Concurrency ≠ Parallelism
Concurrency allows to create a well structured program
Parallelism allows to create a high performance program
Multiple cores/processors are...
possible for concurrent programs
essential to parallelism
What about Ada and SPARK?
GNAT runtimes for concurrency available on single core & multicore (for SMP platforms)
parallel features scheduled for inclusion in Ada and SPARK 202x
Concurrent Program Structure in Ada

The problems with concurrency
Control and data flow become much more complex
possibly nondeterministic even
actual behavior is one of many possible interleavings of tasks
Data may be corrupted by concurrent accesses
so called data races or race conditions
Control may block indefinitely, or loop indefinitely
so called deadlocks and livelocks
Scheduling and memory usage are harder to compute
Ravenscar – the Ada solution to concurrency problems
Ravenscar profile restricts concurrency in Ada
ensures deterministic behavior at every point in time
recommends use of protected objects to avoid data races
prevents deadlocks with Priority Ceiling Protocol
allows use of scheduling analysis techniques (RMA, RTA)
facilitates computation of memory usage with static tasks
GNAT Extended Ravenscar profile lifts some restrictions
still same benefits as Ravenscar profile
removes painful restrictions for some applications
Concurrent Program Structure in Ravenscar

Ravenscar – the SPARK solution to concurrency problems
Ravenscar and Extended_Ravenscar profiles supported in SPARK
Data races prevented by flow analysis
ensures no problematic concurrent access to unprotected data
flow analysis also ensures non-termination of tasks
Run-time errors prevented by proof
includes violations of the Priority Ceiling Protocol
Concurrency – A trivial example
Id can be written by
T1
andT2
at the same time
Setup for using concurrency in SPARK
Any unit using concurrency features (tasks, protected objects, etc.) must set the profile
pragma Profile (Ravenscar);
-- or
pragma Profile (GNAT_Extended_Ravenscar);
... plus an additional pragma
that ensures tasks start after the end of elaboration
pragma Partition_Elaboration_Policy (Sequential);
... which are checked by GNAT partition-wide
pragmas needed for verification even it not for compilation
Tasks in Ravenscar
A task can be either a singleton object or a type
no declarations of entries for rendez-vous
task T;
task type TT;
... completed by a body
infinite loop to prevent termination
task body T is
begin
loop
...
end loop;
end T;
Tasks are declared at library-level
... as standalone objects or inside records/arrays
type TA is array (1 .. 3) of TT;
type TR is record
A, B : TT;
end record;
Communication Between Tasks in Ravenscar
Tasks can communicate through protected objects
A protected object is either a singleton object or a type
all PO private data initialized by default in SPARK
Protected Objects in Ravenscar
Protected objects are declared at library-level
... as standalone objects or inside records/arrays
The record type needs to be volatile, as a non-volatile type cannot contain a volatile component. The array type is implicitly volatile when its component type is volatile.
Protected Communication with Procedures & Functions
CREW enforced (Concurrent-Read-Exclusive-Write)
procedures have exclusive read-write access to PO
functions have shared read-only access to PO
Actual mechanism depends on target platform
scheduler enforces policy on single core
locks used on multicore (using CAS instructions)
lock-free transactions used for simple PO (again using CAS)
Mechanism is transparent to user
user code simply calls procedures/functions
task may be queued until PO is released by another task
Blocking Communication with Entries
Only protected objects have entries in Ravenscar
Entry = procedure with
entry
guard conditionsecond level of queues, one for each entry, on a given PO
task may be queued until guard is True and PO is released
at most one entry in Ravenscar
guard is a
Boolean
component of PO in Ravenscar
Relaxed Constraints on Entries with Extended Ravenscar
Proof limitations with Ravenscar
not possible to relate guard to other components with invariant
GNAT Extended Ravenscar profile lifts these constraints
and allows multiple tasks to call the same entry
Interrupt Handlers in Ravenscar
Interrupt handlers are parameterless procedures of PO
with aspect
Attach_Handler
specifying the corresponding signalwith aspect
Interrupt_Priority
on the PO specifying the priority
Priority of the PO should be in
System.Interrupt_Priority
default is OK – in the range of
System.Interrupt_Priority
checked by proof (default or value of
Priority
orInterrupt_Priority
)
Other Communications Between Tasks in SPARK
Tasks must communicate through synchronized objects
atomic objects
protected objects
suspension objects (standard
Boolean
protected objects)
Constants are considered as synchronized
this includes variables constant after elaboration (specified with aspect
Constant_After_Elaboration
)
Single task or PO can access an unsynchronized object
exclusive relation between object and task/PO must be specified with aspect
Part_Of
Data and Flow Dependencies of Tasks
Input/output relation can be specified for a task
as task never terminates, output is understood while task runs
task itself is both an input and an output
implicit
In_Out => T
explicit dependency
State Abstraction over Synchronized Variables
Synchronized objects can be abstracted in synchronized abstract state with aspect
Synchronous
Synchronized state is a form of external state
Synchronous
same asExternal => (Async_Readers, Async_Writers)
tasks are not volatile and can be part of regular abstract state
Synchronized Abstract State in the Standard Library
Standard library maintains synchronized state
the tasking runtime maintains state about running tasks
the real-time runtime maintains state about current time
package Ada.Task_Identification with
SPARK_Mode,
Abstract_State =>
(Tasking_State with Synchronous,
External => (Async_Readers, Async_Writers)),
Initializes => Tasking_State
package Ada.Real_Time with
SPARK_Mode,
Abstract_State =>
(Clock_Time with Synchronous,
External => (Async_Readers, Async_Writers)),
Initializes => Clock_Time
API of these units refer to
Tasking_State
andClock_Time
Code Examples / Pitfalls
Example #1
This code is not correct. Task rendezvous is not allowed; violation of
restriction Max_Task_Entries = 0
. A local task is not allowed;
violation of restriction No_Task_Hierarchy
Example #2
This code is not correct. Global data in entry guard is not allowed.
Violation of restriction Simple_Barriers
(for Ravenscar) or
Pure_Barriers
(for Extended Ravenscar)
Example #3
This code is not correct. Global unprotected data accessed in protected object shared between tasks
Example #4
This code is correct. Data
is part of the protected object state. The
only accesses to Data
are through P
.
Example #5
This code is correct. Ceiling_Priority
policy is respected. Task
never accesses a protected object with lower priority than its active
priority. Note that PO can call procedure or function from another PO, but
not an entry (possibly blocking).
Example #6
This code is not correct. Integer range cannot be proved correct.
Example #7
This code is correct. Precise range obtained from entry guards allows to prove checks.
Example #8
This code is correct. Precise range obtained from predicate allows to prove checks. Predicate is preserved.
Example #9
This code is not correct. Unsynchronized state cannot be accessed from multiple tasks or protected objects.
Example #10
This code is correct. Abstract state is synchronized, hence can be accessed from multiple tasks and protected objects.