SPARK 2014 Rationale: Support for Ravenscar

by Yannick Moy in Language, Formal Verification – November 23, 2015

As presented in a recent post, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in the Ravenscar profile of Ada. This profile restricts concurrency so that concurrent programs are deterministic and schedulable. SPARK analysis makes it possible to prove that shared data is protected against data races, that deadlocks cannot occur and that no other run-time errors related to concurrency can be encountered when running the program. Avoiding deadlocks in Ravenscar can be seen as a special form of run-time error to avoid, as the Ceiling Priority protocol in Ravenscar defines precisely which tasks are allowed to access which shared data and makes it a run-time error to perform an access which could create a deadlock. The main restriction to respect to fit in Ravenscar profile is that all concurrent objects (tasks and protected objects) should be defined statically at the top-level (that is, not created dynamically inside subprograms). I'll reuse the example presented by Pavlos to illustrate the main features of this support for concurrency in SPARK.

The preferred way to communicate between tasks in Ravenscar is through protected objects, as task rendez-vous (using task entries) are forbidden in Ravenscar (because they make schedulability analysis too difficult). A protected object declares public operations: functions which cannot modify the state of the protected object, procedures which can modify the state of the protected object and entries which are like procedures with a guard to stop the task from entering the protected object until some condition is true. For more details, see the SPARK User's Guide.

Functionally, a protected object maintains an invariant over the data it protects. As a refinement over the code presented by Pavlos, I'm going here to express the invariant that traffic lights maintain as a type predicate:

   --  The following type represents the actual lights of the traffic
   --  light. There are three lights for vehicles and two for pedestrians.
   --  When a component is True the corresponding light is On. When a
   --  component is False the corresponding light is Off.
   type Lights_State is record
      Vehicles_Green    : Boolean := False;
      Vehicles_Yellow   : Boolean := False;
      Vehicles_Red      : Boolean := True;
      Pedestrians_Green : Boolean := True;
      Pedestrians_Red   : Boolean := False;
   end record;

   function Valid_Combination (LS : Lights_State) return Boolean;

   subtype Valid_Lights_State is Lights_State
     with Predicate => Valid_Combination (Valid_Lights_State);

The protected object Traffic_Light is now mostly encapsulating a value of this record type plus a few other components:

   protected Traffic_Light is
      entry Change_Lights;
      procedure Check_Time;

   private
      --  The following holds the time when the last state change occurred.
      Last_State_Change : Time    := Time_First;

      --  The following is a boolean flag that indicates whether or not the
      --  time has arrived to change the state of the traffic light.
      Change_State      : Boolean := False;

      --  The following variable represents the actual lights of the traffic
      --  light. There are three lights for vehicles and two for pedestrians.
      Lights            : Valid_Lights_State;
   end Traffic_Light;

Tasks call the protected subprograms to communicate. So task Change_The_Time calls Check_Time to update the inner state of the protected object so that the next activation of task Change_The_Lights updates the lights by calling Change_Lights which follows the inner automaton of Traffic_Lights. Because the two tasks only communicate through protected object Traffic_Light, there is no possible data race here, and no possible deadlock either, as correctly analyzed by GNATprove. The respect of the Ceiling Priority protocol is guaranteed here because the (default) priority of tasks Change_The_Time and Change_The_Lights is indeed lower than the (default) priority of protected object Traffic_Light. But this could be false if priorities were specified here explicitly, and in such a case GNATprove would detect it. For more details, see the SPARK User's Guide.

Like in the original code, an assumption is still required at the start of entry Change_Lights, for a different reason though. In the original code, the assumption was needed as a replacement for calling protected function Valid_Combination in the precondition. Indeed, as the precondition is logically outside the protected subprogram, getting the assurance that Valid_Combination holds in the precondition is not a protection against it not holding anymore when the protected subprogram is entered. Thus, Ada forbids such calls in preconditions. In our code, the invariant that Valid_Combination expresses is stated on the type of the component Lights of protected object Traffic_Light, so no precondition is needed. The assumption is only needed because GNATprove is not currently smart enough to assume the invariant properties of components of protected objects on entry of protected subprograms.

There is more in the support of concurrency in SPARK, in relation with suspension objects (lightweight form of protected objects, as if the data was a single boolean), task contracts and state abstraction. See the details in SPARK User's Guide.

Finally, here is the complete program:

--  For the sake of this example the lights go as follows:
--
--  Vehicles                 Pedestrians
--
--  Green                    Red
--  Yellow                   Red
--  Red                      Green
--  Red and Yellow           Red
--
--  and over and over they go..

with Ada.Real_Time; use Ada.Real_Time;

package Traffic_Lights is

   --  The following type represents the actual lights of the traffic
   --  light. There are three lights for vehicles and two for pedestrians.
   --  When a component is True the corresponding light is On. When a
   --  component is False the corresponding light is Off.
   type Lights_State is record
      Vehicles_Green    : Boolean := False;
      Vehicles_Yellow   : Boolean := False;
      Vehicles_Red      : Boolean := True;
      Pedestrians_Green : Boolean := True;
      Pedestrians_Red   : Boolean := False;
   end record;

   function Valid_Combination (LS : Lights_State) return Boolean;

   subtype Valid_Lights_State is Lights_State
     with Predicate => Valid_Combination (Valid_Lights_State);

   protected Traffic_Light is
      entry Change_Lights;
      procedure Check_Time;

   private
      --  The following holds the time when the last state change occurred.
      Last_State_Change : Time    := Time_First;

      --  The following is a boolean flag that indicates whether or not the
      --  time has arrived to change the state of the traffic light.
      Change_State      : Boolean := False;

      --  The following variable represents the actual lights of the traffic
      --  light. There are three lights for vehicles and two for pedestrians.
      Lights            : Valid_Lights_State;
   end Traffic_Light;

   task Check_The_Time;
   --  This task determines when it's time to change the traffic light.

   task Change_The_Lights;
   --  This task is periodically notified to change the traffic light.

end Traffic_Lights;

package body Traffic_Lights is
   function Valid_Combination (LS : Lights_State) return Boolean is
      (if LS.Vehicles_Green then
        not LS.Vehicles_Yellow
        and not LS.Vehicles_Red
        and not LS.Pedestrians_Green
        and LS.Pedestrians_Red

      elsif LS.Pedestrians_Green then
        not LS.Vehicles_Green
        and not LS.Vehicles_Yellow
        and LS.Vehicles_Red
        and not LS.Pedestrians_Red

      else
        not LS.Pedestrians_Green
        and LS.Pedestrians_Red);

   protected body Traffic_Light is

      entry Change_Lights when Change_State is
         LS : Lights_State := Lights;
      begin
         pragma Assume (Valid_Combination (Lights));
         if LS.Vehicles_Green then
            LS.Vehicles_Green  := False;
            LS.Vehicles_Yellow := True;

         elsif LS.Vehicles_Yellow and not LS.Vehicles_Red then
            LS.Vehicles_Yellow   := False;
            LS.Vehicles_Red      := True;
            LS.Pedestrians_Green := True;
            LS.Pedestrians_Red   := False;

         elsif LS.Vehicles_Red and not LS.Vehicles_Yellow then
            LS.Vehicles_Yellow   := True;
            LS.Pedestrians_Green := False;
            LS.Pedestrians_Red   := True;

         elsif LS.Vehicles_Red and LS.Vehicles_Yellow then
            LS.Vehicles_Green  := True;
            LS.Vehicles_Yellow := False;
            LS.Vehicles_Red    := False;
         end if;

         Lights := LS;
         Change_State := False;
         Last_State_Change := Clock;
      end Change_Lights;

      procedure Check_Time is
         Wait_Duration : constant Time_Span :=
           (if Lights.Vehicles_Yellow then
               --  States that involve a yellow vehicle light only last 2
               --  seconds.
               Seconds (2)
            else
               --  All other states last 15 seconds.
               Seconds (15));
      begin
         if Clock - Last_State_Change >= Wait_Duration then
            --  We have waited enough. It is time for a state change...
            Change_State := True;
         end if;
      end Check_Time;
   end Traffic_Light;

   task body Check_The_Time is
   begin
      loop
         Traffic_Light.Check_Time;
      end loop;
   end Check_The_Time;

   task body Change_The_Lights is
   begin
      loop
         Traffic_Light.Change_Lights;
      end loop;
   end Change_The_Lights;
end Traffic_Lights;
comments powered by Disqus