4. The Predefined Profiles¶

This chapter describes what is prohibited and what is permitted in the different predefined profiles.

4.1. Choosing a Predefined Profile¶

You choose a particular profile through either of two approaches:

Set the Runtime attribute in a project file (the recommended technique); or
Set the GNAT configuration mode, via the --RTS= switch.

Both approaches specify the run-time library.

You need to specify the run-time library to the compiler, to gnatbind, to gnatlink, to gnatmake, and in general to any tool that needs to be aware of the run-time configuration.

Here is an example showing how to specify the run-time library in a project file (note the necessary inclusion of the language name as index):

project Demo is
    ...
    for Runtime ("Ada") use "ravenscar-cert";
    ...
end Demo;

For platforms with an underlying operating system (e.g., VxWorks), the values for the attribute/switch are zfp, cert, ravenscar-cert and ravenscar-cert-rtp, corresponding to the establishment of Zero Footprint, Cert, Ravenscar Cert Kernel, and Ravenscar Cert RTP profiles, respectively.

Depending on the targeted environment, there may be other supported full Ada alternatives. These are not described here; see the GNAT User’s Guide Supplement for Cross Platforms. The switch settings are not case sensitive.

The set of available profiles depends on the target.

Bare-board and PikeOS Configurations

The Zero Footprint, Ravenscar SFP and Ravenscar Full profiles are supported. In a few words, the runtimes could be ordered like this: zfp (Zero Footprint) < Ravenscar SFP < Ravenscar Full.

There are various criteria for choosing (and there may be contradictions):
- If you don’t plan to use tasking, you’d better to choose zfp, but full also provides many additional packages.
- If you plan to certify your software, choose either zfp or Ravenscar SFP (avoid Ravenscar Full).
- If you need tasking, you have the choice between Ravenscar SFP or Full (zfp doesn’t support tasks).
- If you need exception handlers, then choose Ravenscar Full (zfp and Ravenscar SFP don’t support exception propagation).
The Ravenscar full runtime provides many features over Ravenscar sfp; but it is possible to import some features from full (like the math library) to Ravenscar sfp.

The Zero Footprint and Ravenscar SFP only provide a simple implementation of memory allocation (Gnat_Malloc, see Allocators and the High-Integrity Profiles).

The mechanism relies on the __heap_start and __heap_end symbols to delimit the memory area that can be allocated. Those symbols are defined by the linker script used for the specific board being targeted.

Memory deallocation is a no-op, the rationale being that with certifiable software, dynamic memory allocation is performed only once, at startup, so freeing the memory is unnecessary. This restriction allows a simple, efficient, and predictable behavior for memory allocation.
VxWorks Cert 6.x

Zero Footprint, Ravenscar Cert and Full Profiles are supported. The Cert profile is also supported when VxWorks Cert is used as a Guest Operating System under VxWorks 653 3.x.
VxWorks 653

Zero Footprint, Cert, Ravenscar Cert and Full Profiles are supported.
PikeOS

Zero Footprint, Ravenscar SFP and Ravenscar Full are supported.
Development Host

A native version of the Zero Footprint run-time library is provided for all high integrity development hosts to facilitate native platform testing. It should be installed into the same location as the corresponding native development system. It is selected as described above, using either the Runtime attribute or the --RTS switch. Note that this run-time library is a distinct download available on the GNATtracker page for the high integrity cross-development system.

4.2. The Zero Footprint Profile¶

With the Zero Footprint Profile the generated object modules usually contain no references to the GNAT run-time library. There are a few exceptions related to floating point attributes or for support of software emulated floating point operations. The absence of references to the run-time allows the construction of a standalone program that has no code other than that corresponding to the original source code, together with the elaboration routine generated by the binder. The elaboration routine generated by the binder also avoids any reference to runtime routines or data.

4.2.1. The -nostdlib Switch¶

In a certification context, it may be important to guarantee the enforcement of a strict Zero Footprint Profile where one can ensure that no external library is linked with the final image. This can be achieved by using the builder switch -nostdlib. The GNAT builders (gnatmake, gprbuild) will pass this switch to the binder and to the linker, with the effect of removing the run-time libraries such as libgnat.a and libgcc.a from the link path.

In order to use the -nostdlib switch, the program must meet a number of restrictions in addition to those listed in Ada Restrictions in the Zero Footprint Profile:

No references to entities from runtime packages, e.g., Ada.External_Tag;
No use of pragma Assert;
No use of the following floating-point attributes: - Adjacent, - Ceiling, - Compose, - Copy_Sign, - Exponent, - Floor, - Fraction, - Leading_Part, - Machine, - Machine_Rounding, - Model, - Pred, - Remainder, - Rounding, - Scaling, - Succ, - Truncation, - Unbiased_Rounding (with nonstatic arguments), and - Valid and Unaligned_Valid (with any argument);
No use of a secondary stack (this can be enforced by including pragma Restrictions(No_Secondary_Stack); and
No use of floating-point or other arithmetic operations that are too complex for inline expansion and that therefore require calls to a support library.

4.2.2. Ada Restrictions in the Zero Footprint Profile¶

The following features are excluded from the Zero Footprint Profile:

All constructs defined in Section 9 of the Ada Reference Manual (i.e., all tasking features)
Exception propagation. See Exceptions and the High-Integrity Profiles; note that raise statements and local exception handling are permitted.
Packed arrays with a component size other than 1, 2, 4, 8 or 16 bits; if a packed array has static bounds and the overall size of the array is 64-bits or less, all component sizes are allowed. Note that the restriction applies to accessing or setting elements of such an array (it is permissible to declare a packed array with any component size).
The exponentiation operator, unless one of the following conditions is met:
- The exponentiation expression is a static expression as defined in the Ada Reference Manual, section 4.9
- The right operand is a static expression as defined in the Ada Reference Manual, section 4.9, and is an integral value in the range 0 .. 4
64-bit integer (the type Long_Long_Integer) and fixed-point types
Boolean operations on packed arrays (individual elements may be accessed)
The attributes Value, Body_Version, Version, Width, and Mantissa
The attribute Image for types other than modular integers, signed integers, and Boolean.
Controlled types
The attributes Address, Access, Unchecked_Access, Unrestricted_Access when applied to a non library-level subprogram
Non library-level tagged types
Annex E features (Distributed Systems)

Note that explicit withs of library units are still permitted but the programmer needs to ensure that the GNAT library modules that come with the compiler that is being used in Zero Footprint mode satisfy the requirements of the target hardware.

In particular, in an environment where the code needs to be certified, the user takes responsibility for ensuring that the referenced library unit meets the certification conditions.

4.2.3. Predefined Packages in the Zero Footprint Profile¶

In general, the predefined Ada environment (Annex A), the interfacing packages (Annex B), and the units in the Specialized Needs Annexes may be implemented with the full Ada language and thus will not be appropriate in applications that need to adhere to the Zero Footprint Profile. The only predefined Ada units that are permitted (i.e., that may be withed) in a Zero Footprint Profile program are as follows:

Package System
Package Ada.Tags
Generic function Ada.Unchecked_Conversion
Generic procedure Ada.Unchecked_Deallocation
Package Interfaces, except that references to the types Integer_64 and Unsigned_64 are prohibited
Package Interfaces.C
Package Interfaces.C.Extensions, except that references to Signed_64 and Unsigned_64 are prohibited
Package System.Storage_Elements
Generic package System.Address_To_Access_Conversions
Package System.Machine_Code

Additionally, the following GNAT packages are permitted since all their subprograms are either intrinsic or are expanded inline:

Package GNAT.Source_Info
Package GNAT.IO, which provides basic input / output capabilities

A sample implementation of the secondary stack is provided that can be used and tailored (in the file s-secsta.adb). However, since no certification material is provided for this sample implementation, it is your responsibility to certify this implementation. See Functions Returning Unconstrained Objects, for further details.

s-memory.adb is not provided. If you want to use allocators and unchecked deallocation, you will have to define __gnat_malloc and __gnat_free. See Allocators and the High-Integrity Profiles, for further details.

4.2.4. Thread Registration Issues¶

The Zero Footprint profile does not provide run-time facilities that require per-thread data. Therefore, thread registration is not relevant to this profile.

4.2.5. Pragmas Automatically Enabled in the Zero Footprint Profile¶

The following pragmas are automatically enabled when the Zero Footprint Profile is in effect:

pragma Restrictions (No_Exception_Propagation)
pragma Restrictions (No_Exception_Registration)
pragma Restrictions (No_Implicit_Dynamic_Code)
pragma Restrictions (No_Finalization)
pragma Restrictions (No_Tasking)
pragma Discard_Names

4.2.6. Exceptions and the Last Chance Handler - ZFP and Ravenscar SFP¶

In this profile, all applications are treated as though pragma Restrictions (No_Exception_Propagation) has been applied. It is possible to raise the predefined Ada exceptions, as well as user-defined exceptions and handle them locally.

When such an exception is raised and not handled locally, a function with the following C-convention prototype is called (note that the function name begins with two underscore characters):

void __gnat_last_chance_handler (char *source_location,
                                 int line);

The corresponding Ada subprogram declaration is:

procedure Last_Chance_Handler
  (Source_Location : System.Address; Line : Integer);
pragma Export (C, Last_Chance_Handler,
               "__gnat_last_chance_handler");

The Source_Location parameter is a C null-terminated string representing the source location of the raise statement, as generated by the compiler, or a zero-length string if pragma Suppress_Exception_Locations is used.

The Line parameter (when nonzero) represents the line number in the source. When Line is zero, the line number information is provided in Source_Location itself.

4.3. The Cert Profile¶

The Cert profile is a superset of the Zero Footprint Profile, and thus Predefined Packages in the Zero Footprint Profile, is relevant. This section describes the additional capabilities provided by the Cert profile. The Cert profile also provides atttributes 'Image and 'Value.

The Cert profile is based on an implicitly threaded run-time library. The current implementation of this profile is for use on Wind River Systems VxWorks 653 2.x vThreads partition OS and the VxWorks 653 3.x VxWorks 6 Cert Guest OS with APEX processes. Although there are no Ada tasks, there are different threads (VxWorks 653 vThreads or VxWorks 6 tasks) executing the code and accessing data structures. For example, The following data items must be per-thread:

secondary stack,
thread-accessible pointer to jump buffer,
thread-accessible pointer to secondary stack location.

By “thread-accessible”, we mean that a thread-specific data item is needed to implement the behavior defined by the subset.

4.3.1. Exceptions and the Last Chance Handler - Cert and Ravenscar Cert Profiles¶

The full semantics of Ada 83 exceptions is supported; limited support for Ada 95 / Ada 2005 / Ada 2012 exception occurrences is included. The run-time library supports propagation of exceptions and handlers for multiple threads, provided that the threads have been registered with the Ada run-time library: see Thread Registration, for details.

The run-time libraries provided by these profiles (both available in GNAT Pro Safety-Critical for VxWorks 653, and Ravenscar Cert in GNAT Pro Safety-Critical for VxWorks Cert 6.x) support limited Ada 95 / Ada 2005 exception occurrences, Ada.Exceptions.Exception_Name, and a non-symbolic stack trace capability Ada.Exceptions.Exception_Traces.

As with the zero footprint case, the application developer may provide a body for a last chance handler, to deal with unhandled Ada exceptions. The declaration of the last chance handler for these profiles is:

procedure Ada.Exceptions.Last_Chance_Handler (Except : Exception_Occurrence);
  pragma Export (C,
                 Last_Chance_Handler,
                 "__gnat_last_chance_handler");
  pragma No_Return (Last_Chance_Handler);

Except is an Ada 95 / Ada 2005 / Ada 2012 exception occurrence that can be used to identify the exception and the circumstances under which it occurred. A default body is provided in the rts-cert/adainclude directory of the restricted run-time library as file a-elchha.adb. Its object module a-elchha.o is archived in rts-cert/adalib/libgnat.a along with a partially linked object module libgnat.o containing the remainder of the Cert profile run-time library. This example handler generates a non-symbolic traceback that can be used on the development host to obtain a symbolic traceback via the vxaddr2line utility. It also propagates an event to the VxWorks 653 health monitor on VxWorks 653.

Note that the last chance handler can have any name, and can be written in C. However, it must obey the parameter profile and export the symbol __gnat_last_chance_handler as its entry point.

If you do not supply a last chance handler, the default version will be linked into your application.

The last chance handler for the Cert profile on VxWorks 653 is expected to suspend the vThread or VxWorks task that calls it.

See the GNAT User’s Guide Supplement for Cross Platforms for the details of providing an application-specific last chance handler.

4.3.2. Secondary Stack¶

The secondary stack supports functions returning objects of unconstrained types (e.g., unconstrained array types) and of variant record types. The default secondary stack size (for the environment task) can be set using the gnatbind ‘-D’ switch, that specifies the value in Kbytes. For APEX processes, the value defaults to 1/4 the requested primary stack size, and is added to the requested allocation from APEX. The size can also be specified in the Apex_Processes.Create_Process routine.

4.3.3. Thread Registration¶

The thread registration mechanism allows applications to use system threads with Ada code. Specifically, the mechanism supports the Ada exception semantics outside of an Ada tasking context, so that Ada code that uses exceptions can be called by a non-Ada thread. The mechanism is also necessary to support unconstrained function results in Ada code called by system threads.

The Ada/APEX bindings provided with GNAT Pro Safety-Critical for VxWorks 653 takes care of all thread registration issues when using APEX processes. The bindings are provided as part of the source and object paths, just like the remainder of the Ada run-time library.

Ravenscar Cert does not support the use of foreign threads (eg APEX processes).

4.3.4. Dynamic Allocation¶

A limited dynamic allocation model is supported by this profile. The package System.Memory is provided, as described in Allocators and the High-Integrity Profiles. The package provides a simple version of function gnat_malloc that simply calls the underlying malloc routine. Deallocation is prohibited on VxWorks 653 in certified partition operating system (POS) application partitions.

Note that in VxWorks 653 partitions that use APEX facilities, dynamic allocation is prohibited once the partition has been set into normal mode.

4.3.5. Exponentiation¶

The cert subset supports all standard Ada forms of exponentiation.

4.3.6. 64-bit Numeric Types¶

64-bit fixed point and integer types are fully supported.

4.3.7. Utility Routines¶

The following are provided in addition to the library packages available with the Cert Profile:

GNAT.Debug_Utilities provides formatting routines for use in I/O.
Ada.Exceptions.Exception_Traces provides a non-symbolic traceback capability that can be used with vxaddr2line to generate symbolic tracebacks. See The GNAT User’s Guide Supplement for Cross Platforms.
Pragma Assert is supported.
Ada.Numerics, Ada.Numerics.Generic_Elementary_Functions, Ada.Numerics.Elementary_Functions, Ada.Numerics.Long_Elementary_Functions and Ada.Numerics.Long_Long_Elementary_Functions are supported.

4.4. The Ravenscar Profiles¶

The Ravenscar Profile, named for the venue of the 1997 International Real-Time Ada Workshop where it was first proposed, defines a subset of tasking features suitable for use in applications having extremely demanding requirements. The profile is a part of the Ada programming language and is defined by the language standard in section D.13 of the Real-Time Systems annex. Note that only the tasking subset is specified by the profile; the rest of the language is not addressed.

The profile is intended to support four application domains:

hard real-time applications requiring predictability,
safety-critical applications requiring formal certification,
high-integrity applications requiring formal verification, and
embedded applications requiring small memory footprint and low execution overhead.

The wide range and nature of these requirements necessitate a subset of full Ada tasking. Otherwise, the space/speed overhead is too high, and the complexity of the application code and the underlying run-time library code either preclude analysis or make it prohibitively expensive. For example, abort statements significantly complicate the run-time library implementation and impose size and execution time penalties even when not used in the application.

The resulting tasking subset is designed to be small enough to allow efficient and analyzable run-time libraries, but large enough to permit programming styles needed in practice for these domains.

GNAT Pro provides a number of run-time libraries providing the standard Ravenscar tasking subset, with differing parts of the remaining sequential language supported. The following sections describe these run-times.

4.4.1. Ada Restrictions in the Ravenscar Profiles¶

The tasking restrictions defined by the Ravenscar Profile are itemized in the following list; details on the rationale and implications may be found in The Ravenscar Profile for High-Integrity Real-Time Programs by A. Burns, B. Dobbing and G. Romanski, in Reliable Software Technologies – Ada Europe ‘98, Springer-Verlag Lecture Notes in Computer Science, Number 1411.

No locally-declared task objects or task types
No dynamic allocation (and hence no unchecked deallocation) of task objects or protected objects
No task termination
No locally-declared protected objects or protected types
At most one entry for each protected object/type
Each entry barrier expression must be a single Boolean variable
At most one task at a time may be queued on an entry
No requeue statements
No abort statements or Asynchronous Transfer of Control
No select statements
No task entries (and thus no accept statements)
No relative delay statements
No references to package Ada.Calendar
No user-defined task attributes
No use of dynamic priorities

4.4.2. Ada Features Permitted in the Ravenscar Profiles¶

The Ravenscar profile allows the following tasking features:

Task type and task object declarations in library-level packages
Protected type and protected object declarations in library-level packages
Absolute delay (delay until) statements
References to package Ada.Real_Time
Pragmas Atomic and Volatile for shared data
Count attribute (but not in a barrier expression)
References to package Ada.Task_Identification (but no Abort_Task or task attribute functions Callable or Terminated)
Discriminants for protected types and task types
Protected procedures as interrupt handlers
FIFO_Within_Priority dispatching policy
Ceiling_Locking locking policy

Implementations may also support non-preemptive or cooperative dispatching policies.

The original Ravenscar Profile from the 1997 International Real-Time Ada Workshop defined only a tasking subset and was silent about restrictions on sequential features. In the context of GNAT Pro Safety-Critical and GNAT Pro High-Security, the term Ravenscar Profile means not only the tasking subset just presented, but also the sequential feature subset defined either by the Zero Footprint Profile (Ravenscar SFP) or the Cert Profile (Ravenscar Cert). Thus the Ravenscar SFP Profile is a proper superset of the Zero Footprint Profile and the Ravenscar Cert Profile is a proper superset of the Cert Profile (excepting packages Ada.Calendar and Calendar, which are prohibited by the Ravenscar profile).

A user specifying ravenscar-sfp as the --RTS= option will therefore be able to use the permitted features in the Zero Footprint Profile.

A user specifying ravenscar-cert or ravenscar-cert-rtp as the --RTS= option will be able to use the permitted features in the Cert Profile.

4.4.3. Pragmas Automatically Enabled in the Ravenscar Profiles¶

The same pragmas automatically enabled in the Zero Footprint profile (see Pragmas Automatically Enabled in the Zero Footprint Profile) are also automatically enabled in the Ravenscar SFP profile:

pragma Restrictions(No_Exception_Handlers)

The Ravenscar SFP Profile uses the same last chance handler scheme as the Zero Footprint Profile. The Ravenscar Cert Profile uses the same scheme as the Cert Profile. The last chance handler is expected to terminate the whole application in both cases.
pragma Discard_Names

This pragma is enabled for both Ravenscar profiles.

4.4.4. Non-tasking Predefined Packages in the Ravenscar Profiles¶

The Ravenscar SFP Profile is a superset of the Zero Footprint Profile. So Predefined Packages in the Zero Footprint Profile, is still relevant to the Ravenscar Profile, with one difference: s-secsta.adb is provided. See Functions Returning Unconstrained Objects for further details.

The Ravenscar Cert Profile is a superset of the Cert Profile. It provides the same packages as the Cert Profile, except for Ada.Calendar and Calendar, which are disallowed by the Ravenscar profile definition. The Ravenscar Cert profile also provides atttributes 'Image and 'Value as does the Cert profile.

4.4.5. Interrupt Handling in the Ravenscar Profiles¶

Interrupt handling is supported in the Ravenscar Profiles except for the VxWorks 653 target, LynxOS-178 and in VxWorks 6 Cert. The mechanism is as defined in Annex D of the Ada Reference Manual; the handler is supplied as a parameterless protected procedure, pragma Attach_Handler provides static attachment, and Interrupt_Priority establishes the priority of the handler.

In GNAT Pro Safety-Critical for VxWorks DO-178B and in VxWorks 6 Cert SKM’s, you can use the intConnect() routine directly, for dynamic attachment of handlers to interrupts.

In either case there is no task switching; the interrupt handler is executed at the priority given by the Interrupt_Priority pragma, on the stack of the task that was running when the interrupt occurred (for VxWorks) or on a dedicated interrupt stack (for bare-board platforms).

4.5. The Extended Ravenscar Profiles¶

The GNAT Extended Ravenscar Profile is a distinct profile based on standard Ravenscar. The extended profile is expected to become a part of the Ada language standard, in addition to the existing Ravenscar profile.

The new profile relaxes the restrictions imposed by the Ravenscar profile to provide greater Ada tasking support for applications in the real-time and embedded system domains. These two domains do not require the formal certification and verification analyses of the other application domains. As a result, the new profile can provide greater expressive power with an underlying run-time library that, although more complex, nonetheless supports timing analysis as well as small and efficient implementation.

GNAT Pro provides a number of run-time libraries providing the extended Ravenscar tasking subset, with differing parts of the remaining sequential language supported. The following sections describe the extended Ravenscar profile included in these run-times. Anything not specified as removed or altered from the Ravenscar profile remains unchanged in the GNAT Extended Ravenscar profile.

4.5.1. Protected Entries¶

The GNAT Extended Ravenscar Profile removes certain restrictions pertaining to protected entries and also adds new functionality.

4.5.1.1. Number of Entries Per Protected Object¶

The extended profile does not specify a value for Max_Protected_Entries. As a result, multiple entries per protected object are allowed.

Note that this change also allows entry families to have more than one member.

4.5.1.2. Number of Queued Callers¶

The extended profile does not specify Max_Entry_Queue_Length. As a result, multiple callers can be queued on any given protected entry, rather than only one at a time. Note that task entries remain disallowed.

In addition, any protected object containing protected entry declarations can specify, for each entry, the maximum number of callers allowed. This maximum number is checked at runtime, if specified, and can be used to compute a less pessimistic WCET off-line. Specification of the maximum value is optional.

The maximum value for any given protected entry is specified via the aspect or pragma Max_Queue_Length applied to that entry. The value must be a static (positive) integer value. For example:

protected type P is

   entry A (Item : Integer)
      with Max_Queue_Length => 2;

   entry B (Item : Integer);
   pragma Max_Queue_Length (X);

private
   ...
end P;

4.5.1.3. Entry Barriers¶

The extended profile does not specify Simple_Barriers. Instead, the GNAT-defined restriction “Pure_Barriers” is applied automatically. As a result, in addition to simple Boolean local variables, more complex Boolean expressions are allowed.

However, these expressions are still limited in content so that side effects, exceptions, and recursion are impossible. Removing the possibility of side effects is important because the language does not specify the number of times a given barrier is evaluated. Allowing exceptions would complicate the implementation, whereas the goal is an efficient and predictable run-time library implementation that minimizes barrier evaluation cost.

Specifically, “Pure_Barriers” allows only the following:

Components of the protected object (excluding selection from dereferences)

Discriminants of the protected object

Numeric literals

Enumeration (and thus character) literals

Named numbers

Predefined relational operators

Logical operators (“and”, “or”, “xor”)

Short-circuit control forms (“and then”, “or else”)

The logical negation operator (“not”)

The Count attribute

Note that the Count attribute is allowed in the barriers for protected entries (and protected entry families), not just within entry bodies.

4.5.2. Relative Delay Statements¶

The extended profile does not specify No_Relative_Delay. As a result, both relative and absolute delay statements are allowed.

Although relative delay statements are not appropriate for expressing cyclic behavior, there are cases in which a relative delay has precisely the required semantics. For example, a relay may have a requirement that it not be actuated more than N times per second. A relative delay after each actuation directly implements that requirement.

4.5.3. Additional Non-Tasking Restrictions Removed¶

Some Ravenscar restrictions are not related to tasking and can be relaxed without affecting timing analysis and space/speed performance.

4.5.3.1. No_Implicit_Heap_Allocations¶

The extended profile does not specify No_Implicit_Heap_Allocations. This restriction is in the standard Ravenscar profile for the sake of the other domains and need not be applied when focusing on real-time and embedded systems. Although the run-time library should not implicitly allocate memory, application code should be able to do so. Note that users can specify this restriction in their application code if they want the restriction to apply.

4.5.3.2. No Dependence on Ada.Calendar¶

The extended profile removes the restriction prohibiting use of the Ada.Calendar package. This restriction is present in standard 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.

4.5.4. Default Profile¶

The GNAT Extended Ravenscar profile is active by default on those platforms that support it. Users can instead specify the Ravenscar profile by applying pragma Profile, with Ravenscar as the parameter.

Table Of Contents

Previous topic

Next topic

This Page