Verifying Tasking in Extended, Relaxed Style

by Piotr Trojanek – Nov 07, 2016

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
end;