SPARK 2014 Rationale: Support for Ravenscar
by Yannick Moy –
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;About Yannick Moy
Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.