Camkes Project Status

This status page currently shows the status of CAmkES features and supplied components. The feature list currently only tracks features of the CAmkES Architecture Description Language. Other CAmkES features that are currently not tracked here include: Plugins, Templating engine, CAmkES component runtime environments, Procedure IDL interfaces, CDL refine verification, Tooling and VisualCamkes.

Features

Camkes Architecture Description Language (ADL)

Features of the CAmkES ADL are listed below. Features that are more experimental may not be compatible with the CDL-refinement CAmkES tooling. The Status field for each feature aims to indicate any known compatiblility issues related to a feature.

Features Description Status Maintained by
Assembly An assembly is a top level component system description. It contains a complete description of a full system. Supported Data61
Composition A container for the component and connector instantiations that form a system. Supported Data61
Configuration A container for describing settings. This is a syntactic element to hold the assignment of attributes for a given system.It is expressed inside an assembly block. Supported Data61
Component definition A `type` of functional entity. 'Component' is used colloquially to refer to both types and instances, but in a formal sense 'component' refers only to the type. Supported Data61
Hierarchical components A component can contain its own composition and configuration sections that can define components and connections that are in a different namespace from the toplevel composition and configuration namespaces. Each component instance is still a separate component. The top level component type can then select internal interfaces to export as its own interfaces. Mostly supported. There are some known template bugs where a component exporting dataport interfaces is also required to have a connection to the dataport. Data61
Component Groups A `Group` combines components into a single underlying process so they share an address space. This can reduce communication costs due to reduced context switching requirements, but components in a group are required to mutually trust each other. Mostly supported. Connector implementations need to be aware that they are being used in a group component context. There are also issues with variable storage as some global variables will be defined for each component instance in the group, and threads that call across component boundaries may access incorrect variable instances. Data61
Hardware components A hardware component represents an interface to hardware in the form of a component. Declaring a component with the hardware keyword creates a hardware component. Supported Data61
Component Interfaces An abstract exposed interaction point of a component. The subcategories of interface are procedure, event and dataport. Supported Data61
Exported Interfaces An interface of a compound component that is not implemented by that component, but is an alias for internal instance’s interface. Supported Data61
Optional Interfaces Interfaces of components can be made optional using the `maybe` keyword. Optional interfaces do not need to be connected to any other interfaces. Supported Data61
Procedure IDL An interface with function call semantics use procedures which consist of a series of methods that can be invoked independently. Procedures are defined within the ADL which has a IDL subset for defining methods and parameters. Supported Data61
Attributes An attribute is a configuration option that can be set on a component, connection or procedure definition. It is used to pass configuration information through to the underlying implementations. Supported Data61
Structured attributes Attribute types support struct- and array-like declarations that support bundling and variable length attribute definitions. Supported Data61
Default attribute values Attribute definitions can also provide default settings. These defaults are used in the absence attribute settings. Supported for component and connection attributes Data61
Synchronization Primitives CAmkES provides three primitives for intra-component mutual exclusion and synchronization. Mutexes, semaphores, and binary semaphores are declared similarly to attributes of a component definition. Supported Data61
`include` statements `include` statements are used to declare source language include dependencies on component and procedure definitions. These are used when CAmkES is using types defined by another language. Supported, but only used with C header files. Data61
Connector definitions A type of link between instances. A connector implements the transportation for the interfaces it is connected between. Supported. Data61
Connections An instantiation of a connector. Connections connect two or more instances together via their interfaces. Supported. Data61
Imports `import` statements are used to define an assembly over multiple `.camkes` files and combine them together into a single AST. Supported. It is possible to provide an import path argument to the camkes tool for where to search for files to import. Data61
C-Preprocessed ADL files The C Preprocessor is run over the ADL files before the parser starts parsing them. Supported. Because of the C-Preprocessor, the ADL ignores lines starting with #. This is not a valid comment syntax. Data61
Query syntax and plugins The parser supports adding plugins that can provide configuration values via a setting querying syntax. A plugin is able to respond to a query with a valid configuration value. Supported. Currently only 1 plugin exists, fdtQueryEngine, for querying values out of a Flattened device tree (FDT). Data61

Components

Example Applications

Components Description Status Maintained by
adder A simple 'Hello world' CAmkES application which demonstrates some basics of the CAmkES framework. Supported Data61
aeroplage A CAmkES application which implements a prototype of a previous multi-level terminal for seL4. Supported Data61
alignment A CAmkES application which tests if the stack is aligned properly by crashing on an unaligned stack. Supported Data61
attributes A CAmkES application which demonstrates the use of aliasing attributes. Supported Data61
binary-semaphore A CAmkES application which demonstrates how to use a binary semaphore to turn an asynchronous interface into a synchronous one. Supported Data61
cakeml_hello A 'Hello world' CAmkES application which demonstrates the ability to run CakeML-based CAmkES components inside CAmkES. Supported Data61
cakeml_regex A CAmkES application which demonstrates the use of CakeML to implement a CAmkES component which filters data between two different components. Supported Data61
cakeml_tipc A CAmkES application which demonstrates the Transparent IPC protocol (TIPC) and the use of CakeML to implement a CAmkES component to filter data between two different CAmkES components. Supported Data61
cms-donate A CAmkES application which demonstrates the donation of a scheduling context between a client and server via an intermediary under a Mixed Criticality Scheduling (MCS) environment. Supported Data61
cs-donate A CAmkES application which demonstrates the donation of a scheduling context between a client and server under a Mixed Criticality Scheduling (MCS) environment. Supported Data61
cs-nodonate A CAmkES application which demonstrates two CAmkES components running using their own scheduling contexts under a Mixed Criticality Scheduling (MCS) environment. Supported Data61
dataport A CAmkES application which demonstrates an example of the usage of CAmkES dataports. Supported Data61
debug-simple A CAmkES application which demonstrates the use of the seL4GDB connector to debug CAmkES components. Supported Data61
dhcp A CAmkES application which demonstrates an example DHCP server. Supported Data61
dma-example A CAmkES application which demonstrates the use of a CAmKES-allocated DMA pool. Supported Data61
epit A CAmkES application which demonstrates a simple hardware driver CAmkES component for the EPIT timers on the KZM platform. Supported Data61
event A CAmkES application which demonstrates an example of CAmkES events. Supported Data61
event-driven A CAmkES application which demonstrates an example of a CAmkES event-driven application. Supported Data61
exchangestring A CAmkES application which demonstrates how to pass string arguments between CAmkES components. Supported Data61
fdtgen A CAmkES application which demonstrates an example on how to include a DTB blob and how to modify it. Supported Data61
filter A CAmkES application which demonstrates the use of a CAmkES component to filter communication between two other CAmkES components. Supported Data61
global-imports A CAmkES application which demonstrates an example of allowing CAmkES components to be globally imported using specific CMake macros. Supported Data61
hellorust A CAmkES application which demonstrates an example of running a Rust application inside CAmkES. Supported Data61
hierarchical-attributes A CAmkES application which demonstrates an example of hierarchical attributes in CAmKES. Supported Data61
hierarchical-components A CAmkES application which demonstrates an example of hierarhical CAmkES components in CAmkES. Supported Data61
keyboard A CAmkES application which demonstrates an example keyboard driver for x86 platforms. Supported Data61
lockserver A CAmkES application which demonstrates an example system which contains a CAmkES component that manages a lock. Supported Data61
mcs-donate A CAmkES application which demonstrates the donation of scheduling contexts betwen two clients and a server under a Mixed Criticality Scheduling (MCS) environment. Supported Data61
mcs-nodonate A CAmkES application which demonstrates the three CAmkES components running using their own scheduling contexts under a Mixed Criticality Scheduling (MCS) environment. Supported Data61
multiassembly A CAmkES application which demonstrates the ability to have two different 'assembly' blocks. Supported Data61
multiclient A CAmkES application which demonstrates the ability to allow multiple clients to share one connection. Supported Data61
multiplier A CAmkES application which demonstrates an example of using arrays as arguments for RPC functions between CAmkES components. Supported Data61
mutex A CAmkES application which demonstrates the use of user-defined connectors in CAmkES to implement a lock. Supported Data61
periodic A CAmkES application which demonstrates the periodic timeslices of CAmkES components under a Mixed Criticality Scheduling (MCS) environment. Supported Data61
picoserver A CAmkES application which demonstrates a simple networking example which uses the PicoServer in the global-components repository. Supported Data61
pit A CAmkES application which demonstrates a timer driver CAmkES component for the Programmable Interval Timer on x86 platforms. Supported Data61
reversestring A CAmkES application which demonstrates dataport release and acquire semantics. Supported Data61
rotate A CAmkES application which demonstrates the use of user-defined types as arguments of a RPC interface. Supported Data61
RPCOverMultiSharedData A CAmkES application which demonstrates the use of the seL4RPCOverMultiSharedData connector to perform RPC using shared memory buffers between the client and server. Supported Data61
rumprun_ethernet A CAmkES application which demonstrates a single TCP echo program that runs in a Rumprun unikernel instance on CAmkES. Supported Data61
rumprun_pthreads A CAmKES application which demonstrates a simple pthreads program that runs in a Rumprun unikernel instance on CAmKES. Supported Data61
rumprun_rust A CAmkES application which demonstrates a simple Rust 'Hello world' program that runs in a Rumprun unikernel instance on CAmkES. Supported Data61
serialserver A CAmkES application which demonstrates the use of the SerialServer component in the global-components repository. Supported Data61
serialserver_loopback A CAmkES application which demonstrates the use of the SerialServer component in the global-components repository looping back characters that it reads in from the serial device. Supported Data61
simple A CAmkES application which demonstrates an example of a CAmkES RPC connection. Supported Data61
simplesingleaddressspace A CAmkES application which demonstrates an example of a single address space CAmkES system which contains a RPC connection between its two components. Supported Data61
socket A CAmkES application which demonstrates a user-defined dataport. Supported Data61
structs A CAmkES application which demonstrates the use of structs and arrays for CAmkES component attribute types. Supported Data61
swapcounter A CAmkES application which was used for demonstration purposes for a paper submission to Formal Methods 2015 but has since been modified. Supported Data61
terminal A CAmkES application which serves as a prototype for a secure terminal system. Supported Data61
testbufvariant A CAmkES application which is used to test dataports. Supported Data61
testcamkes438 A CAmkES application that is used to test a specific function of the CAmkES framework. Supported Data61
testcontrolname A CAmkES application that is used to test if interfaces could be named with a particular suffix. Supported Data61
testdataportbifurcate A CAmkES application that tests if we can have multiple dataports within a single component that maps to the same underlying physical memory. Supported Data61
testdataportmux A CAmkES application that tests the ability to have multiple CAmkES components connected to the same dataport. Supported Data61
testdataportmuxflat A CAmkES application that tests the ability to have N-to-M dataport connections in a single address space. Supported Data61
testdataportptrwrap A CAmkES application that tests if dataport pointer wrapping and unwrapping functionality works on multiplexed dataports. Supported Data61
testdataportrpc A CAmkES application that tests if we can back an seL4RPCCall connection with various types of dataports. Supported Data61
testfaulthandlers A CAmkES application that tests if the fault handlers work correctly as intended. Supported Data61
testgrouping A CAmkES application which tests for the various edge cases in grouping CAmkES components into single address spaces. Supported Data61
testgroupingcontrol A CAmkES application which tests whether CAmkES components with a control thread work correctly when grouped in a single address spaces. Supported Data61
testhardwareinterrupt A CAmkES application which tests if an application containing a seL4HardwareInterrupt successfully compiles. Supported Data61
testhwdataportlrgpages A CAmkES application which tests whether or not large pages will be used to back a large dataport. Supported Data61
testnto1mmio A CAmkES application that tests if an N-to-1 MMIO connection to a piece of hardware functions correctly. Supported Data61
testnto1overload A CAmKES application that tests if N-to-1 connections involving multiple ends from a single CAmkES component uses distinct caps. Supported Data61
testrefin A CAmKES application that tests the 'refin' parameter function in CAmkES procedure interfaces. Supported Data61
testreplycapprotection A CAmkES application that tests the reply cap protection functionality. Supported Data61
testsel4notification A CAmkES application that tests the seL4Notification connector. Supported Data61
testsingleaddressspaceheap A CAmkES application that tests that the heaps of CAmkES components that share a single address space do not overlap. Supported Data61
teststringarrays A CAmkES application that tests some unusual usages of string array parameters in procedure interfaces. Supported Data61
testsyscalls A CAmkES application that serves as a testing sandbox for POSIX syscall functionality on CAmkES. Supported Data61
testunderscorename A CAmkES application that tests if CAmkES components can have interface names prefixed with an underscore. Supported Data61
timeserver A CAmkES application which demonstrates the use of the TimeServer componen fromthe global-components repository. Supported Data61
uart A CAmkES application which demonstrates a UART driver CAmkES component for the KZM platform. Supported Data61
uart_cogent A CAmkES application which demonstrates a prototype UART driver for the sabrelite platform that is written in Cogent. Supported Data61
vgatest A CAmkES application which demonstrates a minimal implementation for a text mode VGA terminal. Supported Data61

Reusable components

Components Description Status Maintained by
ClockServer A CAmkES component which abstracts over and multiplexes client accesses to clock devices on a platform. Supported Data61
Ethdriver A CAmkES component which abstracts over and multiplexes client accesses to an Ethernet device. Supported Data61
FileServer A CAmkES component which abstracts over and multiplexes client accesses to a CPIO-based file system. Supported Data61
GPIOMUXServer A CAmkES component which abstracts over and multiplexes client accesses to a GPIO and pin multiplexer controller. Supported Data61
PCIConfigIO A CAmkES component which abstracts over and multiplexes client accesses to the PCI configuration space of a platform. Supported Data61
PicoServer A CAmkES component which abstracts over and multiplexes client accesses to an IP stack, specifically, the PicoTCP TCP/IP stack. Supported Data61
ResetServer A CAmkES component which abstracts over and multiplexes client accesses to a reset line controller. Supported Data61
RTC A CAmkES component which abstracts over and multiplexes client accesses to a real-time clock device. Supported Data61
SerialServer A CAmkES component which abstracts over and multiplexes client accesses to a serial device. Supported Data61
TimeServer A CAmkES component which abstracts over and multiplexes client accesses to a timer device. Supported Data61
VirtQueue A stub CAmkES component which is used to help initialise virtqueue connections. Supported Data61
Serial Stub hardware CAmkES component that abstracts over a pc99-based serial device. Supported Data61
PIT Stub hardware CAmkES component that abstracts over the x86 Programmable Interval Timer. Supported Data61

Camkes Connectors

Components Description Status Maintained by
seL4Ethdriver CAmkES connector which is used to connect clients to the Ethdriver component's procedure interface. Supported Data61
seL4GlobalAsynchCallback CAmkES connector which is used to make the underlying seL4 notificationcapability available to the consuming side of the Event interface. This also allows the coupling of callback function that is called uponreceiving an Event. Supported Data61
seL4GlobalAsync CAmkES connector which is used to make the underlying seL4 notification capability available to the consuming side of the Event interface. Supported Data61
seL4MessageQueue CAmkES connector which allows the sending and queueing of user-defined messages from one component to another. Supported Data61
seL4MultiSharedData CAmkES connector which allows multiple dataports to be connected to a single components and also provides multiplexed access across the dataports. Supported Data61
seL4RPCCallSignal CAmkES connector which bundles a procedure interface with an event interface. Supported Data61
seL4RPCDataport CAmkES connector which bundles a procedure interface with a dataport interface. Supported Data61
seL4RPCDataportSignal CAmkES connector which bundles a procedure interface, event interface, and a dataport interface. Supported Data61
seL4RPCOverMultiSharedData CAmkES connector which uses shared memory to transfer data instead of the IPC buffer for procedure interfaces. Supported Data61
seL4SharedDataWithCaps CAmkES connector which allocates a shared memory region between components and also exposes the underlying frame caps. Supported Data61
seL4VirtQueues CAmkES connector which initialises a virtqueue connection between two components. Supported Data61
seL4DirectCall Used for RPC interfaces between grouped components. Each call becomes a direct function call. Supported Data61
seL4Notification Event connector where a seL4 Notification object is used for sending events. On the receiving end, a callback handler can be registerd or a thread can block waiting for events. Supported Data61
seL4NotificationBind Similar event connector to seL4Notification but the receiver has bound the Notification to its TCB. Supported Data61
seL4NotificationNative Similar event connector to seL4Notification but the receiver end can only call Poll or Wait on notification object. Supported Data61
seL4NotificationQueue seL4Endpoint object is used to queue notifications so that if the sender is sending faster than the receiver is receiving, unreceived events will accumulate in a counter. Supported Data61
seL4RPCCall Used for RPC interfaces where parameters will be marshalled into and out of IPC buffers and calls ocurr over seL4Endpoint objects. Supported. There is also a CakeML implementation for the receiving end. Data61
seL4DTBHardware Hardware connector to hardware component specified by a Device tree node. This will extract MMIO and potentially IRQ information for creating connections to the component. Supported Data61
seL4RPCCallNoType seL4 RPCCall connector but without requirement of single procedure interface. This allows a single receiver thread to handle multiple senders with different interfaces. Supported Data61
seL4SharedData seL4 Dataport connector. Creates a shared memory connection between components. Supported Data61
seL4HardwareMMIO seL4 Dataport connector to MMIO region. Creates a MMIO mapping for device registers into a component. Supported Data61
seL4HardwareIOPort seL4 Procedure connector for x86 IOPorts. Provides functions for performing IOPort instructions via seL4 invocations. Supported Data61
seL4HardwareInterrupt seL4 event connector for hardware interrupts. Provides interface for polling or blocking on interrupts and also for acknowledging IRQs. Supported Data61
seL4IOAPICHardwareInterrupt seL4 event connector for IOAPIC hardware interrupts. Specialised connector for dealing with IOAPIC interrupts. Supported on x86 Data61

Project manifests

Camkes project manifests

These manifests are available for checking out the example CAmkES applications.

Components Description Status Maintained by
master.xml Camkes project manifest with all repositories from master branches. Supported. Updated whenever project repository structure changes. Data61
default.xml Camkes project manifest with all repositories pinned to last versions that passed all tests. Supported. This gets updated automatically by continuous integration. Data61

Configurations

Camkes sample apps

The project containing all of the CAmkES example applications has a couple of configuration options for selecting the example app and seL4 platform it runs on.

Configurations Description Status Maintained by
CAMKES_APP (STRING) CAmkES application to build (Default: adder) Data61
SIMULATION (BOOL) Try and use simulable features (Default: ON) Data61
RELEASE (BOOL) Performance optimized build (Default: OFF) Data61
PLATFORM (STRING) Platform to use (Default: x86_64) Data61