Verifying Tasking in Extended, Relaxed Style
by Piotr Trojanek –
Tasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs allowed by the Ravenscar profile. Now it also supports the more relaxed GNAT Extended Ravenscar profile. The GNAT Reference Manual already documents how the new profile is different from the old one and why you might like it. Here we explain how this new profile might affect your SPARK code.
First, in the GNAT Extended Ravenscar you are no longer restricted to one entry per protected type. In particular, you can now directly implement message stores with multiple consumers: each consumer can wait for a specific kind of messages by blocking on its own entry.
Expressions in entry barriers are no longer restricted to simple Boolean variables. Now they might involve simple protected variables, literals, and predefined relational and logical operators (e.g. "<", "/=", "and"). This is more relaxed, but the new restrictions still guarantee that the evaluation of a barrier expression will raise no runtime errors and will not have side effects. (That's why they are called "pure.") Tip: if strict Ravenscar forced you to have a barrier variable "Non_Empty" then now you can rename it to a more natural "Empty" and write the barrier expression as "not Empty."
Relative delay statements like "delay 1.0" are now allowed. They are much less cumbersome than the strict Ravenscar pattern:
declare
Now : constant Ada.Real_Time.Time := Ada.Real_Time.Clock;
begin
delay until Now + Seconds (1);
end;Finally, you are free to use Ada.Calendar package now, which (as suggested in the GNAT Reference Manual) might be handy for log messages. The relaxed profile also allows "delay until" statements where the expression is of the type Ada.Calendar.Time, not Ada.Real_Time.Time. But here is a detail: both Ada.Calendar and Ada.Real_Time have their own abstract states called Clock_Time. It is because Ada RM says that bases for Ada.Calendar and Ada.Real_Time are not necessarily the same (and SPARK conservatively assumes they are not). Of course, you may ask GNATprove to confirm that you are using the right clock: just put the expected Clock_Time state in your Global contract.
For details on how to enable the new profile and for general introduction to concurrency in SPARK please visit the User's Guide.