Skip to content

Commit

Permalink
[squash] partially address review feedback
Browse files Browse the repository at this point in the history
Signed-off-by: Gerwin Klein <[email protected]>
  • Loading branch information
lsf37 committed Feb 11, 2024
1 parent b83c0f0 commit d715011
Show file tree
Hide file tree
Showing 11 changed files with 95 additions and 84 deletions.
2 changes: 1 addition & 1 deletion libsel4camkes/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
25 changes: 13 additions & 12 deletions libsel4camkes/docs/allocator.md
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -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;
}
Expand All @@ -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
13 changes: 7 additions & 6 deletions libsel4camkes/docs/dataport.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,28 +6,29 @@

# 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,
Expand Down
14 changes: 7 additions & 7 deletions libsel4camkes/docs/dma.md
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -23,7 +23,7 @@ assembly {
composition {
component Foo bar;
}

configuration {
bar.dma_pool = 0x4000;
}
Expand Down
25 changes: 14 additions & 11 deletions libsel4camkes/docs/error.md
Original file line number Diff line number Diff line change
@@ -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);
Expand All @@ -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.
18 changes: 9 additions & 9 deletions libsel4camkes/docs/fault.md
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Empty file removed libsel4camkes/docs/gdb.md
Empty file.
9 changes: 5 additions & 4 deletions libsel4camkes/docs/init.md
Original file line number Diff line number Diff line change
@@ -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.
6 changes: 3 additions & 3 deletions libsel4camkes/docs/msgqueue.md
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,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;
Expand All @@ -60,7 +60,7 @@ int camkes_msgqueue_sender_init(int msgqueue_id, camkes_msgqueue_sender_t *sende
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);
Expand Down
17 changes: 8 additions & 9 deletions libsel4camkes/docs/ps_io_ops_t.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
SPDX-License-Identifier: BSD-2-Clause
-->

# `ps_io_ops_t`

CAmkES provides an implementation of the `ps_io_ops_t` as part
Expand Down Expand Up @@ -47,12 +47,12 @@ errors, but this is currently unsupported.
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
initialisation, and the interface responds to alloc and pin requests by handing
out the virtual and physical addresses for these regions.

Hardware memory management mechanisms (such as IOMMU or SMMU) are not currently
supported, but this will be implemented by also mapping the static DMA pool
memory into the hardware address spaces provided by the IOMMU implementation.
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.
Expand All @@ -74,7 +74,7 @@ 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 as the interface ACK function.
interrupt acknowledgment.

## `ps_io_port_ops_t`

Expand All @@ -83,10 +83,10 @@ interrupt acknowledgment as the interface ACK function.
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 imlementation of the IOPort interface looks up these
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.
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
Expand Down Expand Up @@ -115,4 +115,3 @@ 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.

Loading

0 comments on commit d715011

Please sign in to comment.