seL4

About CAmkES

CAmkES is a component-based software platform for seL4. It provides a software development and runtime platform that allows developers to design seL4-based systems as collections of interacting components.

Motivation

A microkernel-based multi-server operating system is designed as a set of protected and separated services that communicate with each other through interprocess communication mechanisms. Since these services are protected from each other by a combination of kernel and hardware protection, the resulting systems have the potential to be highly reliable and secure.

However, the design of such a system becomes increasingly difficult as the number of services and the complexity of their interconnection grows. They become particularly difficult to build and maintain when there is no explicit specification of how the services should and do interoperate. By making the interactions between these services explicit, a component-based software engineering approach reduces this complexity for the developer and makes the design and implementation of complex microkernel-based systems feasible.

Component-Based Software Engineering

Component-Based Software Engineering (CBSE) is a software development approach that is based on the decomposition of a system into a set of interconnected software components.

A software component is a system element offering a predefined service through well-defined interfaces. Software components are similar to objects in the object-oriented paradigm in that they encapsulate their state so that it is not visible or directly accessible from outside the component. However, components are typically more coarse-grained, and of a higher abstraction level, than objects, and have stricter requirements regarding their interfaces. In particular, besides defining the interfaces they provide, they also define interfaces they use, that is, the interfaces of other components they rely on. A key feature of software components is that they are meant to be reusable and should be designed and implemented such that they can be used in many different systems.

Components are connected to each other using connectors, which are system elements that explicitly connect corresponding interfaces of communicating components. Connectors implement the glue code that binds components together, and they are the only parts of the system that need to explicitly use underlying system mechanisms (such as IPC, capabilities, etc.). A set of components and the connections between them form a system architecture which is commonly referred to as a component system or architecture.

The details of how components, component interfaces, and component architectures are specified are defined by a component model. The features of a component model determine the flexibility and power of a particular CBSE-based approach.

A component platform implements a component model, providing tools and support software for building components and component-based systems according to that model. (Note that terminology varies and there is some overlap: in particular what we call a component platform is sometimes called a component framework, a component architecture or a component system.)

Key Properties of CAmkES

A minimal core model

The core of the CAmkES model provides the minimum functionality required to build static componentised systems. The functionality provided by the core model includes: specification of RPC, event, and dataport interfaces, specification of components, and specification of connectors.

Static

CAmkES is a static system. This means that all the component instances and their connections must be defined in the system architecture specification. Furthermore, at startup time, all components and connections are created by the system initialiser before the system starts running.

Explicit interactions

In a componentised system making communication between components explicit is critical to providing reusable components. This means that components interact with the rest of the system only via well-defined interfaces. As such all communication (including communication through shared data) is explicit in a CAmkES system architecture.

Explicit connectors

Furthermore, in CAmkES we have identified that communication between components is a critical part of a reliable and high performance system. As a result, the connectors that implement communication in our model are first-class entities. This means that system developers may choose which connectors to use when connecting software components and may also define and implement their own connectors. Furthermore connectors can be defined, implemented, and reused by system programmers just like components. We call these user-defined connectors.

Low overhead

CAmkES has a minimal, static, core, which makes it possible for us to limit the overhead introduced by a component-based design. The flexibility provided by user-defined connectors allows us to further optimise systems based on their specific requirements.

Optimisability

Given that all communication between components is explicit, and that the system developer can influence how that communication takes place, CAmkES provides a lot of space for system-specific optimisations. Such optimisations can range from a reorganisation of the system architecture for improved performance based on known best practices or patterns, to a system specific implementation of connectors and key components that takes advantage of system specific behaviour to optimise performance hot-spots. This allows system designers to focus on building systems that combine good software engineering practices with high performance.

The CAmkES component model

A CAmkES-based system is designed as a set of component instances connected together by connections. CAmkES component instances represent the system services and are ultimately implemented as isolated seL4 address spaces. CAmkES connections represent the communication channels and are implemented using appropriate seL4 IPC mechanisms including synchronous IPC, asynchronous notifications, and shared memory sections.

Component

A component is an encapsulation of functionality (similar to an object in object-oriented programming, however, more coarse grained). A component explicitly defines its interaction points with other components. It specifies which interfaces it makes available to others, and which interfaces it expects to use from other.

Interface

An interface specifies the kind of interaction possible between components. CAmkES provides three classes of interfaces:

An interface type declaration specifies a specific type of interface and the properties it has. A procedure interface type declaration specifies procedures (or methods) and their parameters and return types. A procedure interface type is specified in IDL (interface definition language). An event interface type declaration specifies an event type. A dataport interface type specifies the type of data to be shared. Dataport interface types are specified in C.

Interface Instance

A component definition specifies what interfaces an instance of that component makes available to others and what interfaces it expects to use from others. Interaction between component instances is performed on the their interface instances. Each such interface instance has a single interface type. An interface instance usually has a direction associated with it. For procedure interfaces, the direction is either uses, which means that interface instance can be used to access an implementation of it provided by another component, or provides, which means that the interface instance is implemented by that component. For an event, the direction is either emits, which means that the interface instance can be used to sends a event out to another component instance, or consumes, which means that the interface instance will receive events. Dataport instances do not specify directions.

Connector

A connector describes how component instances are connected together.
A connector defines how the communication between components takes place and what underlying mechanisms will be used to implement the connection. A connector type must specify the types of interfaces that it will connect.

Assembly

An assembly encapsulates a component system description. An assembly can be thought of as a complete description of a full system. Within the context of a system there can only be one assembly.

Composition

A composition is one part of an assembly and defines the component and connector instances that form a system.

Component Instance

A component instance is an instantiation of a component type. It is an actual component that will exist in the system. There can be multiple instances of a single component type. A component instance is typically (but not necessarily) implemented as an isolated seL4 address space. A component instance typically also has several seL4 threads associated with it.

Connection

A connection is an instantiation of a connector type and represents an actual communication channel between component instances. Component instances are connected at their interface instances, thus, in order for component instances to be able to communicate with each other, their interface instances must by connected by a connection. A connection is implemented using appropriate underlying kernel mechanisms.

Configuration

A configuration is another part of an assembly and describes system settings. The settings are represented as assignments of values to attributes belonging to specific component or connector instances.
These attributes are extra data of an arbitrary type associated with components and connectors. The description of a component or connector type must describe the name of the attribute and its type. The value of the attribute itself is unspecified. It is assigned when the entity is instantiated, and this assignment is referred to as a setting. Attributes are generally used to specialise or differentiate a component at runtime.

The CAmkES platform

The CAmkES platform provides:

ADL

An architecture description language to define components and system architectures.

IDL

An interface definition language to define component interfaces. CAmkES uses an IDL inspired by CORBA’s OMG IDL.

ADL and IDL compiler

The core of CAmkES is a tool that generates all required scaffolding and glue code from system ADL and IDL descriptions. This generated code deals with all aspects of seL4 initialisation, capability management, resource management, and inter-process communication. Developers of CAmkES-based systems do not interact with seL4’s base API directly.

The CAmkES compiler is template-based; the code to be generated is defined as templates that are expanded based on the system being built. This means that developers can easily adapt the generated code to either extend or specialise its functionality. Furthermore, CAmkES is extensible through its support for user-defined connectors, which allow developers to add system-specific functionality without having to modify the core tool.

Templates

CAmkES provides all the necessary templates required to generate code for seL4-based systems. It also provides alternate implementations for some templates that leverage specific seL4 features that may lead to better performance. We are also developing templates that allow CAmkES to target non-seL4 systems.

seL4 build system integration

CAmkES is fully integrated into the seL4 build system, and uses the same Kbuild-based build process. CAmkES systems are easy to configure and build along with the seL4 kernel and required libraries.

Development with CAmkES

In designing a CAmkES system a developer first decides on the components needed. These can either be pre-existing reusable components, or may need to be custom-built for the desired system. Components are usually designed so that they are reusable in different systems, enabling rapid development of systems from libraries of reusable software components.

When designing and building components a developer first defines the interfaces that the components will provide. The interfaces are defined in an interface definition language (IDL).

The developer then defines the component by specifying the interfaces provided by the component and the interfaces used by the component. This is done using an architecture description language (ADL). The actual functionality of the component is provided as C source code.

Once all the components have been chosen and defined, the developer then defines the system architecture, i.e., how all the components will be connected together. This architecture is described using the ADL and specifies all the components used, the connections between them, and the connectors used for the connections.

The developer then invokes the build system, which analyses the ADL descriptions, generates appropriate runtime and glue code, and compiles and links this together with the component and connector code to produce appropriate seL4 server images.

The build system then then further combines these images with the seL4 kernel and a system initialisation server to produce a final bootable system image.

Finally, the image can be run on the desired hardware or emulator.