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.
CAmkES is an acronym for component architecture for microkernel-based embedded systems.
The correct spelling is CAmkES. But CAMKES, Camkes, and camkes are also acceptable. Cakems, Cakes, Cakmes, and other misspellings are not.
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.
Some people say k æ m k e s, some people say k æ m k i: s. Both are acceptable.
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.
No, only one CAmkES app can run at a time.
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:
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.
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.
Connections can only be defined at design time. They are created at runtime by the system initialiser. You cannot create new connections at runtime.
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.).
One option is to edit the templates found in
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.
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.
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.
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.
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.
epit app for an example.
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.
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
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.
Simply because we haven’t gotten around to it yet.
No. However, we are developing experimental support for Linux, and the eChronos RTOS.
Currently CAmkES only supports C as an output language.
The capDL tool is written in Haskell.
The CAmkES tool is written in Python.
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.
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/.
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.
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.
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.
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.