libsel4camkes: Add markdown documentation

This commit adds documentation written in markdown that explains each
part of the libsel4camkes library in more depth.

Signed-off-by: Gerwin Klein <[email protected]>

libsel4camkes/README.md

@@ -1,39 +1,22 @@
 <!--
-     Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
      SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
-# 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.

libsel4camkes/docs/allocator.md

@@ -0,0 +1,45 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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.<object type>_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

libsel4camkes/docs/dataport.md

@@ -0,0 +1,37 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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);
+```

libsel4camkes/docs/dma.md

@@ -0,0 +1,38 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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.

libsel4camkes/docs/error.md

@@ -0,0 +1,39 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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.

libsel4camkes/docs/fault.md

@@ -0,0 +1,30 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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.

libsel4camkes/docs/init.md

@@ -0,0 +1,12 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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.

libsel4camkes/docs/marshall_macros.md

@@ -0,0 +1,12 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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.

libsel4camkes/docs/msgqueue.md

@@ -0,0 +1,93 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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.

libsel4camkes/docs/pid.md

@@ -0,0 +1,14 @@
+<!--
+     Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
+
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# 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