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.