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 |