Skip to content
/ microkit Public

Microkit - A simple operating system framework for the seL4 microkernel

License

Notifications You must be signed in to change notification settings

seL4/microkit

Repository files navigation

seL4 Microkit

The purpose of the seL4 Microkit is to enable system designers to create static software systems based on the seL4 microkernel.

The seL4 Microkit consists of three parts:

  • Microkit library
  • Microkit initial task
  • Microkit tool

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

This repository is the source for the Microkit SDK.

The development of Microkit is on-going, more information can be found on the roadmap.

If you are developing Microkit itself this is the repo you want!

If you are a system designer and want to use the Microkit SDK please download a pre-built SDK from the latest release. Please see the manual in the SDK for instructions on using the SDK itself.

The remainder of this README is for Microkit developers.

Developer system requirements

Building the Microkit SDK is supported on Linux (x86_64) and macOS (Apple Silicon/Intel).

This section attempts to list the packages or external development tools which are required during development. At this stage it may be incomplete. Please file an issue if additional packages are required.

  • Rust and Cargo
  • git
  • make
  • python3.9
  • python3.9-venv
  • cmake
  • ninja-build
  • ARM GCC compiler for none-elf; version 12.2.1 20221205
  • RISC-V GCC compiler for unknown-elf; version 13.2.0
  • device tree compiler
  • xmllint
  • qemu-system-aarch64

To build the documentation you also need

  • pandoc
  • pdflatex
  • texlive-latex-recommended
  • texlive-fonts-recommended
  • texlive-fonts-extra
  • texlive-latex-extra

On a Debian-like system you can do:

$ curl https://sh.rustup.rs -sSf | sh
$ rustup target add x86_64-unknown-linux-musl
$ sudo apt install build-essential git cmake ninja-build \
    device-tree-compiler libxml2-utils \
    pandoc texlive-latex-base texlive-latex-recommended \
    texlive-fonts-recommended texlive-fonts-extra \
    python3.9 python3.9-venv \
    qemu-system-arm qemu-system-misc \
    gcc-riscv64-unknown-elf

If you do not have Python 3.9 available, you can get it via the deadsnakes PPA: https://launchpad.net/~deadsnakes/+archive/ubuntu/ppa To use this:

$ sudo add-apt-repository ppa:deadsnakes/ppa
$ sudo apt update
$ sudo apt install python3.9 python3.9-venv

On macOS, with the Homebrew package manager you can do:

$ curl https://sh.rustup.rs -sSf | sh
$ brew tap riscv-software-src/riscv
$ brew install riscv-tools
$ brew install pandoc cmake dtc ninja qemu libxml2 [email protected] coreutils texlive qemu

Additonally, a number of Python libraries are needed. These should be installed using pip.

$ python3.9 -m venv pyenv
$ ./pyenv/bin/pip install --upgrade pip setuptools wheel
$ ./pyenv/bin/pip install -r requirements.txt

Note: It is a high priority of the authors to ensure builds are self-contained and repeatable. A high value is placed on using specifically versioned tools. At this point in time this is not fully realised, however it is a high priority to enable this in the near future.

The ARM toolchain is available from:

https://developer.arm.com/downloads/-/arm-gnu-toolchain-downloads.

Development is done with the aarch64-none-elf- toolchain.

On Linux x86-64 the following version is used: https://developer.arm.com/-/media/Files/downloads/gnu/12.2.rel1/binrel/arm-gnu-toolchain-12.2.rel1-x86_64-aarch64-none-elf.tar.xz?rev=28d5199f6db34e5980aae1062e5a6703&hash=F6F5604BC1A2BBAAEAC4F6E98D8DC35B

On macOS Apple Silicon/AArch64 the following version is used: https://developer.arm.com/-/media/Files/downloads/gnu/12.2.rel1/binrel/arm-gnu-toolchain-12.2.rel1-darwin-arm64-aarch64-none-elf.tar.xz?rev=c5523a33dc7e49278f2a943a6a9822c4&hash=6DC6989BB1E6A9C7F8CBFEAA84842FA1

On macOS Intel/x86-64 the following version is used: https://developer.arm.com/-/media/Files/downloads/gnu/12.2.rel1/binrel/arm-gnu-toolchain-12.2.rel1-darwin-x86_64-aarch64-none-elf.tar.xz?rev=09b11f159fc24fdda01e05bb32695dd5&hash=6AAF4239F28AE17389AB3E611DFFE0A6

seL4 Version

The SDK includes a binary of the seL4 kernel. During the SDK build process the kernel is build from source.

At this point in time there are some minor changes to the seL4 kernel required for Microkit. This is temporary, more details can be found here.

Please clone seL4 from:

https://github.com/seL4/seL4.git

The correct branch to use is microkit.

Testing has been performed using commit 4cae30a6ef166a378d4d23697b00106ce7e4e76f.

Building the SDK

$ ./pyenv/bin/python build_sdk.py --sel4=<path to sel4>

Using the SDK

After building the SDK you probably want to build a system! Please see the SDK user manual for documentation on the SDK itself.

When developing the SDK it is helpful to be able to build examples system quickly for testing purposes. The dev_build.py script can be used for this purpose. This script is not included in the SDK and is just meant for use of use of Microkit developers.

By default dev_build.py will use the example source directly from the source directory. In some cases you may want to test that the example source has been correctly included into the SDK. To test this pass --example-from-sdk to the build script.

By default dev_build.py will use the the Microkit tool directory from source (in tool/microkit). However, in some cases it is desirable to test the Microkit tool built into the SDK. In this case pass --tool-from-sdk to use the tool that is built into the SDK.

Finally, by default the dev_build.py script relies on the default Makefile dependecy resolution. However, in some cases it is useful to force a rebuild while doing SDK development. For example, the Makefile can't know about the state of the Microkit tool source code. To support this a --rebuild option is provided.

SDK Layout

The SDK is delivered as a tar.gz file.

The SDK top-level directory is microkit-sdk-$VERSION.

The directory layout underneath the top-level directory is:

doc/
doc/microkit_user_manual.pdf
bin/
bin/microkit
board/
board/$board/$config/include/
board/$board/$config/include/microkit.h
board/$board/$config/lib/
board/$board/$config/lib/libmicrokit.a
board/$board/$config/lib/microkit.ld
board/$board/$config/elf/
board/$board/$config/elf/loader.elf
board/$board/$config/elf/sel4.elf
board/$board/$config/elf/monitor.elf

The currently supported boards are:

  • imx8mm_evk
  • imx8mq_evk
  • maaxboard
  • odroidc2
  • odroidc4
  • qemu_virt_aarch64
  • qemu_virt_riscv64
  • star64
  • tqma8xqp1gb
  • zcu102

The currently supported configurations are:

  • release
  • debug
  • benchmark

Supported Boards

For documentation on each supported board see the manual.

Supported Configurations

For documentation on each supported board see the manual.