secc
/
seL4-microkit
mirror of https://github.com/seL4/microkit.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
seL4-microkit/docs/manual.md

37 KiB
Raw Blame History

title: Microkit User Manual (v1.2-pre) documentclass: article classoption:

  • english
  • 11pt
  • a4paper header-includes:
  • \usepackage[makeTitle,copyright]{sel4}
  • \usepackage{titlesec}
  • \newcommand{\sectionbreak}{\clearpage} subparagraph: yes numbersections: yes colorlinks: true

\maketitle \thispagestyle{empty} \clearpage \tableofcontents \pagenumbering{roman} \clearpage \pagenumbering{arabic} \setcounter{page}{1}

Introduction

The seL4 Microkit is a small and simple operating system (OS) built on the seL4 microkernel. Microkit is designed for building system with a static architecture. A static architecture is one where system resources are assigned up-front at system initialisation time.

Purpose

The Microkit is intended to:

  • provide a small and simple OS for a wide range of IoT, cyberphysical and other embedded use cases;
  • provide a reasonable degree of application portability appropriate for the targeted use cases;
  • make seL4-based systems easy to develop and deploy within the target areas;
  • leverage seL4's strong isolation properties to support a near-minimal trusted computing base (TCB);
  • retain seL4's trademark performance for systems built with it;
  • be, in principle, amenable to formal analysis of system safety and security properties (although such analysis is beyond the initial scope).

Overview

A Microkit system is built from a set of individual programs that are isolated from each other, and the system, in protection domains. Protection domains can interact by calling protected procedures or sending notifications.

Microkit is distributed as a software development kit (SDK). The SDK includes the tools, libraries and binaries required to build a Microkit system. The Microkit source is also available which allows you to customize or extend Microkit and produce your own SDK.

To build a Microkit system you will write some programs that use libmicrokit. Microkit programs are a little different to a typical process on a Linux-like operating system. Rather than a single main entry point, a program has four distinct entry points: init, notified and, potentially, protected, fault.

The individual programs are combined to produce a single bootable system image. The format of the image is suitable for loading by the target board's bootloader. The Microkit tool, which is provided as part of the SDK, is used to generate the system image.

The Microkit tool takes a system description as input. The system description is an XML file that specifies all the objects that make up the system.

Note: Microkit does not impose any specific build system; you are free to choose the build system that works best for you.

\clearpage

Document Structure

The Concepts chapter describes the various concepts that make up Microkit. It is recommended that you familiarise yourself with these concepts before trying to build a system.

The SDK chapter describes the software development kit, including its components and system requirements for use.

The Microkit tool chapter describes the host system tool used for generating a system image from the system description and user-programs.

The libmicrokit chapter describes the interfaces to the Microkit library.

The System Description File chapter describes the format of the system description XML file.

The Board Support Packages chapter describes each of the board support packages included in the SDK.

The Rationale chapter documents the rationale for some of the key design choices of in Microkit.

Concepts

This chapter describes the key concepts provided by Microkit.

As with any set of concepts there are words that take on special meanings. This document attempts to clearly describe all of these terms, however as the concepts are inter-related it is sometimes necessary to use a term prior to its formal introduction.

System

At the most basic level Microkit provides the platform for running a system on a specific board. As a user of Microkit you use the platform to create a software system that implements your use case. The system is described in a declarative configuration file, and the Microkit tool takes this system description as an input and produces an appropriate system image that can be loaded on the target board.

The key elements that make up a system are protection domains, memory regions and channels.

Protection Domains

A protection domain (PD) is the fundamental runtime abstraction in Microkit. It is analogous, but very different in detail, to a process on a UNIX system.

A PD provides a thread of control that executes within a fixed virtual address space. The isolation provided by the virtual address space is enforced by the underlying hardware MMU.

The virtual address space for a PD has mappings for the PD's program image along with any memory regions that the PD can access. The program image is an ELF file containing the code and data which implements the isolated component.

Microkit supports a maximum of 63 protection domains.

Entry points

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 up to four entry points:

  • init, notified which are required.
  • protected which is optional.
  • fault which is required if the PD has children.

When a 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.

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 only required for a parent PD.

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.

The overall computational model for a Microkit system is a set of isolated components reacting to incoming events.

Scheduling

The PD has a number of scheduling attributes that are configured in the system description:

  • priority (0 -- 254)
  • period (microseconds)
  • budget (microseconds)
  • passive (boolean)

The budget and period bound the fraction of CPU time that a PD can consume. Specifically, the budget specifies the amount of time for which the PD is allowed to execute. Once the PD has consumed its budget, it is no longer runnable until the budget is replenished; replenishment happens once every period and resets the budget to its initial value. This means that the maximum fraction of CPU time the PD can consume is budget/period.

The budget cannot be larger than the period. A budget that equals the period (aka. a "full" budget) behaves like a traditional time slice: After executing for a full period, the PD is preempted and put at the end of the scheduling queue of its priority. In other words, PDs with equal priorities and full budgets are scheduled round-robin with a time slice defined by the period.

The priority determines which of the runnable PDs to schedule. A PD is runnable if one of its entry points has been invoked and it has budget remaining in the current period. Runnable PDs of the same priority are scheduled in a round-robin manner.

The passive determines whether the PD is passive. A passive PD will have its scheduling context revoked after initialisation and then bound instead to the PD's notification object. This means the PD will be scheduled on receiving a notification, whereby it will run on the notification's scheduling context. When the PD receives a protected procedure by another PD or a fault caused by a child PD, the passive PD will run on the scheduling context of the callee.

Memory Regions

A memory region is a contiguous range of physical memory. A memory region may have a fixed physical address. For memory regions without a fixed physical address, the physical address is allocated as part of the build process. Typically, memory regions with a fixed physical address represent memory-mapped device registers.

Memory regions that are within main memory are zero-initialised.

The size of a memory region must be a multiple of a supported page size. The supported page sizes are architecture dependent. For example, on AArch64 architectures, Microkit support 4KiB and 2MiB pages. The page size for a memory region may be specified explicitly in the system description. If page size is not specified, the smallest supported page size is used.

Note: The page size also restricts the alignment of the memory region's physical address. A fixed physical address must be a multiple of the specified page size.

A memory region can be mapped into one or more protection domains. The mapping has a number of attributes, which include:

  • the virtual address at which the region is mapped in the PD
  • caching attributes (mostly relevant for device memory)
  • permissions (read, write and execute)

Note: When a memory region is mapped into multiple protection domains, the attributes used for different mappings may vary.

Channels

A channel enables two protection domains to interact using protected procedures or notifications. Each connects exactly two PDs; there are no multi-party channels.

When a channel is created between two PDs, a channel identifier is configured for each PD. The channel identifier is used by the PD to reference the channel. Each PD can refer to the channel with a different identifier. For example if PDs A and B are connected by a channel, A may refer to the channel using an identifier of 37 while B may use 42 to refer to the same channel.

Note: There is no way for a PD to directly refer to another PD in the system. PDs can only refer to other PDs indirectly if there is a channel between them. In this case, the channel identifier is effectively a proxy identifier for the other PD. So, to extend the prior example, A can indirectly refer to B via the channel identifier 37. 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

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. The protected procedure return value may also be up to 64 words.

When a protection domain calls a protected procedure, the procedure executes within the context of the providing protection domain.

A protected call is only possible if the callee has strictly higher priority than the caller. Transitive calls are possible, and as such a PD may call a protected procedure in another PD from a protected entry point. However the overall call graph between PDs must form a directed, acyclic graph. It follows that a PD can not call itself, even indirectly. For example, A calls B calls C is valid (subject to the priority constraint), while A calls B calls A is not valid.

When a protection domain is called, the protected entry point is invoked. The control returns to the caller when the protected entry point returns.

The caller is blocked until the callee returns. Protected procedures must execute in bounded time. It is intended that a future version of Microkit will enforce this condition through static analysis. In the present version the caller must trust the callee to conform.

In general, PPs are provided by services for use by clients that trust the protection domain to provide that service.

To call a PP, a PD calls microkit_ppcall passing the channel identifier and a message structure. 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

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.

To notify another PD, a PD calls microkit_notify, passing the channel identifier. When a PD receives a notification, the notified entry point is invoked with the appropriate channel identifier passed as an argument.

Unlike protected procedures, notifications can be sent in either direction on a channel regardless of priority.

Note: Notifications provide a mechanism for synchronisation between PDs, however this is not a blocking operation. 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.

Interrupt

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. Each hardware interrupt is assigned a channel identifier. In this way the protection domain can distinguish the hardware interrupt from other notifications. A specific hardware interrupt can only be associated with at most one protection domain. It should be noted that once a hardware interrupt has been received, it will not be received again until microkit_irq_ack is called. The seL4 kernel will mask the hardware interrupt until it has been acknowledged.

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.

Fault

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 system fault handler 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 system fault handler 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

Microkit is distributed as a software development kit (SDK).

The SDK includes support for one or more boards. Two configurations are supported for each board: debug and release. The debug configuration includes a debug build of the seL4 kernel to allow console debug output using the kernel's UART driver.

The SDK contains:

  • Microkit user manual (this document)
  • Microkit tool

Additionally, for each supported board configuration the following are provided:

  • libmicrokit
  • loader.elf
  • kernel.elf
  • monitor.elf

For some boards there are also examples provided in the examples directory.

The Microkit SDK does not provide, nor require, any specific build system. The user is free to build their system using whatever build system is deemed most appropriate for their specific use case.

The Microkit tool should be invoked by the system build process to transform a system description (and any referenced program images) into an image file which can be loaded by the target board's bootloader.

The ELF files provided as program images should be standard ELF files and have been linked against the provided libmicrokit.

System Requirements

The Microkit tool requires Linux x86_64, macOS x86_64 or macOS AArch64.

On Linux, the Microkit tool is statically linked and should run on any distribution. On macOS, the Microkit tool should run on macOS 10.12 (Sierra) or higher.

The Microkit tool does not depend on any additional system binaries.

Microkit Tool

The Microkit tool is available in bin/microkit.

The Microkit tool takes as input a system description. The format of the system description is described in a subsequent chapter.

Usage:

microkit [-h] [-o OUTPUT] [-r REPORT] --board [BOARD] --config CONFIG
         [--search-path [SEARCH_PATH ...]] system

The path to the system description file, board to build the system for, and configuration to build for must be provided.

The search paths provided tell the tool where to find any program images specified in the system description file.

In the case of errors, a diagnostic message shall be output to stderr and a non-zero code returned.

In the case of success, a loadable image file and a report shall be produced. The output paths for these can be specified by -o and -r respectively. The default output paths are loader.img and report.txt.

The loadable image will be a binary that can be loaded by the board's bootloader.

The report is a plain text file describing important information about the system. The report can be useful when debugging potential system problems. This report does not have a fixed format and may change between versions. It is not intended to be machine readable.

libmicrokit

All program images should link against libmicrokit.a.

The library provides the C runtime for the protection domain, along with interfaces for the Microkit APIs.

The component must provide the following functions:

void init(void);
void notified(microkit_channel ch);

If the protection domain provides a protected procedure it must also implement:

microkit_msginfo protected(microkit_channel ch, microkit_msginfo msginfo);

If the protection domain has child protection domains it must also implement:

void fault(microkit_pd pd, microkit_msginfo msginfo);

libmicrokit provides the following functions:

microkit_msginfo microkit_ppcall(microkit_channel ch, microkit_msginfo msginfo);
void microkit_notify(microkit_channel ch);
microkit_msginfo microkit_msginfo_new(seL4_Word label, seL4_Uint16 count);
seL4_Word microkit_msginfo_get_label(microkit_msginfo msginfo);
seL4_Word microkit_msginfo_get_count(microkit_msginfo msginfo);
void microkit_irq_ack(microkit_channel ch);
void microkit_pd_restart(microkit_pd pd, seL4_Word entry_point);
void microkit_pd_stop(microkit_pd pd);
void microkit_mr_set(seL4_Uint8 mr, seL4_Word value);
seL4_Word microkit_mr_get(seL4_Uint8 mr);

void init(void)

Every PD must expose an init entry point. This is called by the system at boot time.

void notified(microkit_channel ch)

The notified entry point is called by the system when a PD has received a notification on a channel.

ch identifies the channel which has been notified (and indirectly the PD that performed the notification).

Note: ch could identify an interrupt.

Channel identifiers are specified in the system configuration.

microkit_msginfo protected(microkit_channel ch, microkit_msginfo message)

The protected entry point is optional. This is invoked when another PD calls microkit_ppcall on a channel shared with the PD.

The ch argument identifies the channel on which the PP was invoked. Indirectly this identifies the PD performing the call. Channel identifiers are specified in the system configuration. Note: The channel argument is passed by the system and is unforgeable.

The message argument is the argument passed to the PP and is provided by the calling PD. The contents of the message is up to a pre-arranged protocol between the PDs. The message contents are opaque to the system. Note: The message is copied from the caller.

The returned message is the return value of the protected procedure. As with arguments, this is copied to the caller.

void fault(microkit_pd pd, microkit_msginfo msginfo)

The fault entry point depends on whether the given PD has children. This is invoked when a child PD causes a fault.

The pd argument identifies the child PD that caused the fault.

The msginfo argument is given by the seL4 kernel when a fault occurs and contains information as to what fault occurred.

You can use microkit_msginfo_get_label to deduce what kind of fault happened (for example, whether it was a user exception or a virtual memory fault). The type seL4_Fault_tag_t defines the kinds of faults for a given architecture that could occur. You can find the list of fault labels in the 'Faults' section of the seL4 manual.

microkit_msginfo microkit_ppcall(microkit_channel channel, microkit_msginfo message)

Performs a call to a protected procedure in a different PD. The ch argument identifies the protected procedure to be called. message is passed as argument to the protected procedure. Channel identifiers are specified in the system configuration.

The protected procedure's return data is returned in the microkit_msginfo.

void microkit_notify(microkit_channel ch)

Notify the channel ch. Channel identifiers are specified in the system configuration.

void microkit_irq_ack(microkit_channel ch)

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)

Creates a new message structure.

The message can be passed to microkit_ppcall or returned from protected.

uint64_t microkit_msginfo_get_label(microkit_msginfo message)

Returns the label from a message.

uint64_t microkit_msginfo_get_count(microkit_msginfo msginfo)

Returns the count of message registers in the message.

uint64_t microkit_mr_get(uint8_t mr)

Get a message register.

void microkit_mr_set(uint8_t mr, uint64_t value)

Set a message register.

System Description File

This section describes the format of the System Description File (SDF).

The system description file is an XML file that is provided as input to the microkit tool.

The root element of the XML file is system.

Within the system root element the following child elements are supported:

  • protection_domain
  • memory_region
  • channel

protection_domain

The protection_domain element describes a protection domain.

It supports the following attributes:

  • name: A unique name for the protection domain
  • pp: (optional) Indicates that the protection domain has a protected procedure; defaults to false.
  • priority: The priority of the protection domain (integer 0 to 254).
  • budget: (optional) The PD's budget in microseconds; defaults to 1,000.
  • period: (optional) The PD's period in microseconds; must not be smaller than the budget; defaults to the budget.
  • passive: (optional) Indicates that the protection domain will be passive and thus have its scheduling context removed after initialisation; defaults to false.

Additionally, it supports the following child elements:

  • program_image: (exactly one) Describes the program image for the protection domain.
  • 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.

The map element has the following attributes:

  • mr: Identifies the memory region to map.
  • vaddr: Identifies the virtual address at which to map the memory region.
  • perms: Identifies the permissions with which to map the memory region. Can be a combination of r (read), w (write), and x (eXecute), with the exception of a write-only mapping (just w).
  • cached: Determines if mapped with caching enabled or disabled. Defaults to true.
  • setvar_vaddr: Specifies a symbol in the program image. This symbol will be rewritten with the virtual address of the memory region.

The irq element has the following attributes:

  • irq: The hardware interrupt number.
  • id: The channel identifier. Must be at least 0 and less than 63.
  • trigger: (optional) Whether the IRQ is edge triggered ("edge") or level triggered ("level"). Defaults to "level". \

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.

memory_region

The memory_region element describes a memory region.

It supports the following attributes:

  • name: A unique name for the memory region
  • size: Size of the memory region in bytes (must be a multiple of the page size)
  • page_size: (optional) Size of the pages used in the memory region; must be a supported page size if provided. Defaults to the smallest page size for the target architecture.
  • phys_addr: (optional) The physical address for the start of the memory region (must be a multiple of the page size).

The memory_region element does not support any child elements.

Page sizes by architecture

Below are the available page sizes for each architecture that Microkit supports.

AArch64

  • 0x1000 (4KiB)
  • 0x200000 (2MiB)

channel

The channel element has exactly two end children elements for specifying the two PDs associated with the channel.

The end element has the following attributes:

  • pd: Name of the protection domain for this end.
  • id: Channel identifier in the context of the named protection domain. Must be at least 0 and less than 63.

The id is passed to the PD in the notified and protected entry points. The id should be passed to the microkit_notify and microkit_ppcall functions.

Board Support Packages

This chapter describes the board support packages that are available in the SDK.

i.MX8MM-EVK

Microkit produces a raw binary file, so when using U-Boot you must execute the image using:

=> go 0x41000000

i.MX8MQ-EVK

Microkit produces a raw binary file, so when using U-Boot you must execute the image using:

=> go 0x41000000

MaaXBoard

The MaaXBoard is a low-cost ARM SBC based on the NXP i.MX8MQ system-on-chip.

Microkit produces a raw binary file, so when using U-Boot you must execute the image using:

=> go 0x40480000

Odroid-C2

The HardKernel Odroid-C2 is an ARM SBC based on the Amlogic Meson S905 system-on-chip. It should be noted that the Odroid-C2 is no longer available for purchase but its successor, the Odroid-C4, is readily available at the time of writing.

Microkit produces a raw binary file, so when using U-Boot you must execute the image using:

=> go 0x20000000

Odroid-C4

The HardKernel Odroid-C4 is an ARM SBC based on the Amlogic Meson S905X3 system-on-chip.

Microkit produces a raw binary file, so when using U-Boot you must execute the image using:

=> go 0x20000000

TQMa8XQP 1GB

The TQMa8XQP is a system-on-module designed by TQ-Systems GmbH. The modules incorporates an NXP i.MX8X Quad Plus system-on-chip and 1GiB ECC memory.

TQ-Systems provide the MBa8Xx carrier board for development purposes. The instructions provided assume the use of the MBa8Xx carrier board. If you are using a different carrier board please refer to the appropriate documentation.

Note: There are different configured of the TQMa8Xx board which include different NXP SoCs and different memory configurations. Such modules are not supported.

The MBa8Xx provides access to the TQMa8XQP UART via UART-USB bridge. To access the UART connect a USB micro cable to port X13. The UART-USB bridge supports 4 individual UARTs; the UART is connected to the 2nd port.

By default the SoM will autoboot using U-Boot. Hit any key during the boot process to stop the autoboot.

A new board will autoboot to Linux. You will likely want to disable autoboot:

=> env set bootdelay -1
=> env save

The board can be reset by pressing switch S4 (located next to the Ethernet port). Alternatively, you can use the reset command from the U-Boot prompt.

During development the most convenient way to boot a Microkit image is via network booting. U-Boot support booting via the tftp protocol. To support this you'll want to configure the network. U-Boot supports DHCP, however it is often more reliable to explicitly set an IP address. For example:

=> env set ipaddr 10.1.1.2
=> env set netmask 255.255.255.0
=> env set serverip 10.1.1.1
=> env save

To use tftp you also need to set the file to load and the memory address to load it to:

=> env set bootfile loader.img
=> env set loadaddr 0x80280000
=> env save

The system image generated by the Microkit tool is a raw binary file.

An example sequence of commands for booting is:

=> tftpboot
=> dcache flush
=> icache flush
=> go ${loadaddr}

Rather than typing these each time you can create a U-Boot script:

=> env set microkit 'tftpboot; dcache flush; icache flush; go ${loadaddr}'
=> env save
=> run microkit

When debugging is enabled the kernel will use the same UART as U-Boot.

QEMU virt (AArch64)

Support is available for the virtual AArch64 QEMU platform. This is a platform that is not based on any specific SoC or hardware platform and is intended for simulating systems for development or testing.

It should be noted that the platform support is configured with 2GB of main memory and a single Cortex-A53 CPU.

You can use the following command to simulate a Microkit system:

$ qemu-system-aarch64 \
    -machine virt \
    -cpu cortex-a53 \
    -nographic \
    -serial mon:stdio \
    -device loader,file=[SYSTEM IMAGE],addr=0x70000000,cpu-num=0 \
    -m size=2G

You can find more about the QEMU virt platform in the QEMU documentation.

ZCU102

Initial support is available for the Xilinx ZCU102.

FIXME: Additional documentation required here.

The ZCU102 can run on a physical board or on an appropriate QEMU based emulator.

Microkit produces a raw binary file, so when using U-Boot you must execute the image using:

=> go 0x40000000

For simulating the ZCU102 using QEMU, use the following command:

$ qemu-system-aarch64 \
   -m size=4G  \
   -machine xlnx-zcu102 \
   -nographic \
   -device loader,file=[SYSTEM IMAGE],addr=0x40000000,cpu-num=0 \
   -serial mon:stdio

Adding Platform Support

The following section is a guide for adding support for a new platform to Microkit. Currently only AArch64 is supported in Microkit, so this guide assumes you are trying to add support for an AArch64 platform.

Prerequisites

Before you can start with adding platform support to Microkit, the platform must be supported by the seL4 kernel. You can find information on how to do so here.

Getting Microkit Components Working

The first step to adding Microkit support is to modify the build_sdk.py script in order to build the required artefacts for the new platform. This involves adding to the SUPPORTED_BOARDS list with the BoardInfo options containing the platform specific attributes. This should be fairly self-explanatory by looking at the existing entries with the exception of the loader_link_address.

The loader_link_address parameter specifies the physical address of where the bootloader for Microkit (which is responsible for setting up the system before seL4 starts) is going to be loaded. This address needs to match where in main memory the final system image is actually loaded (e.g where a previous bootloader such as U-Boot loads the image to). This means that the address is restricted to the platform's main memory region.

The other component of Microkit that is platform dependent is the loader itself. The loader will attempt to access the UART for debug output which requires a basic putc implementation. The UART device used in the loader should be the same as what is used for the seL4 kernel debug output.

Once you have patched the loader and the SDK build script, there should be no other changes required to have a working platform port. It is a good idea at this point to boot a hello world system to confirm the port is working.

If there are issues with porting the platform, please open an issue on GitHub.

Contributing Platform Support

Once you believe that the port works, you can open a pull request with required changes as well as documentation in the manual about the platform and how to run Microkit images on it.

Rationale

This section describes the rationales driving the Microkit design choices.

Overview

The seL4 microkernel provides a set of powerful and flexible mechanisms that can be used for building almost arbitrary systems. While minimising constraints on the nature of system designs and scope of deployments, this flexibility makes it challenging to design the best system for a particular use case, requiring extensive seL4 experience from developers.

The Microkit addresses this challenge by constraining the system architecture to one that provides enough features and power for its target usage class (IoT, cyberphysical and other embedded systems with a static architecture), enabling a much simpler set of developer-visible abstractions.

Protection Domains

PDs are single-threaded to keep the programming model and implementations simple, and because this serves the needs of most present use cases in the target domains. Extending the model to multithreaded applications (clients) is straightforward and can be done if needed. Extending to multithreaded services is possible but requires additional infrastructure for which we see no need in the near future.

Protected Procedure Priorities

The restriction of only calling to higher priority prevents deadlocks and reflects the notion that the callee operates on behalf of the caller, and it should not be possible to preempt execution of the callee unless the caller could be preempted as well.

This greatly simplifies reasoning about real-time properties in the system; in particular, it means that PPs can be used to implement resource servers, where shared resources are encapsulated in a component that ensures mutual exclusion, while avoiding unbounded priority inversions through the immediate priority ceiling protocol.

While it would be possible to achieve the same by allowing PPs between PDs of the same priority, this would be much harder to statically analyse for loop-freedom (and thus deadlock-freedom). The drawback is that we waste a part of the priority space where a logical entity is split into multiple PDs, eg to separate out a particularly critical component to formally verify it, when the complete entity would be too complex for formal verification. For the kinds of systems targeted by the Microkit, this reduction of the usable priority space is unlikely to cause problems.

Protected Procedure Argument Size

The limitation on the size of by-value arguments is forced by the (architecture-dependent) limits on the payload size of the underlying seL4 operations, as well as by efficiency considerations. The protected procedure payload should be considered as analogous to function arguments in the C language; similar limitations exist in the C ABIs (Application Binary Interfaces) of various platforms.


\

Limits

The limitation on the number of protection domains in the system is relatively arbitrary. Based on experience with the system and the types of systems being built it is possible for this to be increased in the future.

The limitation on the number of channels for a protection domain is based on the size of the notification word in seL4. Changing this to be larger than 64 would most likely require changes to seL4. The reason for why the limit is not a power of two is due to part of the notification word being for internal libmicrokit use.