It has been mentioned several times already in this book that real-time programming represents a major application area for Ada, and particularly for Ada tasking. The Real-Time Systems Annex specifies additional characteristics of the language that facilitate the programming of embedded and real-time systems. If an implementation supports the Real-Time Systems Annex then it must also support the Systems Programming Annex (see previous chapter). All issues discussed in the Real-Time Systems Annex affect the tasking facilities of the language. They can be grouped together into the following topics.

• Time and clocks – introduced in Chapter 1.

• Scheduling – how to allocate system resources, in particular the processor.

• Resource control – how to monitor and manage the use of the processor by individual tasks or groups of tasks.

• Optimisations and restrictions – specifically the Ravenscar profile.

All of these topics are discussed in this and the next two chapters; starting with the important issue of scheduling.

Scheduling

The functional correctness of a concurrent program should not depend on the exact order in which tasks are executed. It may be necessary to prove that the non-determinism of such programs cannot lead to deadlock or livelock (that is, progress is always taking place), but it is not necessary to program the order in which all actions must occur explicitly.

Designing, implementing and maintaining software for large systems is a non-trivial exercise and one which is fraught with difficulties. These difficulties relate to the management of the software production process itself, as well as to the size and complexity of the software components. Ada is a mature general-purpose programming language that has been designed to address the needs of large-scale system development, especially in the embedded systems domain. A major aspect of the language, and the one that is described comprehensively in this book, is its support for concurrent and real-time programming.

Ada has evolved over the last thirty years from an object-based concurrent programming language into a flexible concurrent and distributed object-oriented language that is well suited for high-reliability, long-lived applications. It has been particularly successful in high-integrity areas such as air traffic control, space systems, railway signalling, and both the civil and military avionics domains. Ada success is due to a number of factors including the following.

• Hierarchical libraries and other facilities that support large-scale software development.

• Strong compile-time type checking.

• Safe object-oriented programming facilities.

• Language-level support for concurrent programming.

• A coherent approach to real-time systems development.

• High-performance implementations.

• Well-defined subsetting mechanisms, and in particular the SPARK subset for formal verification.

The development and standardisation of Ada have progressed through a number of definitions, the main ones being Ada 83 and Ada 95. Ada 2005 now builds on this success and introduces a relatively small number of language changes to provide:

• Better support for multiple inheritance through the addition of Java-like interfaces.

• Better support for OO style of programming by use of the Object.Operator notation.

• […]

In this chapter we look at type systems for the language aPi. The traditional view of types is that they provide an aid to programmers to avoid runtime errors during the execution of programs. We start with this view, explaining what runtime errors might occur during the execution of aPi processes, and design a type system that eliminates the possibility of such errors.

We then modify the set of types, so that they implement a more subtle notion of resource access control. Here the resources are simply channels, and the more subtle type system enables access to these resources to be managed; that is read and write accesses can be controlled. The view taken is that one no longer programs directly with resource names. Instead programming is in terms of capabilities on these names, the ability to read to or write from a particular resource. These capabilities are managed by the owners of resources and may be selectively distributed to be used by other processes.

Runtime errors

The traditional use of types and type checking is to eliminate runtime errors in highlevel programs. Specifically types are annotations inserted into the program text by the program designer, or inferred automatically by a type inference system, which indicate the intended use of various resources. Then prior to execution the annotated program is typechecked, that is syntactically analysed, to ensure that the behaviour of the program will indeed respect the intended use of these resources.

From ATM machines dispensing cash from our bank accounts, to online shopping websites, interactive systems permeate our everyday life. The underlying technology to support these systems, both hardware and software, is well advanced. However design principles and techniques for assuring their correct behaviour are at a much more primitive stage.

The provision of solid foundations for such activities, mathematical models of system behaviour and associated reasoning tools, has been a central theme of theoretical computer science over the last two decades. One approach has been the design of formal calculi in which the fundamental concepts underlying interactive systems can be described, and studied. The most obvious analogy is the use of the λ-calculus as a simple model for the study of sequential computation, or indeed the study of sequential programming languages. CCS (a Calculus for Communicating Systems) [28] was perhaps the first calculus proposed for the study of interactive systems, and was followed by numerous variations. This calculus consists of:

• A simple formal language for describing systems in terms of their structure; how they are constructed from individual, but interconnected, components.

• A semantic theory that seeks to understand the behaviour of systems described in the language, in terms of their ability to interact with users.

Here a system consists of a finite number of independent processes that intercommunicate using a fixed set of named communication channels. This set of channels constitutes a connection topology through which all communication takes place; it includes both communication between system components, and between the system and its users.

Throughout the book we will make extensive use of both induction and coinduction, and their associated proof techniques. Here we give a brief review of these concepts, and an indication of how we intend to use them.

Induction

Figure 1.1 contains a definition of the (abstract) syntax of a simple language of machines. Here a ranges over some set of action labels Act, and intuitively a machine can carry out sequences of these actions, and periodically has a choice of which actions to perform. Let M be the set of all machines defined in Figure 1.1. Formally this is an inductive definition of a set, namely the least set S that satisfies

• stop ∈ S

• M ∈ S implies a.M ∈ S for every action label a in Act

• M1, M2 ∈ S implies M1 + M2 ∈ S.

The fact that M is the least set that satisfies these conditions gives us a proof technique for defining and proving properties of machines in M; any other set satisfying the conditions is guaranteed to contain M.

As an example consider the following definition of the size of a machine:

• |stop| = 0

• |a.M| = 1 + |M|

• |M1 + M2| = |M1| + |M2|.

We know by induction that this function is now defined for every machine. Belabouring the point for emphasis let D be the domain of the size function | |, the set of elements for which it is defined.

Here we describe a simple language in which values are exchanged between concurrent processes via communication channels. These channels can be used to model resources and the syntax allows them to be declared as private, for the exclusive shared use of specific processes. The names of these channels/resources can also be transmitted between processes, resulting in a very powerful descriptive language.

We give two different views of the language. The first, via a reduction semantics, describes how processes may evolve. This may be seen as a specification of an interpreter for the language and is taken to be the primary semantic definition. The second view is an action semantics, which describes how processes can interact with other processes, perhaps as part of a larger system; this describes how processes can behave as part of a larger endeavour. This second view interprets the language as a labelled transition system or lts, as explained in Definition 1.2, and thus induces automatically a bisimulation equivalence between processes.

The language aPi

The syntax of the language aPi is given in Figure 2.1. It presupposes a set Names of names, ranged over by n,m, …, a, b, c … for communication channels or resources. We also use a set Vars of variables, place-holders for values that can be transmitted via the communication channels. These values will include some unspecified collection of base values such as integers, booleans, strings, etc., ranged over by bv, but more importantly channel names themselves.

In this chapter we apply the theory developed for aPi in Chapter 4 to aDpi. For technical reasons it is best to work relative to the extended typing system developed in Section 5.5, although to avoid unnecessary clutter we will abbreviate ⊢rc to simply ⊢.

The motivation for this theory, the relativisation of behavioural equivalences to the partial knowledge of observers as explained in Chapter 4, applies equally well, if not more so, in a distributed setting. Consequently it is not repeated here. Moreover the technical framework, developed in detail in Chapter 4, is easily adapted to aDpi. So we simply apply it, modifying the various concepts as necessary to the distributed setting, in what we hope is a natural manner.

In the first section we discuss distributed actions-in-context and the associated typed bisimulation equivalence, ≈bis, for aDpi systems. Most proofs of the expected properties of this equivalence are left to the reader as they can be easily constructed from the corresponding ones in Sections 4.1 and 4.2.

This is followed by a section on examples, which demonstrates that at least in principle standard bisimulation-based proof methodologies can be adapted to our setting. Necessarily there are more syntactic details to contend with; but in time appropriate software tools, based for example on theorem provers, could be developed to partially alleviate the tedium.

In the final section we revisit the subject first broached in the untyped setting of aDpi, in Section 2.5, namely the justification of our typed bisimulation equivalence for aDpi.