seL4

FAQ

What is CAmkES?

CAmkES is a component-based software development and runtime platform that allows seL4 systems to be modelled and implemented as a collection of interacting software components. See About CAmkES for more details.

What does CAmkES mean?

CAmkES is an acronym for component architecture for microkernel-based embedded systems.

What is the correct spelling of CAmkES?

The correct spelling is CAmkES. But CAMKES, Camkes, and camkes are also acceptable. Cakems, Cakes, Cakmes, and other misspellings are not.

Why does CAmkES have weird capitalisation?

CAmkES is an acronym, hence the capitals. However, the small mk emphasises the smallness of the microkernel. We decided on the capitalisation on a whim and it stuck. But it can get annoying to type correctly, so normally capitalised spellings are also acceptable.

What is the correct pronounciation of CAmkES?

Some people say k æ m k e s, some people say k æ m k i: s. Both are acceptable.

What is a CAmkES app?

A CAmkES app is another word for a CAmkES system, it consists of a graph of multiple interconnected components. Note that the components and connections in a single CAmkES app can form disconnected sub-graphs.

Can I run multiple CAmkES apps simultaneously?

No, only one CAmkES app can run at a time.

What does it mean that CAmkES is a static system?

It means that all the component instances and their connections must be defined at design time in ADL. Furthermore, when the system starts, all components and connections are created by the system initialiser before the system starts running. Practically this means:

Why is CAmkES a static system?

CAmkES is targeted at embedded systems and most embedded systems are static. This is so that the system size and behaviour can be determined at design and build time and will not vary at runtime. This way appropriate hardware can be provisioned and known to be sufficient.

Also, CAmkES is the key platform for developing high assurance systems on top of seL4, and verifying static systems is more feasible than verifying non-static systems. Note that this really means that only the verified parts should be static, whereas the unverified parts could be dynamic. CAmkES does not support such a system however.

How do I create a new component instance?

Component instances can only be defined at design time. They are created at runtime by the system initialiser. You cannot create new component instances at runtime once the CAmkES system has started running.

How do I create a new connection?

Connections can only be defined at design time. They are created at runtime by the system initialiser. You cannot create new connections at runtime.

What is glue code?

Glue code is the code that is generated to ‘glue’ components together.
It provides component scaffolding (i.e. the code that initialises the component instance, runs the appropriate threads, and manages the components resources) and connection code (i.e. code that marshals procedure parameters into message buffers, sends messages and notifications using seL4 endpoints, receives messages and endpoints on seL4 endpoints, unmarshals procedure parameters, invokes appropriate procedures, etc.).

How can I change the glue code generated?

One option is to edit the templates found in tools/camkes/camkes/templates.

If you only want to change code generated for connectors, another options is to create a user-defined connector. See the mutex app for an example of how to do this.

What is the relation between components and address spaces?

By default each component runs in a separate seL4 address space. We have experimental code to place multiple components in the same address space, however this has not been released yet.

What is the relation between components and seL4 threads?

Each component instance has several seL4 threads. There is one thread for each provides procedure interface instance and one thread for each consumes event interface instance. A control component also has a control thread. Each of these threads shares the same address space and cspace.

Can a CAmkES component invoke seL4 system calls directly?

No. Except for generated glue code, a CAmkES component’s code should not invoke seL4 system calls and manipulate seL4 caps. In reality, component code does have access to its cspace, so could invoke seL4 calls and manipulate capabilities. But this is frowned upon. If you find yourself needing to do this, then it might mean that the CAmkES glue code or model may need to be adapted.

Can I write device drivers in CAmkES?

Yes. CAmkES abstracts hardware access in virtual hardware components. These are components that pretend to be hardware and give a component connected to them access to the interrupts and memory regions required to access that hardware. Device drivers in CAmkES are simply components that connect to such virtual hardware components.
See the epit app for an example.

How much overhead does CAmkES add?

In terms of IPC performance, we’ve run experiments with optimised connectors and components that show effectively 0% overhead compared to a raw seL4 system with the same functionality.

Are components reusable?

Yes. However there is currently no support for a shared component repository. This means that to reuse a component you have to either copy the component (its component directory including .camkes and source files) or link to it. In the first case you can make changes in the copied component and these will not be reflected in the original or any other component, in the second case, changes will be reflected in the original and any other linked copies.

Why doesn’t CAmkES support a shared component repository?

Simply because we haven’t gotten around to it yet.

Does CAmkES support any other platforms other than seL4?

No. However, we are developing experimental support for Linux, and the eChronos RTOS.

What languages does CAmkES support?

Currently CAmkES only supports C as an output language.

Do I have to know to know C to develop for CAmkES?

Yes.

Why does CAmkES require Haskell?

The capDL tool is written in Haskell.

Do I have to know Haskell to develop for CAmkES?

No.

Why does CAmkES require Python?

The CAmkES tool is written in Python.

Do I have to know Python to develop for CAmkES?

Not if you only want to write CAmkES components.

Yes if you want to write or modify templates.

Yes if you want to modiy CAmkES itself.

What is Jinja2 and why does CAmkES use it?

It is a templating language. CAmkES relies on templates to generate glue code. It uses Jinja2 as the templating backend for this. If you want to write or modify templates, you should understand Jinja2. More information at http://jinja.pocoo.org/.

Is CAmkES verified?

No. However, Matthew Fernandez, one of the main CAmkES developers, is doing a PhD on generating verified glue code. See Matt’s PhD page for more information. As a result of Matt’s work, CAmkES does have a formally specified model and some support for generating Isabelle theory files.

CAmkES used to support OKL4, but now you say it doesn’t. What is the history of CAmkES?

Originally CAmkES was developed to support NICTA L4 and Iguana. Later it was ported to support OKL4 2.0 and then OKL4 3.0. It was then ported to support seL4. However the original version was quite complex, and it was hard to make significant changes to it, so eventually development stalled.

The current version has been completely rewritten from scratch (although some parts are inspired by the original version). It currently only supports seL4.

What is the CAmkES philosophy?

The main guiding principle in CAmkES is “don’t pay for what you don’t use”. This means that the CAmkES user should not be forced to use (and pay for, in terms of memory use or performance) features they do not use. While this is our guiding principle, CAmkES does stray from it sometimes.

The other guiding principle is flexibility for performance. Our goal is for CAmkES to add minimal overhead compared to non-CAmkES systems.
We believe that flexibility is essential for this, in particular the ability for developers to provide their own optimised connectors whenever possible.

What are plans for the future?

World domination.

Besides further development of components and addition of missing features, the main work being done on CAmkES is support for verification of glue code.

With regards to missing features, we are also working on better integration of virtualisation in the CAmkES model, a device driver framework, and support for zero-copy communication.