libsel4camkes: Add markdown documentation

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

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 contain 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,50 @@
+<!--
+  Copyright 2020, Data61
+  Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+  ABN 41 687 119 230.
+
+  This software may be distributed and modified according to the terms of
+  the BSD 2-Clause license. Note that NO WARRANTY is provided.
+  See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+  -->
+
+# Allocator 
+
+The allocator in libsel4camkes can be used to allocate seL4 capability objects
+from a managed pool. The `camkes_provide` function is mostly used in the 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.
+Here's a following 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,42 @@
+<!--
+  Copyright 2020, Data61
+  Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+  ABN 41 687 119 230.
+
+  This software may be distributed and modified according to the terms of
+  the BSD 2-Clause license. Note that NO WARRANTY is provided.
+  See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+  -->
+
+# 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 some memory between each with the use 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 in a format that's
+understood by all components that have a shared dataport connection.
+
+There is also an addditional function that allows clients to perform cache
+maintaince 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,44 @@
+<!--
+  Copyright 2020, Data61
+  Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+  ABN 41 687 119 230.
+
+  This software may be distributed and modified according to the terms of
+  the BSD 2-Clause license. Note that NO WARRANTY is provided.
+  See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+  -->
+
+# DMA
+
+libsel4camkes provides some functions for interacting with a DMA pool that
+CAmkES allocates and manages. 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,42 @@
+<!--
+  Copyright 2020, Data61
+  Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+  ABN 41 687 119 230.
+
+  This software may be distributed and modified according to the terms of
+  the BSD 2-Clause license. Note that NO WARRANTY is provided.
+  See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+  -->
+
+# Error
+
+libsel4camkes provides some functions for dealing with errors with the CAmkES
+runtime.
+
+## Usage
+
+In rare occasions, the CAmkES runtime can fail on some operations. Upon
+failure, the CAmkES runtime will invoke an error handler to deal with the
+error. The default error handler will simply halt the system upon error. 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,36 @@
+<!--
+  Copyright 2020, Data61
+  Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+  ABN 41 687 119 230.
+
+  This software may be distributed and modified according to the terms of
+  the BSD 2-Clause license. Note that NO WARRANTY is provided.
+  See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+  -->
+
+# Fault
+
+libsel4camkes provides some functions for examining faults that are generated
+by the applications.
+
+## Usage
+
+When an application triggers a fault, the seL4 kernel will invoke the
+applications, or more specifically, the 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 written by the kernel into 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,17 @@
+<!--
+  Copyright 2020, Data61
+  Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+  ABN 41 687 119 230.
+
+  This software may be distributed and modified according to the terms of
+  the BSD 2-Clause license. Note that NO WARRANTY is provided.
+  See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+  -->
+
+# 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 to setup the runtime, and also the component's application code.

libsel4camkes/docs/marshall_macros.md

@@ -0,0 +1,18 @@
+<!--
+  Copyright 2020, Data61
+  Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+  ABN 41 687 119 230.
+
+  This software may be distributed and modified according to the terms of
+  the BSD 2-Clause license. Note that NO WARRANTY is provided.
+  See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+  -->
+
+# Marshall macros
+
+These are a collection of macros intended to be used with the marshalling and
+unmarshalling process of CAmkES RPC functional calls. The RPC-related CAmkES
+connectors are built with the help of these macros and outside of the
+connectors, there does not seem to be a use case for these macros.