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 |
| 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 |