[squash] partially address review feedback

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

libsel4camkes/README.md

@@ -6,7 +6,7 @@
 
 # libsel4camkes
 
-This is a library that contain a collection of user-friendly abstractions to
+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.
 

libsel4camkes/docs/allocator.md

@@ -1,13 +1,13 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
-# Allocator 
+# 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
+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.
@@ -21,14 +21,14 @@ 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.
+Below is an example of asking CAmkES to allocate these objects.
 
 ```c
 assembly {
     composition {
         component Foo bar;
-    } 
-    
+    }
+
     configuration {
         bar.<object type>_pool = 12;
     }
@@ -37,8 +37,9 @@ assembly {
 
 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
+
+- `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

@@ -1,33 +1,34 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
 # Dataport
 
-libsel4camkes provides some functions for interacting with CAmkES dataports.
+`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:
+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
+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 in a format that's
+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 also an addditional function that allows clients to perform cache
-maintaince operations on the dataports.
+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,

libsel4camkes/docs/dma.md

@@ -1,16 +1,16 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
 # 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.
+`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
 
@@ -23,7 +23,7 @@ assembly {
     composition {
         component Foo bar;
     }
-    
+
     configuration {
         bar.dma_pool = 0x4000;
     }

libsel4camkes/docs/error.md

@@ -1,20 +1,20 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
 # Error
 
-libsel4camkes provides some functions for dealing with errors with the CAmkES
+`libsel4camkes` provides some functions for dealing with errors from 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.
+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);
@@ -28,9 +28,12 @@ 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
+return code indicating the action to take. The actions that can be taken are to:
 
-See the [header](https://github.com/seL4/camkes-tool/blob/master/libsel4camkes/include/camkes/error.h) for more information.
+- 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

@@ -1,29 +1,29 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
 # Fault
 
-libsel4camkes provides some functions for examining faults that are generated
-by the applications.
+`libsel4camkes` provides functions for examining faults that are generated
+by 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:
+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 written by the kernel into the
+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

libsel4camkes/docs/init.md

@@ -1,11 +1,12 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
-# Init 
+# Init
 
-The init functions in libsel4camkes are mostly used internally in the CAmkES
+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.
+control thread, which sets up the runtime and prepares the state for running
+the component's application code.

libsel4camkes/docs/marshall_macros.md

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

@@ -1,21 +1,24 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
 # Message queues
 
-libsel4camkes provides an implementation of a message queue transport
+`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. This 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, there exists only one sender and one receiver per channel.
+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 requires components to first initialise a
+The message queue libraries require components to first initialise a
 `seL4Msgqueue` CAmkES connection between components. Here's an example of how
 this is done:
 
@@ -32,10 +35,10 @@ 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;
@@ -45,41 +48,42 @@ assembly {
 ```
 
 From the example above, the sender is `baz`, and the receiver is `bar`. The IDs
-of this particular message queue channel is 1 for both components. It is
-possible to have multiple channels for a component, but each channel's ID must
-be different. The queue size of the message queue is 256 and can also be
-changed, however, it must be a power of two. The messages that will be
-transferred in the channel is of type `Message` as indicated by the dataport.
+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
-end of the channel by calling the appropriate function from the following:
+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. 
+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 a certain limit.
+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 two functions to check the status of the channel
-and possibly block on the channel waiting for a message.
+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 grab a
-message of the channel with the following.
+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);

libsel4camkes/docs/pid.md

@@ -1,14 +1,14 @@
 <!--
      Copyright 2021, Data61, CSIRO (ABN 41 687 119 230)
 
-     SPDX-License-Identifier: BSD-2-Clause
+     SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
 # PID
 
 This is a constant variable that tracks the ID of the CAmkES component.
-Although CAmkES or seL4 does not have a concept of processes, these variable is
+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?
+TODO Check this