CAmkES is an acronym that stands for “Componentized Architecture for microkernel based Embedded Systems”. Within the architecture that CAmkES provides, is an architecture description language (ADL), a code generation tool, and a run time for the generated code. The ADL portion helps to set up seL4 mechanisms and abstract their usage away into a more natural usage. Basically, everything in the Initial Userspace Deep Dive section is taken care of for you.

• Pull in the capdl loader application
• Create your application directory. It should have the following files
  • Kbuild
  • Kconfig
  • Makefile
  • README.md (optional)
  • components/
  • include/
  • interfaces/
  • <app-name>.camkes (top level camkes file)

This file requires the following lines

apps-$(CONFIG_APP_<APP-NAME>) += <app-name>
<app-name>: <library list>

Here, the app name is defined in the $CONFIG variable and should be all caps, while the <app-name> can be lower case. It is IMPORTANT to make sure all references to <app-name> are spelled the same way. The <library-list> is the list of libraries that your app will need. It is generally okay to grab a list from one of the solutions in the tutorials to start with. Something like libsel4 libmuslc libsel4platsupport libsel4muslccamkes libsel4camkes libsel4sync libsel4debug should be okay. If you want to use the benchmarking features, add libsel4bench to the list.

This file determines how your options will appear when make menuconfig is run from the root of the project. The general layout would be similar to:

config APP_<APP_NAME>
    bool "The app description"
    default n
    help
        Some help text here

It is important to make sure the <APP_NAME> in this file and Kbuild are the same.

This is what is pulled in by the top-level Makefile in the root of the project. A general template would be similar to:

TARGETS := $(notdir ${SOURCE_DIR}).cdl
ADL := <app-name>.camkes

<component>_CFILES := \
    $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/<component>/src/*.c))
<component>_HFILES := \
    $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/include/*.h))

include ${PWD}/tools/camkes/camkes.mk

It is important to make sure the $ADL variable is set to your top-level camkes file and that you have make rules for all of the components in your project.

The README.md is optional but your team-mates and future self may thank you for some top-level documentation.

This is your top level camkes file. It generally imports the other components and links everything together inside an assembly block. Within the assembly block there is generally a composition block and a configuration block. The composition block instantiates components and connects their data ports or other connectors. The configuration block sets access to objects or other component attributes. In this simple templated example, two components of the same type are instantiated, they are connected via a seL4SharedData connection, and port access is set to make the connection one way.

import <std_connector.camkes>;

import "components/<component>/<component>.camkes";

assembly {
    composition {
        component <component> <component-instance-1>;
        component <component> <component-instance-2>;

        connection seL4SharedData shared_data(from <component-instance-1>.port, <component-instance-2>.port);
    }
    configuration {

        <component-instance-1>.port_access = "R";
        <component-instance-2>.port_access = "W";
    }
}

This is not an exhaustive template. For more CAmkES information consult the manual

Within the components directory there is a directory for each component definition. The directory layout would be similar to:

components/
└── <component-name>
    ├── <component-name>.camkes
    └── src
        ├── <component-src-file-1>.c
        └── <component-src-file-2>.c

The component definition in the <component-name>.camkes CAmkES file can be used in other files, like the top-level CAmkES file, to create instances of it and connect to other component instances.

An important CAmkES keyword is the control keyword. If this is included in a component’s definition, then that component will be considered “active” and the source code needs to include a run function. Inactive components, such as handlers and communication channels, run in a thread which loop and check for notifications that trigger user defined functions. A template for a simple component definition would be similar to:

import "../../interfaces/<an-interface>.camkes";

component <component-name> {
  include <some-header>.h
  control;
  uses <interface> <interface-instance>;
  dataport Buf port; // This was used in the top level camkes file
}

This component is an active component that is using an interface defined in an external CAmkES file and has a dataport to communicate with another component.

A source file for this component might look similar to:

#include <stdio.h>
#include <camkes.h>
#include <camkes/dataport.h>
 
int run (void) {
  printf("I can print from here!\n");
 
  // Copy to a dataport
  int *n = (int*)port;
  char *str = (char*)(port + 1);
  strcpy(str, "hello");
 
  return 0;
}

It is important to include the camkes.h since it is a generated header for this component. The CAmkES header files include the prototypes for the dataports and attributes that were defined for the component in the CAmkES files, so they are globals here. Another component’s source file won’t have the same CAmkES header file as this one, since they are generated and placed in the correct places during build time.

You can see the structure for the Buf CAmkES type in libsel4camkes/include/camkes/dataport.h.

/** \brief A convenience type for CAmkES dataports.
 *
 * The default dataport type in CAmkES is `Buf`, a generic type for a
 * page-sized shared memory region. While the user is provided with a typed
 * pointer, this should never be directly dereferenced. The only legal things
 * to do with a `Buf` are to call `sizeof` or cast a pointer to one to a
 * pointer of another type. E.g.
 *
 *     char my_buffer[sizeof(Buf)];
 *     strncpy(my_char, buf_ptr, sizeof(Buf));
 */
typedef struct Buf_ {
    char content[PAGE_SIZE_4K] DEPRECATED("Buf type incorrectly accessed directly");
} Buf;

The CAmkES dataports expand from jinja templates and can be seen in tools/camkes/camkes/templates/seL4SharedData-common.template.c.

This directory contains header files that might define structures that can be used in the component CAmkES definition and source files similar to how the Buf structure was used.

The interfaces directory contains other CAmkES building blocks for the other components in your application. These are commonly procedures blocks. A CAmkES component would generally import the CAmkES files in this directory.

A general procedure block would look similar to:

procedure <interface-name> {
  <return-type> <function-name> (<argument-direction> <argument-type> <argument-name>);
}

A CAmkES component needs to provide the interface for it to be used by another component:

component <provider-component-name> {
  provides <interface-name> <interface-instance-name>;
}

A CAmkES component can then use this interface similar to:

component <user-component-name>{
  uses <interface-name> <interface-instance-name>;
}

These two components need to be connected via a CAmkES provided connection. This is usually done in the top level CAmkES configuration block.

configuration {
  <provider-component-name> <provider-instance>;
  <user-component-name> <user-instance>;
  connection <connection-type> <connection-instance>(from <user-instance>.<interface-instance-name>, to <provider-instance>.<interface-instance-name>);
}

In the source of the procedure provider CAmkES component the functions would be implemented similar to:

<return-type> <interface-instance-name>_<function-name>(const <type-argument-mapping> <argument-name>)
{
    // Implementation
}

It is important to realize that the <interface-instance-name> is in relation to the component that it is associated with. The interface provider can also define a interface initialization function if its function signature is void <interface-instance-name>__init(void).

The component that uses this procedure can make calls to the interface similar to:

int run(void)
{
  <interface-instance-name>_<function_name>();
}

A possible usage would be to run utility functions such as printing over an RPC CAmkES connection. More can be found in the CAmkES manual.

The CAmkES parsing process generally goes as follows:

• Parses the CAmkES description file
• Fills in and expands templated code
• Uses the CapDL python tool to create the CapDL spec that the CAmkES project needs

If you would like to see more output while running make from the root of your project, set the verbosity level by setting the V environment variable and save to a text file for easier viewing:

V=3 make | tee makeoutput.txt

The developer does not really have to worry about the finer points of CapDL but they should be aware of what it is and how it fits into the build system.

• Capability Description Language
• A Data61 language used to take a description of capabiltiies and create the glue code and set up code to implement these capabilities
• The tool also provides the capdl-loader-app
  • This runs as the initial root thread that the seL4 kernel first drops down to
• Examples can be found in capdl/capDL-tool/example.cdl.
• The CapDL spec for your project should show up in build/$ARCH/$PLAT/$APP-NAME/$APP-NAME.cdl
• The CapDL usage is largely hidden from the user. The only necessary interaction is to select the capdl-loader-app in the menuconfig Applications list.