diff --git a/libsel4camkes/README.md b/libsel4camkes/README.md index 885f742a..dbc75231 100644 --- a/libsel4camkes/README.md +++ b/libsel4camkes/README.md @@ -1,39 +1,22 @@ -# CAmkES support functionality +# libsel4camkes -To use this library in a project you should link 'sel4camkes' to your target -application/component with CMake. This library provides various utilities for -interfacing with seL4 in a CAmkES-based system. Some of these utilities are: +This is a library that contains a collection of user-friendly abstractions to +the CAmkES runtime environment, as well some backend functions for the CAmkES +environment to bootstrap and configure the runtime environment. -### virtqueue +## Usage -**_This implementation is currently a work in progress_** +All CAmkES components link against this library, but if there is a specific +need to link against this library, include this library using the +`target_link_library` CMake directive or similar with the `sel4camkes` item. -Functions are provided to help create virtqueue connections between your CAmkES -components. This is based on the libvirtqueue implementation -(project_libs/libvirtqueue). The functions provided are divided into two -interfaces, being: - * _virtqueue template.h:_ These are functions intended to be used by a - CAmkES template. This interface is meant to allow a CAmkES template to - register a virtqueue channel. - * _virtqueue.h_ : These are functions intended to be used by a CAmkES - component. This interface provides a CAmkES component the ability to - create virtqueue objects (from libvirtqueue) out of the channels - registered by its templates. This interface also includes - memory allocation mechanisms over dataports for creating virtqueue buffers - to pass data with. +## Contents -#### Caveats - -This library is still under active development. Current shortcomings of the -implementation include: -* Each virtqueue is expected to have its own shared memory buffer region. Thus - allocating a virtqueue buffer will always return the same region of memory. The - allocation mechanisms are intended to be changed to work over a global memory region with - other components. -* The maximum number of virtqueues a component can register is defined by `MAX_CAMKES_VIRTQUEUE_ID` +The functions exposed by this library can be found in the `include` folder. +There is also more in-depth documentation inside the `docs` folder. diff --git a/libsel4camkes/docs/allocator.md b/libsel4camkes/docs/allocator.md new file mode 100644 index 00000000..b3793ab2 --- /dev/null +++ b/libsel4camkes/docs/allocator.md @@ -0,0 +1,45 @@ + + +# Allocator + +The allocator in `libsel4camkes` can be used to allocate seL4 capability objects +from a managed pool. The `camkes_provide` function is mostly used by the +CAmkES backend to setup the pool on behalf of the user. In `simple` or +'dynamic' configurations of CAmkES, other allocators (`vka`, `vspace`, etc) +would be preferred instead. + +## Usage + +The `camkes_alloc` and `camkes_free` functions can be used to allocate and free +seL4 capability objects from and to the managed pool. It is possible to provide +your own seL4 objects to the pool using `camkes_provide` but CAmkES allows +users to specify some objects to be created and provided to the pool +automatically. + +So far, only TCBs, Endpoints, Notifications, and Untypes can be allocated. +Below is an example of asking CAmkES to allocate these objects. + +```c +assembly { + composition { + component Foo bar; + } + + configuration { + bar._pool = 12; + } +} +``` + +In the example, CAmkES would allocate 12 objects of type 'object type'. Valid +object types are: + +- `tcb` +- `ep` +- `notification` +- `untypedX`, where X is a number indicating the size of the untyped, e.g. + `untyped12` would ask for untypes of size 2 to the power 12, or 4096 diff --git a/libsel4camkes/docs/dataport.md b/libsel4camkes/docs/dataport.md new file mode 100644 index 00000000..49b21855 --- /dev/null +++ b/libsel4camkes/docs/dataport.md @@ -0,0 +1,37 @@ + + +# Dataport + +`libsel4camkes` provides some functions for interacting with CAmkES dataports. +There are also some definitions intended for CAmKES internal use. + +## Usage + +There are two functions for wrapping and unwrapping pointers that point to the +dataport into and from a data format that can be shared between components. +These are: + +```c +dataport_ptr_t dataport_wrap_ptr(void *ptr); + +void *dataport_unwrap_ptr(dataport_ptr_t ptr); +``` + +Although components may share memory between each other using CAmkES +dataports, the dataports may not be necessarily be mapped into the same virtual +address in the components' address space. Thus, these functions are used to +communicate pointers in the dataport by converting them into a format that's +understood by all components that have a shared dataport connection. + +There is an additional function that allows clients to perform cache +maintenance operations on the dataports. + +```c +int camkes_dataport_flush_cache(size_t start_offset, size_t size, + uintptr_t dataport_start, size_t dataport_size, + dma_cache_op_t cache_op); +``` diff --git a/libsel4camkes/docs/dma.md b/libsel4camkes/docs/dma.md new file mode 100644 index 00000000..d7063063 --- /dev/null +++ b/libsel4camkes/docs/dma.md @@ -0,0 +1,38 @@ + + +# DMA + +`libsel4camkes` provides functions for interacting with a DMA pool that is +allocated and managed by CAmkES. These functions are essentially an +implementation of the `ps_dma_man_t` interface in `ps_io_ops_t`. It is preferred +that the DMA requests go through the `ps_dma_man_t` interfaces instead of using +these functions. + +## Usage + +Each DMA pool is unique to each component and can be allocated by setting a +specific attribute in CAmkES. For example, the following allocates a DMA pool +that's of size `0x4000` to the component `bar`. + +```c +assembly { + composition { + component Foo bar; + } + + configuration { + bar.dma_pool = 0x4000; + } +} +``` + +CAmkES will then ask the linker to provide a section of memory to be reserved +as the DMA pool. During component initialisation, the CAmkES runtime will +initialise the DMA pool by calling `camkes_dma_init` with the reserved DMA +pool. Clients can then call `camkes_dma_alloc` and `camkes_dma_free`, or use +the functions exposed by the `ps_dma_man_t` interface after a `camkes_io_ops` +call to interact with the DMA pool. diff --git a/libsel4camkes/docs/error.md b/libsel4camkes/docs/error.md new file mode 100644 index 00000000..60ea0a37 --- /dev/null +++ b/libsel4camkes/docs/error.md @@ -0,0 +1,39 @@ + + +# Error + +`libsel4camkes` provides some functions for dealing with errors from the CAmkES +runtime. + +## Usage + +In rare occasions, the CAmkES runtime can produce an error on some operations. +When such an error occurs, the CAmkES runtime will invoke an error handler to +deal with the error. The default error handler will simply halt the system. It +is possible to install a custom error handler with the following function. + +```c +camkes_error_handler_t camkes_register_error_handler(camkes_error_handler_t handler); +``` + +The error handler is of type: + +```c +typedef camkes_error_action_t (*camkes_error_handler_t)(camkes_error_t *); +``` + +The error handler is given relevant information from the `camkes_error_t` +struct and is expected to handle the error and return a `camkes_error_type_t` +return code indicating the action to take. The actions that can be taken are to: + +- discard the transaction +- ignore the error +- exit with failure + +See the +[header](https://github.com/seL4/camkes-tool/blob/master/libsel4camkes/include/camkes/error.h) +for more information. diff --git a/libsel4camkes/docs/fault.md b/libsel4camkes/docs/fault.md new file mode 100644 index 00000000..fcecd655 --- /dev/null +++ b/libsel4camkes/docs/fault.md @@ -0,0 +1,30 @@ + + +# Fault + +`libsel4camkes` provides functions for examining faults that are generated +by applications. + +## Usage + +When an application triggers a fault, the seL4 kernel will invoke the the +faulting thread's fault handler. The fault handler is then given information +about the fault and is expected to resolve the situation. CAmkES will register a +default fault handler on a debug build that will call a function to show +information about the fault. This function is: + +```c +void camkes_show_fault(seL4_MessageInfo_t info, seL4_CPtr thread_id, + const char *name, bool tcp_caps_available, + const camkes_memory_region_t *memory_map); +``` + +The function takes the fault information that the kernel provides in the +faulting thread's IPC buffer and displays it in a human readable format. + +Currently this function is expected to be called by a component's fault handler +if any component threads fault. diff --git a/libsel4camkes/docs/init.md b/libsel4camkes/docs/init.md new file mode 100644 index 00000000..0f33d082 --- /dev/null +++ b/libsel4camkes/docs/init.md @@ -0,0 +1,12 @@ + + +# Init + +The init functions in `libsel4camkes` are mostly used internally in the CAmkES +runtime backend. These functions are the entry points for the component's +control thread, which sets up the runtime and prepares the state for running +the component's application code. diff --git a/libsel4camkes/docs/marshall_macros.md b/libsel4camkes/docs/marshall_macros.md new file mode 100644 index 00000000..03d4d9e3 --- /dev/null +++ b/libsel4camkes/docs/marshall_macros.md @@ -0,0 +1,12 @@ + + +# Marshalling macros + +These are a collection of macros intended to be used with the marshalling and +unmarshalling process of CAmkES RPC functional calls. These macros are used by +the CAmkES tools to build RPC-connectors; they are not intended as a public +interface. diff --git a/libsel4camkes/docs/msgqueue.md b/libsel4camkes/docs/msgqueue.md new file mode 100644 index 00000000..020663c7 --- /dev/null +++ b/libsel4camkes/docs/msgqueue.md @@ -0,0 +1,93 @@ + + +# Message queues + +`libsel4camkes` provides an implementation of a message queue transport +mechanism. The message queues can be used to transfer small messages from a +component to another component asynchronously. The message size is limited by +the underlying `virtqueue` mechanism and the fact that the messages are copied. +For large messages, it is recommended to use shared memory/data ports directly. +Small message transfer is especially useful, when additional state needs to be +passed instead of a simple alert like the notifications that seL4 provides. Note +that message queues are one-way and not a two-way channel, can only be one +sender and one receiver per channel. + +## Usage + +The message queue libraries require components to first initialise a +`seL4Msgqueue` CAmkES connection between components. Here's an example of how +this is done: + +```c +component Foo { + dataport Message rx; +} + +component Foo2 { + dataport Message tx; +} + +assembly { + composition { + component Foo bar; + component Foo2 baz; + + connection messagequeue_foo seL4Msgqueue(from baz.tx, to bar.rx); + } + + configuration { + bar.rx_id = 1; + baz.tx_id = 1; + messagequeue_foo.queue_size = 256; + } +} +``` + +From the example above, the sender is `baz`, and the receiver is `bar`. The IDs +of this particular message queue channel are 1 for both components. It is +possible to have multiple channels for a component, but their IDs must be +different. The queue size of the message queue is 256 and can be changed. It +must be a power of two. The messages that will be transferred in the channel are +of type `Message` as indicated by the dataport. + +Next, in the application code, the sender and receivers must initialise their +ends of the channel by calling the appropriate function from the following: + +```c +int camkes_msgqueue_sender_init(int msgqueue_id, camkes_msgqueue_sender_t *sender); + +int camkes_msgqueue_receiver_init(int msgqueue_id, camkes_msgqueue_receiver_t *receiver); +``` + +The sender can then call the following function to send messages. + +```c +int camkes_msgqueue_send(camkes_msgqueue_sender_t *sender, void *message, size_t message_size); +``` + +The message type should be of the type of the underlying dataport, there are +checks to make sure that the message size does not go over the limit defined in +`camkes_msgqueue_sender_t`. + +On the receiver side, there are two functions to check the status of the channel +and to possibly block on the channel waiting for a message. + +```c +int camkes_msgqueue_poll(camkes_msgqueue_receiver_t *recevier); + +int camkes_msgqueue_wait(camkes_msgqueue_receiver_t *receiver); +``` + +When a message arrives as indicated by the functions, the receiver can retrieve +a message of the channel with the following. + +```c +int camkes_msgqueue_get(camkes_msgqueue_receiver_t *receiver, void *buffer, size_t buffer_size); +``` + +The buffer should be sufficiently sized to store a message of a type as +indicated by the type of the dataport. diff --git a/libsel4camkes/docs/pid.md b/libsel4camkes/docs/pid.md new file mode 100644 index 00000000..d703523e --- /dev/null +++ b/libsel4camkes/docs/pid.md @@ -0,0 +1,14 @@ + + +# PID + +This is a constant variable that tracks the ID of the CAmkES component. +Although CAmkES and seL4 do not have a concept of processes, this variable is +used to maintain compatibility with parts of the POSIX standard. Note that the +variable is managed by CAmkES-generated code. + +TODO Check this diff --git a/libsel4camkes/docs/ps_io_ops_t.md b/libsel4camkes/docs/ps_io_ops_t.md new file mode 100644 index 00000000..5802037b --- /dev/null +++ b/libsel4camkes/docs/ps_io_ops_t.md @@ -0,0 +1,117 @@ + + +# `ps_io_ops_t` + +CAmkES provides an implementation of the `ps_io_ops_t` as part +of its runtime environment. + + + +## `ps_malloc_ops_t` + + + +The CAmkES `ps_malloc_ops_t` interface for performing anonymous memory +allocation is implemented by wrapping musllibc `malloc`, `calloc` and `free` +calls. A CAmkES component can be configured with a fixed sized heap that is +used to perform these memory allocations. + +## `ps_io_mapper_t` + + + +The CAmkES `ps_io_mapper_t` interface for memory mapped I/O (MMIO) uses a record +of all device memory mappings in the component's virtual address space to look +up a virtual address for a corresponding physical address. CAmkES hardware +connector templates generate the MMIO mappings in the CapDL spec. The templates +are also expected to register the mappings in the special linker section +`_dataport_frames`, describing each MMIO mapping region by its size, physical +address and mapping attributes. The CAmkES `ps_io_mapper_t` uses this +information to return the mapping information to callers. + +No action is taken when the `unmap` function is called. + +Mapping attributes requested are currently ignored since the mappings already +exist and cannot be changed. A configuration may be provided in the future to +perform mapping attribute validation in order to catch any configuration +errors, but this is currently unsupported. + +## `ps_dma_man_t` + + + +The CAmkES `ps_dma_man_t` interface for Direct Memory Access (DMA) uses a +statically defined pool of DMA memory from which the interface implementation +allocates DMA regions. The mappings for this pool are created during system +initialisation, and the interface responds to alloc and pin requests by handing +out the virtual and physical addresses for these regions. + +IOMMU and SMMU are not currently supported. This could be implemented by also +mapping the static DMA pool memory into the hardware address spaces provided by +the IOMMU implementation. + +The cache operations provided by this interface are no-ops as the entire pool +is mapped uncached. + +The size of the DMA pool is configured for each component by setting +`${component_name}.dma_pool = ${pool_size_in_bytes};` in the `configuration` +section of a `.camkes` file. + +## `ps_irq_ops_t` + + + +The CAmkES `ps_irq_ops_t` interface for hardware interrupt handling uses a +record of interrupt to seL4 notification mappings to register callback handlers +for specific interrupts. When a CAmkES connector allocates an seL4 notification +as a specific interrupt handler it records information in the `_allocated_irqs` +linker section. The CAmkES `ps_irq_ops_t` implementation looks through this +section to match a requested register call with an existing interrupt +notification. CAmkES then sets the provided callback handler to be invoked when +an interrupt arrives on the notification. When an interrupt is received, the +provided handler is invoked and given a function for performing the seL4 +interrupt acknowledgment. + +## `ps_io_port_ops_t` + + + +The `ps_io_port_ops_t` interface for architectural I/O operations is +implemented for x86 IOPorts. Connectors that allocate CapDL IOPort capabilities +are expected to register these capabilities in the `_ioport_regions` linker +section. The CAmkES implementation of the IOPort interface looks up these +capabilities for requested IOPorts and then performs the correct seL4 IOPort +invocation. Errors are returned for any IOPorts that the component does not +have access to. + +A feature may be added in the future for delegating IOPort calls to a different +CAmkES component. This is required to support sharing of devices across +components such as for a PCI bus. Currently, IOPort operations for accessing +PCI configuration IOPorts located in a different components need to be called +through a separate API. + +## `ps_io_fdt_t` + + + +The CAmkES `ps_io_fdt_t` interface for providing access to a flattened device +tree (FDT) uses node information made available in the component's address space +during system initialisation. CAmkES hardware connectors register a CapDL FDT +content frame that causes the FDT (which is passed into CapDL loader by seL4 +during startup) to be copied into the component's address space. The CAmkES +`ps_io_fdt_t` interface returns a reference to this FDT. + +## `ps_interface_registration_ops_t` + + + +The CAmkES `ps_interface_registration_ops_t` interface is implemented as a +two-level nested linked list data structure that can have elements appended and +removed while also allowing iteration over it. + +CAmkES populates the list for each component based on which other components it +is connected to according the static system architecture. diff --git a/libsel4camkes/docs/syscalls.md b/libsel4camkes/docs/syscalls.md new file mode 100644 index 00000000..98985680 --- /dev/null +++ b/libsel4camkes/docs/syscalls.md @@ -0,0 +1,13 @@ + + +# Syscalls + +While the CAmkES runtime isn't fully POSIX compliant (and does not intend to +be), the CAmkES runtime implements a subset of POSIX syscalls to provide some +compatibility with POSIX applications. The +[header](https://github.com/seL4/camkes-tool/blob/master/libsel4camkes/include/camkes/syscalls.h) +provides a list of syscalls that the CAmkES runtime implements. diff --git a/libsel4camkes/docs/timing.md b/libsel4camkes/docs/timing.md new file mode 100644 index 00000000..0704f00e --- /dev/null +++ b/libsel4camkes/docs/timing.md @@ -0,0 +1,11 @@ + + +# Timing + +This part of the `libsel4camkes` library provides functions that are useful for +benchmarking CAmkES applications. However, these functions are out of date +and are likely not usable in their current state. diff --git a/libsel4camkes/docs/tls.md b/libsel4camkes/docs/tls.md new file mode 100644 index 00000000..16135c1d --- /dev/null +++ b/libsel4camkes/docs/tls.md @@ -0,0 +1,26 @@ + + +# Thread-Local Storage (TLS) + +This part of the library contains definitions and functions related to +CAmkES-specific thread-local storage. These functions are intended for +CAmkES-internal use to manage the state of each thread on top of the CAmkES +runtime. + +## Usage + +When constructing templates for RPC-related CAmkES-connections, there may be +situations where the seL4 endpoint reply cap may need to be managed. There are +three functions which can be used to manage the reply cap, these are: + +```c +int camkes_declare_reply_cap(seL4_CPtr shadow_slot); + +void camkes_protect_reply_cap(void); + +seL4_Error camkes_unprotect_reply_cap(void); +``` diff --git a/libsel4camkes/docs/virtqueue.md b/libsel4camkes/docs/virtqueue.md new file mode 100644 index 00000000..c256227a --- /dev/null +++ b/libsel4camkes/docs/virtqueue.md @@ -0,0 +1,139 @@ + + +# Virtqueues + +`libsel4camkes` provides an implementation of the virtqueue transport mechanism. +virtqueues can be used to asynchronously transfer data between two components. +Although virtqueues are mostly used between clients and device drivers, this +transport mechanism is useful for general producer-consumer patterns. + +## Usage + +The virtqueue libraries requires components to first initialise a +`seL4VirtQueue` CAmkES connection between components. Here's an example of how +this is done: + +```c +component Foo { + uses VirtQueueDrv drv; +} + +component Foo2 { + uses VirtQueueDev dev; +} + +assembly { + composition { + component VirtQueueInit vq_init; + component Foo bar; + component Foo2 baz; + + connection virtqueue_foo seL4VirtQueue(to vq_init.init, from bar.drv, from baz.dev); + } + + configuration { + bar.drv_id = 1; + baz.dev_id = 1; + bar.drv_shmem_size = 4096; + baz.dev_shmem_size = 4096; + virtqueue_foo.init_topology = [{"drv" : "bar.drv", "dev": "baz.dev" }]; + } +} +``` + +From the example above, the driver side of the virtqueue is `bar` and the device +side is `baz`. The IDs of this particular virtqueue channel are 1 for both +components. It is possible to have multiple channels for a component, but each +channel's ID must be different. The memory size of the channel is one page by +default and can be changed. However, it must be page-aligned. The size of a small +page on all currently supported platforms (Arm, x86, x64, RISCV) is 4096 bytes. + +Next, in the application code, the driver and device side of the channel must +each initialise their end of the channel by calling the appropriate function +from the following: + +```c +static inline int camkes_virtqueue_driver_init(virtqueue_driver_t *driver, unsigned int camkes_virtqueue_id) { ... } + +static inline int camkes_virtqueue_device_init(virtqueue_device_t *device, unsigned int camkes_virtqueue_id) { ... } +``` + +There is also a version of these functions which can return the underlying +notification object that is backing the notification part of the virtqueues. + +```c +int camkes_virtqueue_driver_init_with_recv(virtqueue_driver_t *driver, unsigned int camkes_virtqueue_id, + seL4_CPtr *recv_notification, seL4_CPtr *recv_badge); + +int camkes_virtqueue_device_init_with_recv(virtqueue_device_t *device, unsigned int camkes_virtqueue_id, + seL4_CPtr *recv_notification, seL4_CPtr *recv_badge); +``` + +The rest of the functions are essentially helper or convenience functions over +the virtqueue interface as defined +[here](https://github.com/SEL4PROJ/projects_libs/blob/master/libvirtqueue/include/virtqueue.h). + +### Driver + +When sending data over to the device side, it is preferred to use to these two +functions. + +```c +int camkes_virtqueue_driver_send_buffer(virtqueue_driver_t *vq, void *buffer, size_t size); + +int camkes_virtqueue_driver_scatter_send_buffer(virtqueue_driver_t *vq, void *buffer, size_t size); +``` + +When collecting buffers from the device side, the client must first obtain a +handle to a used buffer ring via this virtqueue interface function: + +```c +int virtqueue_get_used_buf(virtqueue_driver_t *vq, virtqueue_ring_object_t *robj, uint32_t *len); +``` + +It is then possible to gather each buffer in the used buffer ring and copy it +into a larger buffer using the first function or iterate through each buffer in +the ring using the second function: + +```c +int camkes_virtqueue_driver_gather_copy_buffer(virtqueue_driver_t *vq, virtqueue_ring_object *handle, + void *buffer, size_t size); + +int camkes_virtqueue_driver_gather_buffer(virtqueue_driver_t *vq, virtqueue_ring_object_t *handle, + void **buffer, unsigned *size, vq_flags_t *flag); +``` + +### Device side + +Collecting buffers from the driver side requires the client to first obtain a +handle to an available buffer ring via this virtqueue interface function: + +```c +int virtqueue_get_available_buf(virtqueue_device_t *vq, virtqueue_ring_object_t *robj); +``` + +The buffers can then be: + +- gathered and copied into a larger buffer using the first function, +- have the contents of a larger scatter-copied into the buffers using the second + function, +- or, iterated through using the second function: + +```c +int camkes_virtqueue_device_gather_copy_buffer(virtqueue_device_t *vq, virtqueue_ring_object_t *handle, + void *buffer, size_t size); + +int camkes_virtqueue_device_scatter_copy_buffer(virtqueue_device_t *vq, virtqueue_ring_object_t *handle, + void *buffer, size_t size); + +int camkes_virtqueue_device_gather_buffer(virtqueue_device_t *vq, virtqueue_ring_object_t *handle, + void **buffer, unsigned *size, vq_flags_t *flag); +``` + +Note that the first two functions will automatically add the buffers to the +device channel's used ring for the driver side to collect; the third one will +not. diff --git a/libsel4camkes/docs/vma.md b/libsel4camkes/docs/vma.md new file mode 100644 index 00000000..3477dc3a --- /dev/null +++ b/libsel4camkes/docs/vma.md @@ -0,0 +1,26 @@ + + +# VMA + +This part of the library contains definitions that can be used to obtain +information about the Virtual Memory Areas (VMA) of a CAmkES application. The +definitions are mostly used by other parts of the library to manipulate a +component's address space. + +## Usage + +Information about the sections of a component's address space can be found via +the following variables. + +```c +extern const struct camkes_vma camkes_vmas[]; + +extern const size_t camkes_vmas_size; +``` + +This array is filled in by the CAmkES backend as it generates code for a +particular component.