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¶

../../../_images/concurrent_program_struct_ada.png

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¶

../../../_images/concurrent_program_struct_ravenscar.png

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¶

package Show_Trivial_Task is type Task_Id is new Integer; task type T (Id : Task_Id); T1 : T (0); T2 : T (1); end Show_Trivial_Task;

package body Show_Trivial_Task is task body T is Current_Task : Task_Id := Id; begin loop delay 1.0; end loop; end T; end Show_Trivial_Task;

Id can be written by T1 and T2 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

package Show_Protected_Object is protected P is procedure Set (V : Natural); function Get return Natural; private The_Data : Natural := 0; end P; end Show_Protected_Object;

package body Show_Protected_Object is protected body P is procedure Set (V : Natural) is begin The_Data := V; end Set; function Get return Natural is (The_Data); end P; end Show_Protected_Object;

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.

package Show_Protected_Object_Ravenscar is protected type PT is procedure Set (V : Natural); function Get return Natural; private The_Data : Natural := 0; end PT; P : PT; type PAT is array (1 .. 3) of PT; PA : PAT; type PRT is record A, B : PT; end record with Volatile; PR : PRT; end Show_Protected_Object_Ravenscar;

package body Show_Protected_Object_Ravenscar is protected body PT is procedure Set (V : Natural) is begin The_Data := V; end Set; function Get return Natural is (The_Data); end PT; end Show_Protected_Object_Ravenscar;

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 condition
- second 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

package Show_Blocking_Communication is protected type PT is entry Reset; private Is_Not_Null : Boolean := False; The_Data : Integer := 1000; end PT; end Show_Blocking_Communication;

package body Show_Blocking_Communication is protected body PT is entry Reset when Is_Not_Null is begin The_Data := 0; end Reset; end PT; end Show_Blocking_Communication;

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

package Show_Relaxed_Constraints_On_Entries is protected type Mailbox is entry Publish; entry Retrieve; private Num_Messages : Natural := 0; end Mailbox; end Show_Relaxed_Constraints_On_Entries;

package body Show_Relaxed_Constraints_On_Entries is Max : constant := 100; protected body Mailbox is entry Publish when Num_Messages < Max is begin Num_Messages := Num_Messages + 1; end Publish; entry Retrieve when Num_Messages > 0 is begin Num_Messages := Num_Messages - 1; end Retrieve; end Mailbox; end Show_Relaxed_Constraints_On_Entries;

Interrupt Handlers in Ravenscar¶

Interrupt handlers are parameterless procedures of PO
- with aspect Attach_Handler specifying the corresponding signal
- with aspect Interrupt_Priority on the PO specifying the priority

with System; use System; with Ada.Interrupts.Names; use Ada.Interrupts.Names; package Show_Interrupt_Handlers is protected P with Interrupt_Priority => System.Interrupt_Priority'First is procedure Signal with Attach_Handler => SIGHUP; end P; end Show_Interrupt_Handlers;

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 or Interrupt_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

package Show_Data_And_Flow_Dependencies is X, Y, Z : Integer; task T with Global => (Input => X, Output => Y, In_Out => Z), Depends => (T => T, Z => X, Y => X, null => Z); end Show_Data_And_Flow_Dependencies;

State Abstraction over Synchronized Variables¶

Synchronized objects can be abstracted in synchronized abstract state with aspect Synchronous

package Show_State_Abstraction with Abstract_State => (State with Synchronous, External) is protected type Protected_Type is procedure Reset; private Data : Natural := 0; end Protected_Type; task type Task_Type; end Show_State_Abstraction;

package body Show_State_Abstraction with Refined_State => (State => (A, P, T)) is A : Integer with Atomic, Async_Readers, Async_Writers; P : Protected_Type; T : Task_Type; protected body Protected_Type is procedure Reset is begin Data := 0; end Reset; end Protected_Type; task body Task_Type is begin P.Reset; A := 0; end Task_Type; end Show_State_Abstraction;

Synchronized state is a form of external state
- Synchronous same as External => (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 and Clock_Time

Code Examples / Pitfalls¶

Example #1¶

procedure Rendezvous is task T1 is entry Start; end T1; task body T1 is begin accept Start; end T1; begin T1.Start; end Rendezvous;

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¶

package Example_02 is protected P is entry Reset; end P; private Data : Boolean := False; end Example_02;

package body Example_02 is protected body P is entry Reset when Data is begin null; end Reset; end P; end Example_02;

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¶

package Example_03 is protected P is procedure Set (Value : Integer); end P; private task type TT; T1, T2 : TT; end Example_03;

package body Example_03 is Data : Integer := 0; protected body P is procedure Set (Value : Integer) is begin Data := Value; end Set; end P; task body TT is Local : Integer := 0; begin loop Local := (Local + 1) mod 100; P.Set (Local); end loop; end TT; end Example_03;

This code is not correct. Global unprotected data accessed in protected object shared between tasks

Example #4¶

package Example_04 is protected P is procedure Set (Value : Integer); end P; private Data : Integer := 0 with Part_Of => P; task type TT; T1, T2 : TT; end Example_04;

package body Example_04 is protected body P is procedure Set (Value : Integer) is begin Data := Value; end Set; end P; task body TT is Local : Integer := 0; begin loop Local := (Local + 1) mod 100; P.Set (Local); end loop; end TT; end Example_04;

This code is correct. Data is part of the protected object state. The only accesses to Data are through P.

Example #5¶

package Example_05 is protected P1 with Priority => 3 is procedure Set (Value : Integer); private Data : Integer := 0; end P1; protected P2 with Priority => 2 is procedure Set (Value : Integer); end P2; private task type TT with Priority => 1; T1, T2 : TT; end Example_05;

package body Example_05 is protected body P1 is procedure Set (Value : Integer) is begin Data := Value; end Set; end P1; protected body P2 is procedure Set (Value : Integer) is begin P1.Set (Value); end Set; end P2; task body TT is Local : constant Integer := 0; begin loop P2.Set (Local); end loop; end TT; end Example_05;

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¶

package Example_06 is protected type Mailbox is entry Publish; entry Retrieve; private Not_Empty : Boolean := True; Not_Full : Boolean := False; Num_Messages : Natural := 0; end Mailbox; end Example_06;

package body Example_06 is Max : constant := 100; protected body Mailbox is entry Publish when Not_Full is begin Num_Messages := Num_Messages + 1; Not_Empty := True; if Num_Messages = Max then Not_Full := False; end if; end Publish; entry Retrieve when Not_Empty is begin Num_Messages := Num_Messages - 1; Not_Full := True; if Num_Messages = 0 then Not_Empty := False; end if; end Retrieve; end Mailbox; end Example_06;

This code is not correct. Integer range cannot be proved correct.

Example #7¶

package Example_07 is protected type Mailbox is entry Publish; entry Retrieve; private Num_Messages : Natural := 0; end Mailbox; end Example_07;

package body Example_07 is Max : constant := 100; protected body Mailbox is entry Publish when Num_Messages < Max is begin Num_Messages := Num_Messages + 1; end Publish; entry Retrieve when Num_Messages > 0 is begin Num_Messages := Num_Messages - 1; end Retrieve; end Mailbox; end Example_07;

This code is correct. Precise range obtained from entry guards allows to prove checks.

Example #8¶

package Example_08 is Max : constant := 100; type Content is record Not_Empty : Boolean := False; Not_Full : Boolean := True; Num_Messages : Natural := 0; end record with Predicate => Num_Messages in 0 .. Max and Not_Empty = (Num_Messages > 0) and Not_Full = (Num_Messages < Max); protected type Mailbox is entry Publish; entry Retrieve; private C : Content; end Mailbox; end Example_08;

package body Example_08 is protected body Mailbox is entry Publish when C.Not_Full is Not_Full : Boolean := C.Not_Full; Num_Messages : Natural := C.Num_Messages; begin Num_Messages := Num_Messages + 1; if Num_Messages = Max then Not_Full := False; end if; C := (True, Not_Full, Num_Messages); end Publish; entry Retrieve when C.Not_Empty is Not_Empty : Boolean := C.Not_Empty; Num_Messages : Natural := C.Num_Messages; begin Num_Messages := Num_Messages - 1; if Num_Messages = 0 then Not_Empty := False; end if; C := (Not_Empty, True, Num_Messages); end Retrieve; end Mailbox; end Example_08;

This code is correct. Precise range obtained from predicate allows to prove checks. Predicate is preserved.

Example #9¶

--% src_file: Example_09.ads --% cflags: -gnaty --% make_flags: -gnaty -gnata package Example_09 is package Service with Abstract_State => (State with External) is procedure Extract (Data : out Integer) with Global => (In_Out => State); end Service; private task type T; T1, T2 : T; end Example_09;

package body Example_09 is package body Service with Refined_State => (State => Extracted) is Local_Data : constant Integer := 100; Extracted : Boolean := False; procedure Extract (Data : out Integer) is begin if not Extracted then Data := Local_Data; Extracted := True; else Data := Integer'First; end if; end Extract; end Service; task body T is X : Integer; begin loop Service.Extract (X); end loop; end T; end Example_09;

This code is not correct. Unsynchronized state cannot be accessed from multiple tasks or protected objects.

Example #10¶

package Example_10 is package Service with Abstract_State => (State with Synchronous, External) is procedure Extract (Data : out Integer) with Global => (In_Out => State); private protected type Service_Extracted is procedure Set; function Get return Boolean; private Extracted : Boolean := False; end Service_Extracted; end Service; private task type T; T1, T2 : T; end Example_10;

package body Example_10 is package body Service with Refined_State => (State => Extracted) is Local_Data : constant Integer := 100; Extracted : Service_Extracted; protected body Service_Extracted is procedure Set is begin Extracted := True; end Set; function Get return Boolean is (Extracted); end Service_Extracted; procedure Extract (Data : out Integer) is Is_Extracted : constant Boolean := Extracted.Get; begin if not Is_Extracted then Data := Local_Data; Extracted.Set; else Data := Integer'First; end if; end Extract; end Service; task body T is X : Integer; begin loop Service.Extract (X); end loop; end T; end Example_10;

This code is correct. Abstract state is synchronized, hence can be accessed from multiple tasks and protected objects.