Making software FACE-conformant and fully portable: Coding guidance for Ada

Story

March 15, 2021

Benjamin Brosgol

AdaCore

The FACE [Future Airborne Capability Environment] approach to reducing life cycle costs for the military is based on reusing software components across different platforms and airborne systems. The FACE Technical Standard addresses this issue through a reference architecture and data model, well-defined interfaces, and widely used underlying industry standards (IDL, Posix, ARINC-653).

Conformance with the FACE [Future Airborne Capability Environment] requirements is a necessary condition for reuse and software portability, but full source-code portability means more than using a common set of interfaces. In order for a FACE-conformant software component – known as a Unit of Conformance or UoC – to be fully portable, it should have equivalent behavior across different platforms and/or compiler implementations. However, each of the programming languages called out in the FACE Technical Standard – C, C++, Ada, and Java – has features whose effect may depend on the compiler implementation or target platform. Writing a fully portable UoC in any of these languages involves avoiding the potential implementation dependencies. Where full portability is not possible, for example if there are intrinsic target dependencies, the software structure should encapsulate such dependencies.

Ada has strong advantages to FACE UoC developers in terms of software engineering support and program reliability, and it was designed to facilitate the development of fully portable code, but even Ada has features with implementation dependencies. This article shows how application developers can use Ada or its formally analyzable SPARK subset to achieve full portability of FACE UoCs, in particular for the Safety or Security capability sets / profiles defined in the FACE Technical Standard.

Functional portability

Portability, or what will be called functional portability here to distinguish it from portability in the sense of FACE conformance, has been a goal of programming-language design since the earliest days. Ideally, functional portability means that a source program can be compiled and run on one platform and then, possibly with a different vendor’s compiler, the same program can be successfully compiled and run on either the same platform or a different one and have an equivalent effect. (“Equivalent” informally means that the program has the same external effects except for those resulting from permissible timing differences. A real-time program has a limited concept of which timing differences are permissible – i.e., some of its timing constraints are essential – since missing a deadline may mean that the program fails to meet its requirements.) In practice, however, several impediments may interfere with functional portability. These can include: Using language features that are either nonstandard (i.e., unique to a specific compiler vendor), or else are standard but optional and not implemented by all compilers; using standard language features with imprecisely defined semantics; and dependence on characteristics of the target platform.

The following will offer guidance for Ada functional portability, covering both Ada 95 and Ada 2012, with a focus on features allowed by the Security and Safety capability sets of the FACE Technical Standard Edition 3.0 or later. Where applicable, the guidance shows how the SPARK Ada subset can be used to mitigate potential nonportabilities. (Here, the language name “Ada” refers to both Ada 95 and Ada 2012 unless indicated otherwise.) This guidance is not an exhaustive list; the Ada reference manual is the definitive source of information on which features can have implementation-dependent effects.

Language extensions

To prevent vendor “lock-in” from nonstandard extensions, the certification policy for Ada compilers has included a “no supersets” directive from the outset. That policy, however, has always recognized the utility of vendor-specific functionality provided that no new syntax is introduced, and thus allows certain kinds of language extensions; in particular, implementation-defined libraries, pragmas, attributes, arguments to pragma Restrictions, and (for Ada 2012) aspects.

The FACE Safety-Extended and Safety-Base & Security capability sets impose a few restrictions in this area but do not otherwise restrict such language extensions. To facilitate portability, the use of implementation-defined language extensions should be minimized. Ada 2012 has explicit support for enforcing the absence of implementation-defined extensions, through arguments to pragma Restrictions; for example, No_Implementation_Pragmas and No_Implementation_Units.

Optional features

Another impediment to functional portability is to use a standard feature that is not supported by all compilers. The certification policy for Ada addresses this issue by prohibiting subsets: every Ada compiler must implement the full language. Nevertheless, the revision process that led to Ada 95 recognized that particular domains have specialized (and sometimes conflicting) requirements, and a number of annexes (the “Specialized Needs” Annexes) are therefore optional with respect to compiler certification. A compiler has to implement the full “core” language, including the predefined environment (standard library) and the interlanguage interfacing facilities, but the Systems Programming, Real-Time Systems, Distributed Systems, Numerics, Information Systems, and Safety and Security Annexes are optional.

In practice this optionality has not been an issue, since the most commonly used annexes – Systems Programming and Real-Time Systems – are supported by the vendors in the Ada ecosystem. Moreover, the FACE Safety and Security capability sets for Ada prohibit the Distributed Systems, Numerics, and Information Systems Annexes, so their optionality is not relevant to functional portability. Nevertheless, the Systems Programming and Real-Time Annexes raise a few issues that might affect FACE UoC developers:

Some of the services defined in these annexes and permitted by the FACE Safety and Security capability sets are intrinsically system-dependent (for example, interrupt handling) and thus will require revision on porting to a different execution environment. Designing the application to encapsulate such dependencies will ease the porting effort.
The FACE Safety and Security capability sets significantly restrict the functionality supplied by these annexes. The UoC developer will need to demonstrate, through static analysis or code review/inspection, that prohibited features in these annexes are not used.

Guidance for features with implementation-dependent semantics

Functional portability requires well-defined semantics, so that a source program has an equivalent effect on each platform where it is compiled. In practice, however, there is sometimes a tradeoff between precisely defined semantics and efficient run-time performance. Since efficiency is typically a critical requirement for programmers, language standards (including Ada) contain features whose effect may vary across different implementations.

Order of evaluation in expressions

To facilitate optimization, Ada does not specify the order of evaluation of the terms comprising an arithmetic expression, but in some cases the effect depends on the order that the compiler chooses. One way to mitigate this issue is to identify potentially problematic instances (by inspection or static analysis) and make the order deterministic by rewriting the expression as a sequence of assignment statements that compute the intermediate results. Alternatively, the potential nonportability can be eliminated completely by using the SPARK Ada subset: restrictions such as the prohibition of side effects in functions ensure that the value of an expression is the same, regardless of the compiler’s choice of evaluation order.

Parameter passing

Formal parameters to a subprogram in Ada are specified in terms of the direction of data flow:

“in,” from the caller to the called subprogram
“out,” from the called subprogram back to the caller when the subprogram returns
“in out,” from the caller to the called subprogram, and then from the called subprogram back to the caller when the subprogram returns

The compiler chooses whether a parameter is passed by copy or by reference. For certain classes of types – in particular, scalar types and access types (“pointers”) – the semantics of parameter passing is by copy. For some other classes of types the semantics is by reference. But for types that do not fall into these categories, the compiler can choose either strategy, generally using the type’s object size as the criterion. If the size of each object is smaller than some threshold value, then by copy is used, otherwise it will be by reference.

The potential functional portability issue is that the effect of the subprogram may depend on the compiler’s choice. This can occur through “aliasing” (e.g., a global variable is passed as a parameter to, and is also assigned from, the subprogram) or exception handling (a formal “out” or “in out” parameter is assigned from the subprogram, but an exception is propagated before the subprogram returns).

These implementation-dependent effects can be mitigated in several ways. The aliasing issue can be avoided by ensuring that a global variable is not passed as a parameter to a subprogram that can assign to the variable. Violations can be detected by code review/inspection or static analysis tools and are prevented in SPARK (which prohibits such aliasing).

The exception propagation issue can be avoided by appropriate programming style: deferring any assignment to the formal parameter until after it can be assured that exception propagation will not occur. This issue is completely avoided with SPARK, since the proof tools can demonstrate the absence of run-time exceptions.

References to uninitialized variables

The Ada language enables variables to be declared without initialization. Requiring initialization universally would be problematic: A sensible initial value might not exist, or the program logic might require initialization to be supplied by an external input at system startup. More subtly, default initialization can lead to a hard-to-detect programming error where a variable that needs to be explicitly initialized is referenced prematurely, yielding the default initialization that is valid for the variable’s type but incorrect.

Referencing a variable before it has been initialized is a programming error. In the absence of a guaranteed value, the Ada semantics leave the effect of such a reference undefined. Ensuring that variables are initialized before being referenced is outside the scope of the restrictions in the FACE Safety and Security capability sets, and thus needs to be enforced through other means.

Several Ada language features can help:

Some types require a default initialization. In particular when an access value (pointer) is declared without an explicit initialization, it will be set to the special value null. An attempt to dereference the null value raises an exception
The programmer can define default initial values for record fields
In Ada 2012 any scalar type can define a default initial value

In practice, references to uninitialized variables for other types are detected in many instances by the Ada compiler, especially at higher optimization levels where sophisticated flow analysis is used. Static-analysis tools can also address this issue while minimizing “false alarms.” And as with all the other potential nonportabilities discussed in this section, references to uninitialized variables are completely prevented in SPARK since they will be detected by the SPARK proof tools.

Concurrency

Ada has a powerful and high-level concurrency model, but in the interest of supporting a wide range of target environments the language enables a number of scheduling policy decisions to be determined by the implementation. This nondeterminism is mitigated by the Ravenscar profile, a simple, deterministic and efficient subset of the Ada tasking features. Both the FACE Safety-Extended and Safety-Base & Security capability sets restrict the Ada tasking facility to the Ravenscar subset and thus avoid the functional portability issues of the full tasking model. (The Ravenscar features are allowed in the Safety capability sets for Ada 95 in Edition 3.0 of the FACE Technical Standard, and for both Ada 95 and Ada 2012 in Edition 3.1.)

The Ravenscar subset is supported by SPARK, and thus a SPARK program will avoid the nondeterminism of the full Ada tasking model.

Elaboration order

An Ada program typically consists of a main subprogram together with the modules (“packages”) that the main subprogram depends on, directly or indirectly. Program execution first executes run-time code in the various dependent packages (for example to initialize global data) – known as “package elaboration” – then invokes the main subprogram. The order in which the packages are elaborated is partially constrained by language semantics but is generally implementation-dependent, with different orders possibly yielding different results. Implementation dependence is intrinsic to the language semantics, since any attempt to completely specify the elaboration order would also prohibit useful cases such as interdependent packages.

Several techniques can help ensure portability:

Add appropriate pragmas to constrain the elaboration order (see Figure 1 for an example) or
Avoid elaboration-time code in the dependent packages by moving all such code into procedures that are explicitly invoked at the start of the main subprogram

[Figure 1 | Elaboration order.]

Elaboration order nondeterminism can also be avoided by using SPARK, since the SPARK restrictions ensure that all elaboration orders have the same effect.

Guidance for target dependencies

System.* package hierarchy and representation clauses: Although low-level programming involves accessing target-specific characteristics, Ada helps to mitigate the nonportability through standard language features. The package System declares a type Address and associated operations, and the child packages System.Storage_Elements and System.Address_To_Access_Conversions offer standard facilities for dealing with “raw storage” and for treating a pointer as a physical address or vice versa. Representation clauses allow the program to define low-level properties of program entities, such as the layout of a record or the address of a variable. These features are permitted by the FACE Safety and Security capability sets. Although their usage is platform-specific, encapsulating such code in the bodies of packages will localize and help minimize the adaptation needed when porting the code to a new target platform.

Numeric type representation: The predefined numeric types in Ada (Integer, Float, etc.) have implementation-defined ranges/precisions. This situation can cause functional portability issues if the programmer implicitly assumes that a type such as Integer always has some minimum range; an arithmetic expression may overflow and raise an exception when the code is ported to a platform where Integer has a narrower range.

The potential nonportability can be avoided by declaring custom numeric types instead of using the predefined types. Figure 2 shows an example.

[Figure 2 | Portable numeric type.]

Follow usage patterns

Writing fully portable code requires not only FACE conformance but also functional portability. That means following appropriate usage patterns, especially for features whose semantics are not completely defined by the language standard.

Ada is, in general, a language with strong support for functional portability, and over the years system modernizations have successfully ported large Ada programs to new hardware and new compiler implementations. Nonetheless, functional portability does not come automatically, it must be planned for; developers should either avoid language features that are implementation-dependent or else take appropriate mitigation measures. This is especially important for applications that need to adhere to one of the FACE Safety and Security capability sets/profiles. Such applications have strong assurance requirements, which are difficult to demonstrate if the code uses language features that are not precisely defined. The SPARK subset of Ada is particularly relevant, since the SPARK language restrictions ensure deterministic semantics.

In brief, adopting appropriate stylistic conventions for Ada (most of which can be enforced by static analysis tools such as AdaCore’s CodePeer or GNATcheck) or using SPARK can help developers achieve full portability for their FACE-conformant software while also realizing the assurance benefits that Ada and SPARK bring.

Dr. Benjamin Brosgol is a senior member of the technical staff at AdaCore. He has been involved with programming language design and implementation throughout his career, concentrating on languages and technologies for high-assurance systems with a focus on Ada and safety certification (DO-178B/C). Dr. Brosgol is Vice Chair of The Open Group FACE Consortium’s Technical Working Group. Readers may reach him at [email protected].

AdaCore • www.adacore.com