Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 44 additions & 7 deletions docs/manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -97,10 +97,11 @@ This document attempts to clearly describe all of these terms, however as the co

* [system](#system)
* [protection domain (PD)](#pd)
* [channel](#chan)
* [channel](#channel)
* [memory region](#mr)
* [notification](#notification)
* [protected procedure](#pp)
* [faults](#faults)

## System {#system}

Expand Down Expand Up @@ -128,15 +129,21 @@ Microkit supports a maximum of 63 protection domains.
Although a protection domain is somewhat analogous to a process, it has a considerably different program structure and life-cycle.
A process on a typical operating system will have a `main` function which is invoked by the system when the process is created.
When the `main` function returns the process is destroyed.
By comparison a protection domain has three entry points: `init`, `notify` and, optionally, `protected`.

By comparison a protection domain has up to four entry points:
* `init`, `notify` which are required.
* `protected`, `fault` which are optional.

When an Microkit system is booted, all PDs in the system execute the `init` entry point.

The `notified` entry point will be invoked whenever the protection domain receives a *notification* on a *channel*.
The `protected` entry point is invoked when a PD's *protected procedure* is called by another PD.
A PD does not have to provide a protected procedure, therefore the `protected` entry point is optional.
These entry points are described in more detail in subsequent sections.

The `fault` entry point is invoked when a PD that is a child of another PD causes a fault.
A PD does not have to have child PDs, therefore the `fault` entry point is optional.

These entry points are described in more detail in subsequent sections.

**Note:** The processing of `init` entry points is **not** synchronised across protection domains.
Specifically, it is possible for a high priority PD's `notified` or `protected` entry point to be called prior to the completion of a low priority PD's `init` entry point.
Expand Down Expand Up @@ -191,7 +198,7 @@ The mapping has a number of attributes, which include:
**Note:** When a memory region is mapped into multiple protection
domains, the attributes used for different mapping may vary.

## Channels
## Channels {#channel}

A *channel* enables two protection domains to interact using protected procedures or notifications.
Each connects exactly two PDs; there are no multi-party channels.
Expand All @@ -209,7 +216,7 @@ Similarly, **B** can refer to **A** via the channel identifier **42**.

The system supports a maximum of 63 channels and interrupts per protection domain.

### Protected procedure
### Protected procedure {#pp}

A protection domain may provide a *protected procedure* (PP) which can be invoked from another protection domain.
Up to 64 words of data may be passed as arguments when calling a protected procedure.
Expand Down Expand Up @@ -239,7 +246,7 @@ A *message* structure is returned from this function.
When a PD's protected procedure is invoked, the `protected` entry point is invoked with the channel identifier and message structure passed as arguments.
The `protected` entry point must return a message structure.

### Notification
### Notification {#notification}

A notification is a (binary) semaphore-like synchronisation mechanism.
A PD can *notify* another PD to indicate availability of data in a shared memory region if they share a channel.
Expand All @@ -253,7 +260,7 @@ Unlike protected procedures, notifications can be sent in either direction on a
If a PD notifies another PD, that PD will become scheduled to run (if it is not already), but the current PD does **not** block.
Of course, if the notified PD has a higher priority than the current PD, then the current PD will be preempted (but not blocked) by the other PD.

## Interrupts
## Interrupts {#irqs}

Hardware interrupts can be used to notify a protection domain.
The system description specifies if a protection domain receives notifications for any hardware interrupt sources.
Expand All @@ -268,6 +275,20 @@ Microkit does not provides timers, nor any *sleep* API.
After initialisation, activity in the system is initiated by an interrupt causing a `notified` entry point to be invoked.
That notified function may in turn notify or call other protection domains that cause other system activity, but eventually all activity indirectly initiated from that interrupt will complete, at which point the system is inactive again until another interrupt occurs.

## Faults {#faults}

Faults such as an invalid memory access or illegal instruction are delivered to the seL4 kernel which then forwards them to
a designated 'fault handler'. By default, all faults caused by protection domains go to the Monitor which simply prints out
details about the fault in a debug configuration.

When a protection domain is a child of another protection domain, the designated fault handler for the child is the parent
protection domain.

This means that whenever a fault is caused by a child PD, it will be delivered to the parent PD instead of the monitor via the
`fault` entry point. It is then up to the parent to decide how the fault is handled. The label of the given `msginfo` can be
used to determine what kind of fault occurred. You can find more information about decoding the fault in the 'Faults' section
of the seL4 manual.

# SDK {#sdk}

Microkit is distributed as a software development kit (SDK).
Expand Down Expand Up @@ -414,6 +435,14 @@ Channel identifiers are specified in the system configuration.

Acknowledge the interrupt identified by the specified channel.

## `void microkit_pd_restart(microkit_pd id, uintptr_t entry_point)`

Restart the execution of a child protection domain with ID `id` at the given `entry_point`.
This will set the program counter of the child protection domain to `entry_point`.

## `void microkit_pd_stop(microkit_pd id)`

Stop the execution of the child protection domain with ID `id`.

## `microkit_msginfo microkit_msginfo_new(uint64_t label, uint16_t count)`

Expand Down Expand Up @@ -472,6 +501,7 @@ Additionally, it supports the following child elements:
* `map`: (zero or more) describes mapping of memory regions into the protection domain.
* `irq`: (zero or more) describes hardware interrupt associations.
* `setvar`: (zero or more) describes variable rewriting.
* `protection_domain`: (zero or more) describes a child protection domain.

The `program_image` element has a single `path` attribute describing the path to an ELF file.

Expand All @@ -494,6 +524,13 @@ The `setvar` element has the following attributes:
* `symbol`: Name of a symbol in the ELF file.
* `region_paddr`: Name of an MR. The symbol's value shall be updated to this MR's physical address.

The `protection_domain` element the same attributes as any other protection domain as well as:
* `id`: The ID of the child for the parent to refer to.

Child protection domains have their faults handled by the parent protection domain itself instead of the Microkit monitor.
The parent protection domain is able to control the child's thread allowing it to stop it or restart it using the
Microkit API.

## `memory_region`

The `memory_region` element describes a memory region.
Expand Down
63 changes: 63 additions & 0 deletions example/qemu_virt_aarch64/hierachy/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
#
# Copyright 2021, Breakaway Consulting Pty. Ltd.
#
# SPDX-License-Identifier: BSD-2-Clause
#
ifeq ($(strip $(BUILD_DIR)),)
$(error BUILD_DIR must be specified)
endif

ifeq ($(strip $(MICROKIT_SDK)),)
$(error MICROKIT_SDK must be specified)
endif

ifeq ($(strip $(MICROKIT_BOARD)),)
$(error MICROKIT_BOARD must be specified)
endif

ifeq ($(strip $(MICROKIT_CONFIG)),)
$(error MICROKIT_CONFIG must be specified)
endif

TOOLCHAIN := aarch64-none-elf

CPU := cortex-a53

CC := $(TOOLCHAIN)-gcc
LD := $(TOOLCHAIN)-ld
AS := $(TOOLCHAIN)-as
MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit

RESTARTER_OBJS := restarter.o
CRASHER_OBJS := crasher.o
HELLO_OBJS := hello.o

BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG)

IMAGES := restarter.elf crasher.elf hello.elf
CFLAGS := -mcpu=$(CPU) -mstrict-align -nostdlib -ffreestanding -g -O3 -Wall -Wno-unused-function -Werror -I$(BOARD_DIR)/include
LDFLAGS := -L$(BOARD_DIR)/lib
LIBS := -lmicrokit -Tmicrokit.ld

IMAGE_FILE = $(BUILD_DIR)/loader.img
REPORT_FILE = $(BUILD_DIR)/report.txt

all: $(IMAGE_FILE)

$(BUILD_DIR)/%.o: %.c Makefile
$(CC) -c $(CFLAGS) $< -o $@

$(BUILD_DIR)/%.o: %.s Makefile
$(AS) -g -mcpu=$(CPU) $< -o $@

$(BUILD_DIR)/restarter.elf: $(addprefix $(BUILD_DIR)/, $(RESTARTER_OBJS))
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@

$(BUILD_DIR)/crasher.elf: $(addprefix $(BUILD_DIR)/, $(CRASHER_OBJS))
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@

$(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS))
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@

$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) hierachy.system
$(MICROKIT_TOOL) hierachy.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
19 changes: 19 additions & 0 deletions example/qemu_virt_aarch64/hierachy/crasher.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <microkit.h>

void init(void)
{
int *x = 0;
microkit_dbg_puts("crasher, starting\n");
/* Crash! */
*x = 1;
}

void notified(microkit_channel ch)
{
}
16 changes: 16 additions & 0 deletions example/qemu_virt_aarch64/hierachy/hello.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <microkit.h>

void init(void)
{
microkit_dbg_puts("hello, world\n");
}

void notified(microkit_channel ch)
{
}
17 changes: 17 additions & 0 deletions example/qemu_virt_aarch64/hierachy/hierachy.system
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--
Copyright 2021, Breakaway Consulting Pty. Ltd.

SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<protection_domain name="restarter" priority="254">
<program_image path="restarter.elf" />
<protection_domain name="crasher" priority="253" id="1">
<program_image path="crasher.elf" />
</protection_domain>
<protection_domain name="hello" priority="1" id="2">
<program_image path="hello.elf" />
</protection_domain>
</protection_domain>
</system>
58 changes: 58 additions & 0 deletions example/qemu_virt_aarch64/hierachy/restarter.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <stdint.h>
#include <microkit.h>

static uint8_t restart_count = 0;

static char decchar(unsigned int v)
{
return '0' + v;
}

static void put8(uint8_t x)
{
char tmp[4];
unsigned i = 3;
tmp[3] = 0;
do {
uint8_t c = x % 10;
tmp[--i] = decchar(c);
x /= 10;
} while (x);
microkit_dbg_puts(&tmp[i]);
}

void init(void)
{
microkit_dbg_puts("restarter: starting\n");
}

void notified(microkit_channel ch)
{
}

seL4_MessageInfo_t protected(microkit_channel ch, microkit_msginfo msginfo)
{
microkit_dbg_puts("restarter: received protected message\n");

return microkit_msginfo_new(0, 0);
}

void fault(microkit_pd id, microkit_msginfo msginfo)
{
microkit_dbg_puts("restarter: received fault message for pd: ");
put8(id);
microkit_dbg_puts("\n");
restart_count++;
if (restart_count < 10) {
microkit_pd_restart(id, 0x200000);
microkit_dbg_puts("restarter: restarted\n");
} else {
microkit_pd_stop(id);
microkit_dbg_puts("restarter: too many restarts - PD stopped\n");
}
}
45 changes: 45 additions & 0 deletions libmicrokit/include/microkit.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,19 +12,22 @@
#include <sel4/sel4.h>

typedef unsigned int microkit_channel;
typedef unsigned int microkit_pd;
typedef seL4_MessageInfo_t microkit_msginfo;

#define MONITOR_EP 5
#define BASE_OUTPUT_NOTIFICATION_CAP 10
#define BASE_ENDPOINT_CAP 74
#define BASE_IRQ_CAP 138
#define BASE_TCB_CAP 202

#define MICROKIT_MAX_CHANNELS 63

/* User provided functions */
void init(void);
void notified(microkit_channel ch);
microkit_msginfo protected(microkit_channel ch, microkit_msginfo msginfo);
void fault(microkit_channel ch, microkit_msginfo msginfo);

extern char microkit_name[16];
/* These next three variables are so our PDs can combine a signal with the next Recv syscall */
Expand All @@ -42,6 +45,19 @@ void microkit_dbg_putc(int c);
*/
void microkit_dbg_puts(const char *s);

static inline void microkit_internal_crash(seL4_Error err)
{
/*
* Currently crash be dereferencing NULL page
*
* Actually derference 'err' which means the crash reporting will have
* `err` as the fault address. A bit of a cute hack. Not a good long term
* solution but good for now.
*/
int *x = (int *)(seL4_Word) err;
*x = 0;
}

static inline void microkit_notify(microkit_channel ch)
{
seL4_Signal(BASE_OUTPUT_NOTIFICATION_CAP + ch);
Expand All @@ -52,6 +68,35 @@ static inline void microkit_irq_ack(microkit_channel ch)
seL4_IRQHandler_Ack(BASE_IRQ_CAP + ch);
}

static inline void microkit_pd_restart(microkit_pd pd, seL4_Word entry_point)
{
seL4_Error err;
seL4_UserContext ctxt = {0};
ctxt.pc = entry_point;
err = seL4_TCB_WriteRegisters(
BASE_TCB_CAP + pd,
seL4_True,
0, /* No flags */
1, /* writing 1 register */
&ctxt
);

if (err != seL4_NoError) {
microkit_dbg_puts("microkit_pd_restart: error writing TCB registers\n");
microkit_internal_crash(err);
}
}

static inline void microkit_pd_stop(microkit_pd pd)
{
seL4_Error err;
err = seL4_TCB_Suspend(BASE_TCB_CAP + pd);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_pd_stop: error writing TCB registers\n");
microkit_internal_crash(err);
}
}

static inline microkit_msginfo microkit_ppcall(microkit_channel ch, microkit_msginfo msginfo)
{
return seL4_Call(BASE_ENDPOINT_CAP + ch, msginfo);
Expand Down
Loading