An Introduction to Jorvik, the New Tasking Profile in Ada 2022
by Pat Rogers –
In 2016, AdaCore developed and deployed a new tasking profile based directly on the standard Ravenscar profile, but with some restrictions relaxed or replaced. We presented the new profile in 2017 at Ada Europe [1], providing the justification, additional capabilities, execution-time costs, and resulting schedulability analysis supported. That same year, AdaCore extended SPARK to include the new profile, thus supporting both tasking subsets.
The new profile is included in the Ada 2022 draft with some refinements and an official name: Jorvik (pronounced “Yourvick”). Jorvik was the Viking name for a Roman fort/settlement that eventually became known as York, in northern England. Said to be England's "Second City," some well-known cities around the world are named after it. The cover picture shows the city today, with the 13th-century Gothic cathedral and its Rose window in the background. York is not far from the village of Ravenscar, where that profile was introduced.
Similarly, Jorvik is not far, technically speaking, from Ravenscar. The differences can be summarized by the small handful of restrictions that are removed or replaced from the Ravenscar list. Everything else in Jorvik remains as it is in Ravenscar. Although the changes are few in number, they are nonetheless significant. We will explore the details below.
Before we do, you should understand that Jorvik is not a replacement for Ravenscar. The Ada community can benefit from both profiles. To understand why, let's start with a little background.
Ravenscar is intended for applications using tasking in four distinct application domains:
- safety-critical systems requiring stringent, exhaustive certification analyses,
- high-integrity applications requiring formal static analysis and verification,
- hard real-time applications requiring predictability and schedulability analysis,
- embedded applications requiring a small memory footprint, high performance, or both.
Note the changing requirements. They begin with very expensive, comprehensive and rigorous analyses, shift to less costly forms of analysis and non-functional properties (predictability), and end with only non-functional properties (space and speed).
Applications can be in more than one of these domains. A hard-real-time application might also be a high-integrity application, for example, and any of them might also be embedded. The requirements for such applications is then the union of all the applicable domains' requirements.
In response to that set of requirements, the Ravenscar profile restrictions remove complexity, both in the application source and in the run-time library (RTL), where Ada tasking is largely implemented. The results address the domains' requirements in three ways:
- A simplified RTL, and resultingly simpler application code, are less costly to analyze for certification and safety. A subset of any modern language is essential to make these analyses feasible, both technically and economically.
- At the application level, the tasking subset facilitates the various forms of analysis. The structure of the tasks, especially their possible control and data interactions, enables at the task level the sort of safety analysis previously applied to entire (sequential) programs. That same set of restricted interactions also simplifies schedulability analysis for the application code.
- A simplified RTL can be far more efficient in both object-code space and speed. For example, abort statements impose distributed costs, i.e., object code size and execution performance penalties whether or not they are actually used in an application. Some other constructs do not impose distributed costs but do require complicated run-time support. Removing support for these constructs reduces object code size and improves speed, dramatically.
Ravenscar is designed to maximize simplicity to the degree necessary to meet all of the domains' requirements. Therefore, when certification or formal (e.g., safety) analysis is required, Ravenscar is clearly the right choice. When the smallest possible object code size, and absolutely utmost performance is required, Ravenscar is again the best choice.
The cost of a simplified RTL, however, is reduced expressive power at the language level. The most expressive language constructs require RTL support and cannot be made available without it. The requeue statement is a good example, as are task entries and accept statements. A rendezvous is effectively an atomic action with two participants, a very potent facility that requires integrated run-time support for both tasking and exceptions.
Both profiles trade away expressive power, but to different extents. The controlling factor is the analyses: the high-integrity and safety-critical domains necessitate stringent analyses, whereas the real-time and embedded domains do not. It follows that they do not, in isolation, require the same degree of simplicity. Consequently, Jorvik is designed to enhance expressive power for applications that are only in the real-time and/or embedded domains. As we said earlier, Ravenscar can be used in this case, and sometimes should be used, but the additional expressive power of Jorvik makes it an attractive alternative.
With that understood, let’s explore the Jorvik facilities.
The differences between the two profiles can be summarized by the restrictions that are removed or replaced from the Ravenscar restrictions list. The pertinent restrictions applied by Ravenscar are as follows:
- Max_Entry_Queue_Length => 1
- Max_Protected_Entries => 1
- Simple_Barriers
- No_Relative_Delay
- No_Dependence => Ada.Calendar
- No_Dependence => Ada.Synchronous_Barriers
- No_Implicit_Heap_Allocations
The first two restrictions are the most significant. Removing the first allows multiple callers to be queued simultaneously on a protected entry in Jorvik, rather than at most one. Removing the second restriction allows multiple protected entries per protected object (PO). Note that task schedulability analysis remains possible, and the new aspect Max_Entry_Queue_Length can be used to good effect when performing that analysis.
Given those two protected entry relaxations, classic protected type idioms are much more likely allowed in Jorvik. Our example is a concurrent bounded buffer, with two entries and as many queued callers at runtime as necessary:
generic
type Element is private;
package Concurrent_Bounded_Buffers is
type Content is array (Positive range <>) of Element;
protected type Bounded_Buffer (Capacity : Positive) is
entry Put (Item : in Element);
entry Get (Item : out Element);
function Is_Empty return Boolean;
function Is_Full return Boolean;
private
Values : Content (1 .. Capacity);
Next_In : Positive := 1;
Next_Out : Positive := 1;
Count : Natural := 0;
end Bounded_Buffer;
end Concurrent_Bounded_Buffers;
The other major difference between the two profiles is the content of entry barrier expressions. Ravenscar applies the Simple_Barriers restriction that requires these expressions to consist of either a static expression or a name that statically denotes a Boolean component of the enclosing protected object. Loosely speaking that means either Boolean literals (e.g., “when True”), or single Boolean components (e.g., “when Some_Boolean”). Jorvik replaces Simple_Barriers with a new restriction named Pure_Barriers. The new restriction allows more complex Boolean expressions, within limits.
Loosely speaking, Pure_Barriers allows the following content for scalar expressions comprising protected entry barriers. You should assume that there are restrictions in the details that I am glossing over. (See RM clauses D.7 and 4.9 for the full definitions.)
- a static expression (numeric literals, named numbers, static constants, static calls to static functions, certain attributes, etc.);
- a name for a scalar (i.e., a discrete or real type) component of the enclosing protected unit;
- a Count attribute reference for an entry in the enclosing protected unit;
- a call to a predefined relational operator or Boolean logical operator;
- a membership test;
- a short-circuit control form;
- a conditional_expression;
- an allowed expression that is enclosed in parentheses.
No other language entities are allowed in the barrier expressions. Content is restricted so that side effects, exceptions, and recursion are impossible. Precluding them is important because the language does not specify the number of times a given barrier is evaluated. With these restrictions in place the number of evaluations won’t matter.
Given this relaxed content, the typical implementations for our Bounded_Buffer entry bodies are allowed without changes, including especially the entry barriers:
protected body Bounded_Buffer is
entry Put (Item : in Element) when Count /= Capacity is
begin
Values (Next_In) := Item;
Next_In := (Next_In mod Capacity) + 1;
Count := Count + 1;
end Put;
entry Get (Item : out Element) when Count > 0 is
begin
Item := Values (Next_Out);
Next_Out := (Next_Out mod Capacity) + 1;
Count := Count - 1;
end Get;
function Is_Empty return Boolean is
(Count = 0);
function Is_Full return Boolean is
(Count = Capacity);
end Bounded_Buffer;
For the sake of comparison, imagine we have some other protected object and are using the Ravenscar profile. There will be only one entry, but let’s reuse entry Get above just for illustration. In Ravenscar, we would have a new Boolean component used solely for the entry barrier. It could be named Not_Empty, would be initialized to False, and then updated in the entry body:
entry Get (Item : out Element) when Not_Empty is
begin
Item := Values (Next_Out);
Next_Out := (Next_Out mod Capacity) + 1;
Count := Count - 1;
Not_Empty := Count > 0;
end Get;
We must include the negation in the name and value because Simple_Barriers requires static expressions. We could not say “not Empty” in the barrier. But note that the assignment to Not_Empty in the entry body has no barrier-oriented restrictions, so the expression comparing Count to zero is allowed, as would much more complex, potentially non-static references. This approach certainly works, but it isn’t the way one would write an entry body and barrier normally, and we’d like to use implementations without requiring code changes when possible. That won’t always be possible, though, because Pure_Barriers does restrict barrier content. The Ravenscar approach might be used occasionally in Jorvik applications too, in combination with the content Jorvik allows.
Note that, in the list of content allowed by Jorvik’s Pure_Barriers, “a name that statically names a scalar subcomponent of the immediately enclosing protected unit” has a specific meaning you need to understand. Remember that the Pure_Barriers restriction doesn’t allow anything that can raise exceptions. Therefore, any part of an expression that has to be checked at run-time is not allowed. For example, maybe you have a discriminated record type with dependent components, a default for the discriminant, and a PO component of this type that takes the default. The dependent record components don’t exist except for specific values of the discriminant, which, thanks to the default, can vary as the program executes. Ada checks to make sure that references to those components are consistent with the current value of the discriminant, raising an exception if the check fails. Such a reference would be rejected by the compiler in an expression required to be consistent with the Pure_Barrier restriction. It is not “pure-barrier-eligible” to use the technical term. Likewise, if you have an object of some array type, the correctness of a variable used as the index must be checked (in certain cases). That usage would not be allowed. In other cases, though, the index need not be checked, because the index value is static -- determinable at compile-time -- and so can be checked then.
To make this discussion concrete, let’s change the private part and body of the Bounded_Buffer type so that we use a record object. Currently, the private part is as shown earlier:
private
Values : Content (1 .. Capacity);
Next_In : Positive := 1;
Next_Out : Positive := 1;
Count : Natural := 0;
end Bounded_Buffer;
Let’s say that Next_In, Next_Out, and Count are to be components of a record object instead of direct PO components. In this case that wouldn’t really be worth doing, but we’ll use it to illustrate what’s allowed. In real code, though, especially an application specific PO, you might very well compose the PO from various abstract data types declared in their own packages (that being good software engineering, after all).
type Management is record
Next_In : Positive := 1;
Next_Out : Positive := 1;
Count : Natural := 0;
end record;
protected type Bounded_Buffer (Capacity: Positive) is
… as before
private
Values : Content (1 .. Capacity);
State : Management;
end Bounded_Buffer;
The entry barriers then become:
entry Put (Item : in Element) when State.Count /= Capacity is
…
entry Get (Item : out Element) when State.Count > 0 is
…
The references are slightly more verbose, but the point is that the barriers can reference those record components because they are scalar components, because State is declared immediately within the PO, and because the called functions (the relational operators) are static functions statically called. Your real, application-specific PO may very well contain objects of composite types, and you can reference their components in the barriers as long as they follow the rules.
Similarly, and perhaps abandoning realistic code altogether, we could use an array of three Integers in place of the three distinct variables. We could say that Next_In will now be State (1), Next_Out will now be State (2), and Count will be State (3).
type Management is array (1 .. 3) of Positive;
protected type Bounded_Buffer (Capacity : Positive) is
…
private
Values : Content (1 .. Capacity);
State : Management;
end Bounded_Buffer;
The entry barriers would be like so:
entry Put (Item : in Element) when State (3) /= Capacity is
…
entry Get (Item : out Element) when State (3) > 0 is
…
That approach would not be an improvement, all other things being equal. But it serves to show that array indexing is allowed when the indexes are static.
What would be an improvement, however, is using the two existing functions, Is_Full and Is_Empty, in the barriers. They directly express what the reader must otherwise deduce:
entry Put (Item : in Element) when not Is_Full is
…
entry Get (Item : out Element) when not Is_Empty is
…
Sadly, those barrier expressions are not allowed by Pure_Barriers because Is_Full and Is_Empty are not static functions. They cannot be made to be static, either.
The other restrictions removed in Jorvik are mostly a matter of application developer convenience.
We fully expect Jorvik applications to delay periodic tasks with absolute delay statements, just as in Ravenscar applications. Elsewhere, a relative delay statement can be appropriate, and they are now allowed. For example, an electro-mechanical relay may have a requirement that it not be actuated more than N times per second in order to prevent burn-out. The semantics of a relative delay match that requirement nicely.
In a way, relative delay statements were already allowed in Ravenscar, via the ugly “hack” of using an absolute delay statement to delay until the value of Clock + some-time-span. Jorvik isn’t really adding much here, but the direct expression is cleaner and simpler.
Jorvik removes the restriction prohibiting use of the Ada.Calendar package. This restriction is present in Ravenscar because the Ada.Real_Time package has more appropriate semantics for real-time/embedded applications. However, not all usage of Ada.Calendar is unreasonable, for example time-stamping log messages. That said, Ada.Real_Time will surely remain the primary facility.
Jorvik removes the restriction prohibiting use of the Ada.Synchronous_Barriers package. A “barrier” in this case is an abstract data type, not a Boolean expression controlling a protected entry. The semantics are much like visiting a restaurant that requires all members of the dinner party to be present before any are seated. An object of type Synchronous_Barrier has a discriminant that specifies how many tasks are in the “party.” Once that many tasks “arrive” by calling the entry for that object, the entire set of caller tasks are allowed to continue. The obvious implementation of type Synchronous_Barrier is as a protected type that, by definition, must allow multiple callers to queue on a single entry. Jorvik allows that implementation so there was no need to restrict the package.
Finally, the restriction No_Implicit_Heap_Allocations is removed. That restriction is most pertinent to the domains requiring certification and/or safety analyses, but Jorvik is not targeted to those domains. Some implicit allocations would not be a problem for Jorvik applications. Nevertheless, related restrictions are needed in this regard. Recall that in both Ravenscar and Jorvik no protected objects or tasks are ever allocated. They are always declared. There are cases, however, in which GNAT would allocate a task or protected object dynamically, transparently, even though an allocation is not visible in the source code. The restriction No_Implicit_Heap_Allocations would catch that, but we’ve removed it in Jorvik.
For example, consider a composite object declared in a library package, say a String object. If the bounds of the object are not known at compile-time GNAT will allocate the object, implicitly.
with Max_Size; -- a function
package P is
Name : String (1 .. Max_Size);
end P;
Now, instead of being a library object, imagine Name is a component of a protected type or protected object:
with Max_Size; -- a function
package P is
protected PO is
procedure Q;
private
Name : String (1 .. Max_Size);
end PO;
end P;
It’s the same problem, except now the compiler will be allocating the enclosing protected object, thus violating the restriction. The same behavior is possible for task objects. Therefore, GNAT adds two new restrictions to Jorvik to prevent these specific cases: No_Implicit_Task_Allocations and No_Implicit_Protected_Object_Allocations.
With those two restrictions in place, the above code causes this error message from GNAT:
p.ads:7:07: violation of restriction "No_Implicit_Protected_Object_Allocations"
These two restrictions are not part of the Jorvik profile in the Ada 2022 standard. They are specific to the GNAT implementation. However, we intend to argue for them in a subsequent update to the standard.
In conclusion, if you are unsure when to use one of the profiles, or any subset, there is an applicable maxim, originally expressed for Ravenscar: “If an application cannot be reasonably expressed within the Ravenscar subset, it isn’t a Ravenscar application.” In other words, the application code in these domains, particularly those undergoing rigorous analyses, must be very simple, and, consequently, will be expressible in the subset. Otherwise, the project lead should review whether adhering to Ravenscar is appropriate. That maxim is true for the Jorvik profile as well. If an application “genuinely requires” requeue statements, for example, maybe a larger subset is appropriate.
Of course, “genuinely requires” is difficult to define precisely, especially because one can work around some of the two profiles’ restrictions via additional application source code. For example, multiple entry queues in a single protected object can be simulated via multiple protected objects, each with a single entry. This additional application code, in effect, implements in a bespoke manner that which the run-time library would have implemented more generally, had the corresponding restriction not been in place. However, that additional source code injects complexity back into the system under analysis. In a very real sense, the complexity has been “moved” from the run-time library up to the application level. At some point, additional application code complexity argues against use of the profiles. That said, Ravenscar is widely used, and justly so. We think Jorvik will be as well.
[1] P. Rogers, J. Ruiz, T. Gingold, and P. Bernardi, A New Ravenscar-Based Profile in Reliable Software Technologies Ada-Europe 2017, Johann Blieberger and Marcus Bader (eds) (2017), LNCS 10300, Springer-Verlag, pp. 169-183.