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 maintainer wanted
Composition A container for the component and connector instantiations that form a system. Supported maintainer wanted
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 maintainer wanted
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 maintainer wanted
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. maintainer wanted
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. maintainer wanted
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 maintainer wanted
Component Interfaces An abstract exposed interaction point of a component. The subcategories of interface are procedure, event and dataport. Supported maintainer wanted
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 maintainer wanted
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 maintainer wanted
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 maintainer wanted
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 maintainer wanted
Structured attributes Attribute types support struct- and array-like declarations that support bundling and variable length attribute definitions. Supported maintainer wanted
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 maintainer wanted
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 maintainer wanted
`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. maintainer wanted
Connector definitions A type of link between instances. A connector implements the transportation for the interfaces it is connected between. Supported. maintainer wanted
Connections An instantiation of a connector. Connections connect two or more instances together via their interfaces. Supported. maintainer wanted
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. maintainer wanted
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. maintainer wanted
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). maintainer wanted

Components

Example Applications

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

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

Camkes Connectors

Components Description Status Maintained by
seL4Ethdriver CAmkES connector which is used to connect clients to the Ethdriver component's procedure interface. Supported maintainer wanted
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 maintainer wanted
seL4GlobalAsync CAmkES connector which is used to make the underlying seL4 notification capability available to the consuming side of the Event interface. Supported maintainer wanted
seL4MessageQueue CAmkES connector which allows the sending and queueing of user-defined messages from one component to another. Supported maintainer wanted
seL4MultiSharedData CAmkES connector which allows multiple dataports to be connected to a single components and also provides multiplexed access across the dataports. Supported maintainer wanted
seL4RPCCallSignal CAmkES connector which bundles a procedure interface with an event interface. Supported maintainer wanted
seL4RPCDataport CAmkES connector which bundles a procedure interface with a dataport interface. Supported maintainer wanted
seL4RPCDataportSignal CAmkES connector which bundles a procedure interface, event interface, and a dataport interface. Supported maintainer wanted
seL4RPCOverMultiSharedData CAmkES connector which uses shared memory to transfer data instead of the IPC buffer for procedure interfaces. Supported maintainer wanted
seL4SharedDataWithCaps CAmkES connector which allocates a shared memory region between components and also exposes the underlying frame caps. Supported maintainer wanted
seL4VirtQueues CAmkES connector which initialises a virtqueue connection between two components. Supported maintainer wanted
seL4DirectCall Used for RPC interfaces between grouped components. Each call becomes a direct function call. Supported maintainer wanted
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 maintainer wanted
seL4NotificationBind Similar event connector to seL4Notification but the receiver has bound the Notification to its TCB. Supported maintainer wanted
seL4NotificationNative Similar event connector to seL4Notification but the receiver end can only call Poll or Wait on notification object. Supported maintainer wanted
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 maintainer wanted
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. maintainer wanted
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 maintainer wanted
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 maintainer wanted
seL4SharedData seL4 Dataport connector. Creates a shared memory connection between components. Supported maintainer wanted
seL4HardwareMMIO seL4 Dataport connector to MMIO region. Creates a MMIO mapping for device registers into a component. Supported maintainer wanted
seL4HardwareIOPort seL4 Procedure connector for x86 IOPorts. Provides functions for performing IOPort instructions via seL4 invocations. Supported maintainer wanted
seL4HardwareInterrupt seL4 event connector for hardware interrupts. Provides interface for polling or blocking on interrupts and also for acknowledging IRQs. Supported maintainer wanted
seL4IOAPICHardwareInterrupt seL4 event connector for IOAPIC hardware interrupts. Specialised connector for dealing with IOAPIC interrupts. Supported on x86 maintainer wanted

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. maintainer wanted
default.xml Camkes project manifest with all repositories pinned to last versions that passed all tests. Supported. This gets updated automatically by continuous integration. maintainer wanted

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) maintainer wanted
SIMULATION (BOOL) Try and use simulable features (Default: ON) maintainer wanted
RELEASE (BOOL) Performance optimized build (Default: OFF) maintainer wanted
PLATFORM (STRING) Platform to use (Default: x86_64) maintainer wanted