CAmkES Components
Example Applications
Most of these examples can be found on the examples & demos page.
Components | Description |
---|---|
|
A simple ‘Hello world’ CAmkES application which demonstrates some basics of the CAmkES framework. |
|
A CAmkES application which implements a prototype of a previous multi-level terminal for seL4. |
|
A CAmkES application which tests if the stack is aligned properly by crashing on an unaligned stack. |
|
A CAmkES application which demonstrates the use of aliasing attributes. |
|
A CAmkES application which demonstrates how to use a binary semaphore to turn an asynchronous interface into a synchronous one. |
|
A ‘Hello world’ CAmkES application which demonstrates the ability to run CakeML-based CAmkES components inside CAmkES. |
|
A CAmkES application which demonstrates the use of CakeML to implement a CAmkES component which filters data between two different components. |
|
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. |
|
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. |
|
A CAmkES application which demonstrates the donation of a scheduling context between a client and server under a Mixed Criticality Scheduling (MCS) environment. |
|
A CAmkES application which demonstrates two CAmkES components running using their own scheduling contexts under a Mixed Criticality Scheduling (MCS) environment. |
|
A CAmkES application which demonstrates an example of the usage of CAmkES dataports. |
|
A CAmkES application which demonstrates the use of the seL4GDB connector to debug CAmkES components. |
|
A CAmkES application which demonstrates an example DHCP server. |
|
A CAmkES application which demonstrates the use of a CAmKES-allocated DMA pool. |
|
A CAmkES application which demonstrates a simple hardware driver CAmkES component for the EPIT timers on the KZM platform. |
|
A CAmkES application which demonstrates an example of CAmkES events. |
|
A CAmkES application which demonstrates an example of a CAmkES event-driven application. |
|
A CAmkES application which demonstrates how to pass string arguments between CAmkES components. |
|
A CAmkES application which demonstrates an example on how to include a DTB blob and how to modify it. |
|
A CAmkES application which demonstrates the use of a CAmkES component to filter communication between two other CAmkES components. |
|
A CAmkES application which demonstrates an example of allowing CAmkES components to be globally imported using specific CMake macros. |
|
A CAmkES application which demonstrates an example of running a Rust application inside CAmkES. |
|
A CAmkES application which demonstrates an example of hierarchical attributes in CAmKES. |
|
A CAmkES application which demonstrates an example of hierarhical CAmkES components in CAmkES. |
|
A CAmkES application which demonstrates an example keyboard driver for x86 platforms. |
|
A CAmkES application which demonstrates an example system which contains a CAmkES component that manages a lock. |
|
A CAmkES application which demonstrates the donation of scheduling contexts betwen two clients and a server under a Mixed Criticality Scheduling (MCS) environment. |
|
A CAmkES application which demonstrates the three CAmkES components running using their own scheduling contexts under a Mixed Criticality Scheduling (MCS) environment. |
|
A CAmkES application which demonstrates the ability to have two different ‘assembly’ blocks. |
|
A CAmkES application which demonstrates the ability to allow multiple clients to share one connection. |
|
A CAmkES application which demonstrates an example of using arrays as arguments for RPC functions between CAmkES components. |
|
A CAmkES application which demonstrates the use of user-defined connectors in CAmkES to implement a lock. |
|
A CAmkES application which demonstrates the periodic timeslices of CAmkES components under a Mixed Criticality Scheduling (MCS) environment. |
|
A CAmkES application which demonstrates a simple networking example which uses the PicoServer in the global-components repository. |
|
A CAmkES application which demonstrates a timer driver CAmkES component for the Programmable Interval Timer on x86 platforms. |
|
A CAmkES application which demonstrates dataport release and acquire semantics. |
|
A CAmkES application which demonstrates the use of user-defined types as arguments of a RPC interface. |
|
A CAmkES application which demonstrates the use of the seL4RPCOverMultiSharedData connector to perform RPC using shared memory buffers between the client and server. |
|
A CAmkES application which demonstrates a single TCP echo program that runs in a Rumprun unikernel instance on CAmkES. |
|
A CAmKES application which demonstrates a simple pthreads program that runs in a Rumprun unikernel instance on CAmKES. |
|
A CAmkES application which demonstrates a simple Rust ‘Hello world’ program that runs in a Rumprun unikernel instance on CAmkES. |
|
A CAmkES application which demonstrates the use of the SerialServer component in the global-components repository. |
|
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. |
|
A CAmkES application which demonstrates an example of a CAmkES RPC connection. |
|
A CAmkES application which demonstrates an example of a single address space CAmkES system which contains a RPC connection between its two components. |
|
A CAmkES application which demonstrates a user-defined dataport. |
|
A CAmkES application which demonstrates the use of structs and arrays for CAmkES component attribute types. |
|
A CAmkES application which was used for demonstration purposes for a paper submission to Formal Methods 2015 but has since been modified. |
|
A CAmkES application which serves as a prototype for a secure terminal system. |
|
A CAmkES application which is used to test dataports. |
|
A CAmkES application that is used to test a specific function of the CAmkES framework. |
|
A CAmkES application that is used to test if interfaces could be named with a particular suffix. |
|
A CAmkES application that tests if we can have multiple dataports within a single component that maps to the same underlying physical memory. |
|
A CAmkES application that tests the ability to have multiple CAmkES components connected to the same dataport. |
|
A CAmkES application that tests the ability to have N-to-M dataport connections in a single address space. |
|
A CAmkES application that tests if dataport pointer wrapping and unwrapping functionality works on multiplexed dataports. |
|
A CAmkES application that tests if we can back an seL4RPCCall connection with various types of dataports. |
|
A CAmkES application that tests if the fault handlers work correctly as intended. |
|
A CAmkES application which tests for the various edge cases in grouping CAmkES components into single address spaces. |
|
A CAmkES application which tests whether CAmkES components with a control thread work correctly when grouped in a single address spaces. |
|
A CAmkES application which tests if an application containing an seL4HardwareInterrupt successfully compiles. |
|
A CAmkES application which tests whether or not large pages will be used to back a large dataport. |
|
A CAmkES application that tests if an N-to-1 MMIO connection to a piece of hardware functions correctly. |
|
A CAmKES application that tests if N-to-1 connections involving multiple ends from a single CAmkES component uses distinct caps. |
|
A CAmKES application that tests the ‘refin’ parameter function in CAmkES procedure interfaces. |
|
A CAmkES application that tests the reply cap protection functionality. |
|
A CAmkES application that tests the seL4Notification connector. |
|
A CAmkES application that tests that the heaps of CAmkES components that share a single address space do not overlap. |
|
A CAmkES application that tests some unusual usages of string array parameters in procedure interfaces. |
|
A CAmkES application that serves as a testing sandbox for POSIX syscall functionality on CAmkES. |
|
A CAmkES application that tests if CAmkES components can have interface names prefixed with an underscore. |
|
A CAmkES application which demonstrates the use of the TimeServer componen fromthe global-components repository. |
|
A CAmkES application which demonstrates a UART driver CAmkES component for the KZM platform. |
|
A CAmkES application which demonstrates a minimal implementation for a text mode VGA terminal. |
adder
A simple ‘Hello world’ CAmkES application which demonstrates some basics of the CAmkES framework.
aeroplage
A CAmkES application which implements a prototype of a previous multi-level terminal for seL4.
alignment
A CAmkES application which tests if the stack is aligned properly by crashing on an unaligned stack.
attributes
A CAmkES application which demonstrates the use of aliasing attributes.
binary-semaphore
A CAmkES application which demonstrates how to use a binary semaphore to turn an asynchronous interface into a synchronous one.
cakeml_hello
A ‘Hello world’ CAmkES application which demonstrates the ability to run CakeML-based CAmkES components inside CAmkES.
cakeml_regex
A CAmkES application which demonstrates the use of CakeML to implement a CAmkES component which filters data between two different components.
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.
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.
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.
cs-nodonate
A CAmkES application which demonstrates two CAmkES components running using their own scheduling contexts under a Mixed Criticality Scheduling (MCS) environment.
dataport
A CAmkES application which demonstrates an example of the usage of CAmkES dataports.
debug-simple
A CAmkES application which demonstrates the use of the seL4GDB connector to debug CAmkES components.
dhcp
A CAmkES application which demonstrates an example DHCP server.
dma-example
A CAmkES application which demonstrates the use of a CAmKES-allocated DMA pool.
epit
A CAmkES application which demonstrates a simple hardware driver CAmkES component for the EPIT timers on the KZM platform.
event
A CAmkES application which demonstrates an example of CAmkES events.
event-driven
A CAmkES application which demonstrates an example of a CAmkES event-driven application.
exchangestring
A CAmkES application which demonstrates how to pass string arguments between CAmkES components.
fdtgen
A CAmkES application which demonstrates an example on how to include a DTB blob and how to modify it.
filter
A CAmkES application which demonstrates the use of a CAmkES component to filter communication between two other CAmkES components.
global-imports
A CAmkES application which demonstrates an example of allowing CAmkES components to be globally imported using specific CMake macros.
hellorust
A CAmkES application which demonstrates an example of running a Rust application inside CAmkES.
hierarchical-attributes
A CAmkES application which demonstrates an example of hierarchical attributes in CAmKES.
hierarchical-components
A CAmkES application which demonstrates an example of hierarhical CAmkES components in CAmkES.
keyboard
A CAmkES application which demonstrates an example keyboard driver for x86 platforms.
lockserver
A CAmkES application which demonstrates an example system which contains a CAmkES component that manages a lock.
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.
mcs-nodonate
A CAmkES application which demonstrates the three CAmkES components running using their own scheduling contexts under a Mixed Criticality Scheduling (MCS) environment.
multiassembly
A CAmkES application which demonstrates the ability to have two different ‘assembly’ blocks.
multiclient
A CAmkES application which demonstrates the ability to allow multiple clients to share one connection.
multiplier
A CAmkES application which demonstrates an example of using arrays as arguments for RPC functions between CAmkES components.
mutex
A CAmkES application which demonstrates the use of user-defined connectors in CAmkES to implement a lock.
periodic
A CAmkES application which demonstrates the periodic timeslices of CAmkES components under a Mixed Criticality Scheduling (MCS) environment.
picoserver
A CAmkES application which demonstrates a simple networking example which uses the PicoServer in the global-components repository.
pit
A CAmkES application which demonstrates a timer driver CAmkES component for the Programmable Interval Timer on x86 platforms.
reversestring
A CAmkES application which demonstrates dataport release and acquire semantics.
rotate
A CAmkES application which demonstrates the use of user-defined types as arguments of a RPC interface.
RPCOverMultiSharedData
A CAmkES application which demonstrates the use of the seL4RPCOverMultiSharedData connector to perform RPC using shared memory buffers between the client and server.
rumprun_ethernet
A CAmkES application which demonstrates a single TCP echo program that runs in a Rumprun unikernel instance on CAmkES.
rumprun_pthreads
A CAmKES application which demonstrates a simple pthreads program that runs in a Rumprun unikernel instance on CAmKES.
rumprun_rust
A CAmkES application which demonstrates a simple Rust ‘Hello world’ program that runs in a Rumprun unikernel instance on CAmkES.
serialserver
A CAmkES application which demonstrates the use of the SerialServer component in the global-components repository.
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.
simple
A CAmkES application which demonstrates an example of a CAmkES RPC connection.
simplesingleaddressspace
A CAmkES application which demonstrates an example of a single address space CAmkES system which contains a RPC connection between its two components.
socket
A CAmkES application which demonstrates a user-defined dataport.
structs
A CAmkES application which demonstrates the use of structs and arrays for CAmkES component attribute types.
swapcounter
A CAmkES application which was used for demonstration purposes for a paper submission to Formal Methods 2015 but has since been modified.
terminal
A CAmkES application which serves as a prototype for a secure terminal system.
testbufvariant
A CAmkES application which is used to test dataports.
testcamkes438
A CAmkES application that is used to test a specific function of the CAmkES framework.
testcontrolname
A CAmkES application that is used to test if interfaces could be named with a particular suffix.
testdataportbifurcate
A CAmkES application that tests if we can have multiple dataports within a single component that maps to the same underlying physical memory.
testdataportmux
A CAmkES application that tests the ability to have multiple CAmkES components connected to the same dataport.
testdataportmuxflat
A CAmkES application that tests the ability to have N-to-M dataport connections in a single address space.
testdataportptrwrap
A CAmkES application that tests if dataport pointer wrapping and unwrapping functionality works on multiplexed dataports.
testdataportrpc
A CAmkES application that tests if we can back an seL4RPCCall connection with various types of dataports.
testfaulthandlers
A CAmkES application that tests if the fault handlers work correctly as intended.
testgrouping
A CAmkES application which tests for the various edge cases in grouping CAmkES components into single address spaces.
testgroupingcontrol
A CAmkES application which tests whether CAmkES components with a control thread work correctly when grouped in a single address spaces.
testhardwareinterrupt
A CAmkES application which tests if an application containing an seL4HardwareInterrupt successfully compiles.
testhwdataportlrgpages
A CAmkES application which tests whether or not large pages will be used to back a large dataport.
testnto1mmio
A CAmkES application that tests if an N-to-1 MMIO connection to a piece of hardware functions correctly.
testnto1overload
A CAmKES application that tests if N-to-1 connections involving multiple ends from a single CAmkES component uses distinct caps.
testrefin
A CAmKES application that tests the ‘refin’ parameter function in CAmkES procedure interfaces.
testreplycapprotection
A CAmkES application that tests the reply cap protection functionality.
testsel4notification
A CAmkES application that tests the seL4Notification connector.
testsingleaddressspaceheap
A CAmkES application that tests that the heaps of CAmkES components that share a single address space do not overlap.
teststringarrays
A CAmkES application that tests some unusual usages of string array parameters in procedure interfaces.
testsyscalls
A CAmkES application that serves as a testing sandbox for POSIX syscall functionality on CAmkES.
testunderscorename
A CAmkES application that tests if CAmkES components can have interface names prefixed with an underscore.
timeserver
A CAmkES application which demonstrates the use of the TimeServer componen fromthe global-components repository.
uart
A CAmkES application which demonstrates a UART driver CAmkES component for the KZM platform.
vgatest
A CAmkES application which demonstrates a minimal implementation for a text mode VGA terminal.
Reusable components
Components | Description |
---|---|
|
A CAmkES component which abstracts over and multiplexes client accesses to clock devices on a platform. |
|
A CAmkES component which abstracts over and multiplexes client accesses to an Ethernet device. |
|
A CAmkES component which abstracts over and multiplexes client accesses to a CPIO-based file system. |
|
A CAmkES component which abstracts over and multiplexes client accesses to a GPIO and pin multiplexer controller. |
|
A CAmkES component which abstracts over and multiplexes client accesses to the PCI configuration space of a platform. |
|
A CAmkES component which abstracts over and multiplexes client accesses to an IP stack, specifically, the PicoTCP TCP/IP stack. |
|
A CAmkES component which abstracts over and multiplexes client accesses to a reset line controller. |
|
A CAmkES component which abstracts over and multiplexes client accesses to a real-time clock device. |
|
A CAmkES component which abstracts over and multiplexes client accesses to a serial device. |
|
A CAmkES component which abstracts over and multiplexes client accesses to a timer device. |
|
A stub CAmkES component which is used to help initialise virtqueue connections. |
|
Stub hardware CAmkES component that abstracts over a pc99-based serial device. |
|
Stub hardware CAmkES component that abstracts over the x86 Programmable Interval Timer. |
ClockServer
A CAmkES component which abstracts over and multiplexes client accesses to clock devices on a platform.
Ethdriver
A CAmkES component which abstracts over and multiplexes client accesses to an Ethernet device.
FileServer
A CAmkES component which abstracts over and multiplexes client accesses to a CPIO-based file system.
GPIOMUXServer
A CAmkES component which abstracts over and multiplexes client accesses to a GPIO and pin multiplexer controller.
PCIConfigIO
A CAmkES component which abstracts over and multiplexes client accesses to the PCI configuration space of a platform.
PicoServer
A CAmkES component which abstracts over and multiplexes client accesses to an IP stack, specifically, the PicoTCP TCP/IP stack.
ResetServer
A CAmkES component which abstracts over and multiplexes client accesses to a reset line controller.
RTC
A CAmkES component which abstracts over and multiplexes client accesses to a real-time clock device.
SerialServer
A CAmkES component which abstracts over and multiplexes client accesses to a serial device.
TimeServer
A CAmkES component which abstracts over and multiplexes client accesses to a timer device.
VirtQueue
A stub CAmkES component which is used to help initialise virtqueue connections.
Serial
Stub hardware CAmkES component that abstracts over a pc99-based serial device.
PIT
Stub hardware CAmkES component that abstracts over the x86 Programmable Interval Timer.
CAmkES Connectors
Components | Description | Status |
---|---|---|
|
CAmkES connector which is used to connect clients to the Ethdriver component’s procedure interface. |
Supported |
|
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 |
|
CAmkES connector which is used to make the underlying seL4 notification capability available to the consuming side of the Event interface. |
Supported |
|
CAmkES connector which allows the sending and queueing of user-defined messages from one component to another. |
Supported |
|
CAmkES connector which allows multiple dataports to be connected to a single components and also provides multiplexed access across the dataports. |
Supported |
|
CAmkES connector which bundles a procedure interface with an event interface. |
Supported |
|
CAmkES connector which bundles a procedure interface with a dataport interface. |
Supported |
|
CAmkES connector which bundles a procedure interface, event interface, and a dataport interface. |
Supported |
|
CAmkES connector which uses shared memory to transfer data instead of the IPC buffer for procedure interfaces. |
Supported |
|
CAmkES connector which allocates a shared memory region between components and also exposes the underlying frame caps. |
Supported |
|
CAmkES connector which initialises a virtqueue connection between two components. |
Supported |
|
Used for RPC interfaces between grouped components. Each call becomes a direct function call. |
Supported |
|
Event connector where an 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 |
|
Similar event connector to seL4Notification but the receiver has bound the Notification to its TCB. |
Supported |
|
Similar event connector to seL4Notification but the receiver end can only call Poll or Wait on notification object. |
Supported |
|
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 |
|
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. |
|
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 |
|
seL4 RPCCall connector but without requirement of single procedure interface. This allows a single receiver thread to handle multiple senders with different interfaces. |
Supported |
|
seL4 Dataport connector. Creates a shared memory connection between components. |
Supported |
|
seL4 Dataport connector to MMIO region. Creates a MMIO mapping for device registers into a component. |
Supported |
|
seL4 Procedure connector for x86 IOPorts. Provides functions for performing IOPort instructions via seL4 invocations. |
Supported |
|
seL4 event connector for hardware interrupts. Provides interface for polling or blocking on interrupts and also for acknowledging IRQs. |
Supported |
|
seL4 event connector for IOAPIC hardware interrupts. Specialised connector for dealing with IOAPIC interrupts. |
Supported on x86 |
seL4Ethdriver
CAmkES connector which is used to connect clients to the Ethdriver component’s procedure interface.
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.
seL4GlobalAsync
CAmkES connector which is used to make the underlying seL4 notification capability available to the consuming side of the Event interface.
seL4MessageQueue
CAmkES connector which allows the sending and queueing of user-defined messages from one component to another.
seL4MultiSharedData
CAmkES connector which allows multiple dataports to be connected to a single components and also provides multiplexed access across the dataports.
seL4RPCCallSignal
CAmkES connector which bundles a procedure interface with an event interface.
seL4RPCDataport
CAmkES connector which bundles a procedure interface with a dataport interface.
seL4RPCDataportSignal
CAmkES connector which bundles a procedure interface, event interface, and a dataport interface.
seL4RPCOverMultiSharedData
CAmkES connector which uses shared memory to transfer data instead of the IPC buffer for procedure interfaces.
seL4SharedDataWithCaps
CAmkES connector which allocates a shared memory region between components and also exposes the underlying frame caps.
seL4VirtQueues
CAmkES connector which initialises a virtqueue connection between two components.
seL4DirectCall
Used for RPC interfaces between grouped components. Each call becomes a direct function call.
seL4Notification
Event connector where an 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.
seL4NotificationBind
Similar event connector to seL4Notification but the receiver has bound the Notification to its TCB.
seL4NotificationNative
Similar event connector to seL4Notification but the receiver end can only call Poll or Wait on notification object.
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.
seL4RPCCall
Used for RPC interfaces where parameters will be marshalled into and out of IPC buffers and calls ocurr over seL4Endpoint objects.
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.
seL4RPCCallNoType
seL4 RPCCall connector but without requirement of single procedure interface. This allows a single receiver thread to handle multiple senders with different interfaces.
seL4SharedData
seL4 Dataport connector. Creates a shared memory connection between components.
seL4HardwareMMIO
seL4 Dataport connector to MMIO region. Creates a MMIO mapping for device registers into a component.
seL4HardwareIOPort
seL4 Procedure connector for x86 IOPorts. Provides functions for performing IOPort instructions via seL4 invocations.
seL4HardwareInterrupt
seL4 event connector for hardware interrupts. Provides interface for polling or blocking on interrupts and also for acknowledging IRQs.
seL4IOAPICHardwareInterrupt
seL4 event connector for IOAPIC hardware interrupts. Specialised connector for dealing with IOAPIC interrupts.