The build seems to be currently broken:

...
-- Installing: /work/galois-sel4cp/build/imx8mm/release/sel4/install/libsel4/include
CMake Error at build/imx8mm/release/sel4/build/cmake_install.cmake:51 (file):
  file INSTALL cannot duplicate symlink

    /work/breakaway-seL4/libsel4/sel4_plat_include/imx8mm-evk

  at

    /work/galois-sel4cp/build/imx8mm/release/sel4/install/libsel4/include

  because: A directory already exists at that location

This seems to be related to something in https://github.com/BreakawayConsulting/seL4/tree/sel4cp-core-support because building the SDK works with this fork of the kernel: https://gitlab.com/coliasgroup/seL4/-/commits/rust-sel4cp?ref_type=heads

The build also works (==it compiles, I haven't tested it further) with the latest master of the kernel: https://github.com/seL4/seL4

Could the vanilla version of the kernel be used?

After making all the upgrades mentioned in build instructions build instructions build_sdk.py still fails to build monitor.
The reason is that cmake doesn't install required sel4 headers and kernel.elf to where they are expected to be.

The issue was observed while running the script in updated Docker container submitted recently

Do you have updated an build_sdk.py script? kernel scripts?

It seems that 457a83f causes the SDK to no longer build. Attempting to build the SDK will give the following error when it tries to build the kernel for the i.MX8MM-EVK:

CMake Error at build/imx8mm/release/sel4/build/cmake_install.cmake:46 (file):
  file INSTALL cannot duplicate symlink
  "/sel4cp/seL4/libsel4/sel4_plat_include/imx8mm-evk"
  at
  "/sel4cp/build/imx8mm/release/sel4/install/libsel4/include":
  File exists.

I believe this is fixed with seL4/seL4#629. Not sure whether this commit to seL4 should be cherry-picked or should update the kernel to mainline?

I think this also shows some basic CI that runs on each PR that simply attempts to build the SDK would be nice...

Can seL4 kernel be added as a submodule to Microkit?
That way the build is always reproducible - I know you have a version listed in the README, but this will inevitably become outdated.

There is currently a single patch to the seL4 kernel (seL4/seL4@c8ef493) that Microkit depends on.

What is the patch for?

The patch allows the boot-loader, which runs before seL4, to specify an extra region of device untyped at run-time when the boot-loader jumps to seL4.

Why is the patch necessary?

The boot-loader that Microkit systems use places all binaries in the expected places in physical memory before jumping to seL4. This includes binary for seL4 itself, the initial task (aka the monitor), as well as the binary for each protection domain.

However, when seL4 starts, it clears all physical memory that it defines as 'normal'. This means all memory in RAM (except seL4 itself and the initial task) will be cleared. Without the kernel patch, this would include the PD ELFs, meaning that when the PDs start, all the code for them will be gone.

In order to avoid this, we place all the PD ELFs in a contiguous region of physical memory that we tell seL4 at boot is 'device' memory, meaning that it won't clear it and hence the PD ELFs remain in tact after seL4 has booted.

How will the patch be removed?

Assuming there are no blocking issues, the new Rust capDL initialiser can be used to embed the binaries for each PD in the initialiser itself, while not copying the binaries around in memory. This allows us to have the memory efficiency desired without a patch to the kernel.

After the kernel patch is removed, a specific branch of seL4 will no longer be required. Note that Microkit may be pinned to a specific version of seL4 still, so not just any commit of the kernel will work.

The approach of using seL4_NBSendRecv in the event handler loop of libmicrokit when PDs essentially 'make' themselves passive by sending a message to the monitor is not ideal for multiple reasons.

1. It will not scale/work in multi-core setups. Given that it is a non-blocking send, a scenario may occur where the monitor is already dealing with a message from one PD (meaning that it is not waiting on an endpoint) and another PD that wants to make itself passive on another core which means the message will be lost.
2. It affects verification as it leads to assumptions needing to be made about the scheduling of the system.

This issue was found in the process of verifying the passive PD changes in Microkit.

The current proposed solution is to have synchronisation using notifications so that all PDs block until they receive a notification from the monitor that all PDs that needed to be converted to passive have completed. This means that no PDs start their init procedure until everything else in the system is also ready to start their init procedure. This should remove any concurrency issues such as what happens when a PD is in the middle of being converted to passive and another PD on a separate core tries to communicate with it, I believe this may lead to lost notifications.

This solution is not final as we have not implemented and evaluated it, however, from our internal discussions it I think it is the cleanest solution and should require minimal changes to Microkit.

The compilation worked fine after two hick-ups (I wasn't sure where to install the arm toolchain and had to upgrade pyoxidizer, both are sorted).

RUST_BACKTRACE=full ./release/sel4cp-sdk-1.2.6/bin/sel4cp
thread 'main' panicked at 'already borrowed: BorrowMutError', /home/siagraw/.cargo/registry/src/github.com-1ecc6299db9ec823/pyo3-0.17.3/src/gil.rs:433:45
stack backtrace:
   0:     0x7f52aead67b0 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::had334ddb529a2169
   1:     0x7f52aeb62c5e - core::fmt::write::h1aa7694f03e44db2
   2:     0x7f52aeac80f5 - <unknown>
   3:     0x7f52aead6575 - <unknown>
   4:     0x7f52aead937f - <unknown>
   5:     0x7f52aead90ba - std::panicking::default_hook::he03a933a0f01790f
   6:     0x7f52aead9b28 - std::panicking::rust_panic_with_hook::he26b680bfd953008
   7:     0x7f52aead98c7 - <unknown>
   8:     0x7f52aead6c5c - <unknown>
   9:     0x7f52aead95e2 - rust_begin_unwind
  10:     0x7f52adc920d3 - core::panicking::panic_fmt::he7679b415d25c5f4
  11:     0x7f52adc92393 - core::result::unwrap_failed::hb71caff146724b6b
  12:     0x7f52adf42086 - pyo3::gil::register_owned::h998547cdd21fc09e
  13:     0x7f52adf548c8 - pyo3::types::string::PyString::new::heccde79697d72abe
  14:     0x7f52adc94e4d - <unknown>
  15:     0x7f52adc96aa4 - pyembed::interpreter::MainPythonInterpreter::new::h6ff8b944283a0e80
  16:     0x7f52adc93345 - <unknown>
  17:     0x7f52adc93663 - <unknown>
  18:     0x7f52adc927d9 - <unknown>
  19:     0x7f52aeab91ee - std::rt::lang_start_internal::h167a33dedfef305a
  20:     0x7f52adc93655 - main

There was a brief discussion at the summit that maybe using XML for the system description is not the best (hjson anyone?:-) ). Either way, there should be proper grammar (EBNF?) and associated rules for the manifest language.

Why?

1. then switching between different manifest languages should be trivial
2. generating the manifest from other tools should be simpler (think SysMLv2/AADL -> microkit)
3. with proper rules we can ensure the manifest is well formed (I know you are already doing a number of checks, but we should be explicit about it)

As some may be aware, there has been significant development and change on Microkit outside of the mainline version. This currently lives here.

This issue outlines the roadmap of up-streaming all development changes such that the notion of a 'development' Microkit is gone, and everyone can build the systems they need to using the mainline Microkit.

Once each table entry has 'Merged' as 'Yes', this issue can be closed.

Below is outlining the main changes and the status of each (for clarity feature support and platform support is separate):

Note that everything above is subject to change.

Hello,
I am running intro problems running the ZCU102 example. I am using the Xilinx QEMU fork, and I can boot the sel4 test on the emulated board from Uboot using tftpboot (so I am reasonably confident that the emulator is set up correctly).

I am building the example with dev_build.py --board=zcu102 --example=hello

However, when I attempt to run the loader.img I get the following error:

# Starting application at 0x08000000 ...
LDR|INFO: altloader for seL4 starting
LDR|ERROR: mismatch on loader data structure magic number
...
Resetting CPU ...

The docs say that:

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

Can you advise how to run the hello world example on ZCU102?

seL4 enforces a maximum IRQ number for ARM and RISC-V platforms, we should check for this at build time to avoid an seL4 invocation error upon boot.

Depends on seL4/seL4#1207.

Currently Microkit supports 4K and 2MiB page sizes. It would be fairly easy to add 1GiB page sizes as well which would be useful especially for things like virtual machines.

Currently, there is some dependence on system headers:

It would be preferable, if the SDK is truly self-contained; then an empty sysroot would be sufficient to compile. I know, most many cross tool-chains do ship some header files, and often this works else just by leaking in the header from a glibc based toolchain (since we don't actually link something), but I'd much prefer not rely on any of that.

Hi, currently there is no easy way to configure the stack size. It would be nice to be able to set it without having to update and rebuild the sdk.

The Core Platform headers contain static inline functions. Calling a static inline function from Rust (or any non C language) is difficult, because I believe that static inline functions are not visible outside of their translation unit, and placing such functions in the same translation unit as the Rust code would practically amount to including a C compiler. Is the Core Platform intended to be used with languages other than C?

Currently, the MicroKit tool fails if symbols it plans to patch (e.g. microkit_name or those referred to by setvar_vaddr) aren't present. One example of a case where this is inconvenient is when a PD never actually uses microkit_name , and so the linker might exclude microkit_name from the final binary. This happens in Rust PDs for which the compiler can prove that they never panic.

In Rust, there is no way to instruct the linker to include certain unused symbols in the final binary without using unstable features.

I think the best solution is for the tool to permit such symbols to be absent in the binary.

Hello!

I am very excited about the new core platform! I tried to build the SDK following the instructions, but I am getting this error:

generating custom link library containing Python...
deriving custom config.c from 101 extension modules
compiling custom config.c to object file
running: "musl-gcc" "-O0" "-ffunction-sections" "-fdata-sections" "-fPIC" "-m64" "-I" "/tmp/libpython58Y2ML" "-Wall" "-Wextra" "-std=c99" "-DNDEBUG" "-DPy_BUILD_CORE" "-o" "/tmp/pyoxidizer-build-exe-packagingQ0Ofjv/config.o" "-c" "/tmp/libpython58Y2ML/config.c"
cargo:warning=In file included from /tmp/libpython58Y2ML/config.c:1:
cargo:warning=/tmp/libpython58Y2ML/Python.h:44:10: fatal error: crypt.h: No such file or directory
cargo:warning=   44 | #include <crypt.h>
cargo:warning=      |          ^~~~~~~~~
cargo:warning=compilation terminated.
exit status: 1


error occurred: Command "musl-gcc" "-O0" "-ffunction-sections" "-fdata-sections" "-fPIC" "-m64" "-I" "/tmp/libpython58Y2ML" "-Wall" "-Wextra" "-std=c99" "-DNDEBUG" "-DPy_BUILD_CORE" "-o" "/tmp/pyoxidizer-build-exe-packagingQ0Ofjv/config.o" "-c" "/tmp/libpython58Y2ML/config.c" with args "musl-gcc" did not execute successfully (status code exit status: 1).

Not quite sure where is the problem coming from, libcrypt-dev is installed, and a simple call to import crypt succeeds:

# ./pyenv/bin/python                           
Python 3.10.6 (main, Nov 14 2022, 16:10:14) [GCC 11.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import crypt
>>> 

I am building this on ubuntu:latest:

# cat /etc/lsb-release 
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=22.04
DISTRIB_CODENAME=jammy
DISTRIB_DESCRIPTION="Ubuntu 22.04.1 LTS

Hi, following up on #15 I am looking into adding support for RISCV, specifically for the Polarfire Icicle kit. Besides the obvious changes in build_sdk.py and makefiles (mostly replace the hardcoded arm toolchain with something configurable), what else do you expect to be the major pain points?

The loader seems to provide a good number of utilities (enable/disable mmu and such), but it is not clear how much are these used. Not sure how this changes for RISCV (the existing platforms don't support virtualization for example).

Some of this could be provided by OpenSbi, and in fact that is what the riscv version of the seL4 tests suite uses.

The same goes for the monitor - besides some of the debug prints it looks fairly generic, unless I am missing something?

Initial CI has been added just to double-check PRs that look like they don't break anything.

We will of course need proper CI that also tests the SDK. This will include

• Tests of basic functionality that do not depend on specific hardware. Some tests exist, but not enough.
• Building and executing (when possible) the examples for each hardware platform.
• Figuring out every dependency Microkit has and what version of each dependency to pin it to. This needs to be done systematically, the only way I know of doing that is via Nix. We could look into a Docker container as well.
• Checking that the Microkit tool still type checks with mypy.
• Documenting how contributors can reproduce each step of CI.
• From #62, we should also test using non-GCC tools to produce a Microkit system.

We should also discuss whether to make available a 'mainline' build of the SDK for download for those who want to use the latest version.

It is vital to have a guide for porting Microkit to a new hardware platform, it should outline everything needed to get Microkit working as well as what the project requires from contributors that want to upstream their own platform ports.

A (most-likely) non-exhaustive list is as follows:

• First have seL4 and seL4test working on the platform
• Add the platform to SUPPORTED_BOARDS in build_sdk.py.
• Add serial output (putc) functionality to the boot-loader.
  • Note that the boot-loader assumes that the UART is already turned on by the previous boot-loading stage. An assumption that is often true but not necessarily true.
• Add documentation in the manual for the platform.

Lastly, we need some of testing new platforms in CI. At a minimum, each example for a platform and tests should be built for the new platform. If we do have access to the hardware, we can also perform run-time tests.

Once the Renode simulator becomes more mature, we can look into using it to simulate platforms that we do not plan to have access to.

In the present version the callee must trust the callee to conform.

I believe the first callee is intended to be caller.

One of the goals of Microkit is to have minimal overhead with regards to memory usage. A number of design decisions have been made in order to make this possible. However, what we are missing is a systematic way of measuring the memory usage of a system, where the overheads are, and so on. The report created by the Microkit tool helps with this, but is not enough.

The goal would to have automated tests that run on each commit to Microkit that analyse and report regressions of memory efficiency.

Hello!

Is 32 bit ARM support on the roadmap for CP? Or is it strictly 64bit?

Hello!
What is the key for the interrupt numbers that are defined in .system? For example, the ethernet example for tqma8xqp1gb defines interrupts 112, 290 and 294. Looking at tqma8xqp1gb.dts, which is a device tree that seL4 presumably uses, there don't seem to be matching interrupts.

Similarly, the virt ARM example from Nick Spinale has a UART interrupt 33 but that number doesn't seem to match QEMU documentation / source code.

Does the kernel do any irq mapping, or should the numbers generally match what is in a datasheet/documentation for a particular board?

Hi, Microkit system description (XML) provides the map element, to map a memory region into protection domains. It has some attributes, including "setvar_vaddr", which specifies a symbol name in the program image (of type uintptr_t), which is rewritten to hold the start of the virtual address of the memory region. It's a nice means to declare constant decisions once in the high level system description, and make them available in the code.

An information gap we have with this, is that we sometimes need both the start of the virtual address for the memory region, and the size of that region. At the moment, we work around this, by assuming blocks are allocated contiguously, and deriving size from the gap between two addresses.

Instinctively, an additional map attribute might be apt to communicate size as well as the virtual address. But, I wonder if "size" is neither virtual nor physical specific, and would be the same value, and handy to know, in both contexts?

So, perhaps, maybe "memory_region" could provide a "setvar_size", to allow us to gain access to the size information? For example, something like:
memory_region name="shared_heap" size="0x200_000" setvar_size="shared_heap_size"/>

Hello!

I am porting an existing network driver code to sel4cp, and the driver has a couple of vTaskDelay() calls (it is for FreeRTOS).

Is there a recommended way of handling such case - e.g. I need my PD to suspend for a short time before continuing in execution?

I can think of the following options:

1. refactor the code so it fits the event driven paradigm of sel4cp (effectively a state machine) - not practical, the state machine size could get out of hand rather quickly
2. use pp_call to a timer to get current system time, and busy wait until the desired time elapses - rather inefficient
3. something else?

@Ivan-Velickovic @nspin

It is important to outline the philosophy and goals of Microkit in a transparent way. This has been partially done in various places, but not in any single central place like this repository.

This documentation should contain the general goals as well as an overview of the design of Microkit and all the components that make up Microkit (e.g loader, initial task, libmicrokit).

I believe there are a couple of ARM platforms (the Raspberry Pi 3 is one of them) that have a non-standard interrupt controller. This platforms are configured with HAVE_SET_TRIGGER to false, which means that the kernel invocation seL4_IRQControl_GetTrigger cannot be used.

Right now this isn't a problem for any of the supported platforms by Microkit, but it may be a problem in the future. This depends on seL4/seL4#1073 being solved.

Currently we need to manually declare the relevant channel numbers for each PD, for example here. The microkit should generate an appropriate header with the channel numbers from the system manifest. Each PD can then include the generated file. Generating .h files should be trivial, Rust modules might need some more thought.

If there are concerns about sharing these channel IDs, perhaps a header file for each PD can be generated.

Currently, https://trustworthy.systems/projects/microkit/tutorial/part0.html just recommends to download curl -L trustworthy.systems/Downloads/microkit_tutorial/sdk-linux-x64.tar.gz -o sdk.tar.gz. I would much prefer if the sdk would be versioned, with a list of all previous versions as well:

• trustworthy.systems/Downloads/microkit_tutorial/sdk-linux-x64-0.1.0.tar.gz
• trustworthy.systems/Downloads/microkit_tutorial/sdk-linux-x64-latest.tar.gz

Of course it lends itself to have a latest version, and refer to that in the tutorial.

I'm trying to build the zcu102 hello example with SEL4CP_CONFIG set to "release" but it fails with the error message:

Traceback (most recent call last):
  File "runpy", line 197, in _run_module_as_main
  File "runpy", line 87, in _run_code
  File "sel4coreplat.__main__", line 1781, in <module>
  File "sel4coreplat.__main__", line 1632, in main
  File "sel4coreplat.__main__", line 674, in build_system
  File "sel4coreplat.sel4", line 819, in emulate_kernel_boot_partial
  File "sel4coreplat.sel4", line 791, in _kernel_partial_boot
  File "sel4coreplat.sel4", line 718, in _kernel_device_addrs
  File "sel4coreplat.elf", line 442, in find_symbol
KeyError: 'No symbol named kernel_device_frames found'

I can build a "debug" binary w/o any issue.

I'm using Nataliya Korovkina's docker file. I'm using the latest sel4cp sources (commit 192c223).

The command I'm using:

PATH=$PATH:/usr/local/musl/aarch64/bin:/usr/local/gcc-x86_64-aarch64-none-elf/bin make BUILD_DIR=./release SEL4CP_SDK=/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6 SEL4CP_BOARD=zcu102 SEL4CP_CONFIG=release

The output prior to the error message:

aarch64-none-elf-gcc -c -mcpu=cortex-a53 -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall  -Wno-unused-function -Werror -I/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6/board/zcu102/release/include hello.c -o release/hello.o
aarch64-none-elf-ld -L/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6/board/zcu102/release/lib release/hello.o -lsel4cp -Tsel4cp.ld -o release/hello.elf
/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6/bin/sel4cp hello.system --search-path ./release --board zcu102 --config release -o ./release/loader.img -r ./release/report.txt

I'm getting a similar error message for other platforms (e.g., Odroid-C2).

Here are some additional tools and packages I had to install to get build_sdk.py to work on a fresh Ubuntu 18.04 install. (these are based on using the initial public release - I notice some more recent updates have added some of the missing python dependencies)

• pandoc: sudo apt install pandoc
• pdflatex: sudo apt install texlive-latex-base
• cmake: sudo apt install cmake - see note below about wrong cmake version
• ninja: sudo apt-get install ninja-build
• gcc-aarch64-linux-gnu: sudo apt-get install gcc-aarch64-linux-gnu
• dtc: sudo apt-get install device-tree-compiler
• pyyaml: ./pyenv/bin/pip install pyyaml
• pyfdt: ./pyenv/bin/pip install pyfdt
• jinja2: ./pyenv/bin/pip install jinja2
• xmllint: ./pyenv/bin/pip install libxml2-utils
• ply: ./pyenv/bin/pip install ply

Note about cmake:

• cmake >= 3.13 is required. apt installs cmake 3.10.2
• instructions for newer cmakes:
  • sudo apt-get update
  • sudo apt-get install apt-transport-https ca-certificates gnupg software-properties-common wget
  • wget -O - https://apt.kitware.com/keys/kitware-archive-latest.asc 2>/dev/null | sudo apt-key add -
  • sudo apt-add-repository 'deb https://apt.kitware.com/ubuntu/ bionic main'
  • sudo apt-get install cmake

Note about docs:

• I still got errors trying to build documentation, Font T1/cmr/m/n/10.95=ecrm1095 at 10.95pt not loadable: Metric (TFM) file not found.
• so I commented out build_doc and just built the sdk

Hi! What is required in order to support the SDK on other platforms (specifically on Raspberry Pi 4)?
Looking at the code base, looks like the board specific code is only the https://github.com/BreakawayConsulting/sel4cp/blob/main/loader/src/loader.c and https://github.com/BreakawayConsulting/sel4cp/blob/main/build_sdk.py

Would all platform specific details be part of the .system file connecting irqs and defining memory regions (such as in the ethernet example)?

Hi, if I have an application built on CAMKES, how would I convert such an application to a core-platform based one?
Specifically, is there an example of how to represent dataports, connections etc in the core-platform?

There is currently no API for doing cache operations on ARM platforms. This leads to code like this

which should not be necessary.

We could add simple wrappers such as microkit_arm_cache_clean and microkit_arm_cache_invalidate and so on, these would simply abstract away the VSpace cap since it's fixed.

However, I believe the default seL4 configurations for AArch64 also allow users to do some of these operations from user-space. Should these microkit_arm_cache_* APIs only call the system call if caching operations from user-space are not enabled? Are there any issues with this indirection? Should we be simple and only supply the system call wrappers and leave it to users to decide what to do?

It certainly leads to better performance.

Hello!
Just wondering - is there a migration plan for the Rust Core platform? It looks like @nspin made some tweaks to the seL4 kernel and to the Core Platform itself, but I am not sure how easy is to merge those changes here?

The cargo and rust part should be pretty independent, it would just be nice to use the same kernel and Core Platform SDK.

Since building the SDK requires a specific GCC toolchain, I was wondering whether it should be used for building the kernel as well? I notice that by default the kernel will be built with aarch64-linux-gnu- if it is installed, which is not the same toolchain that's being used for all the other components of seL4CP.

Context: I am a simple hobbyist who discovered seL4 a few days ago: I watched a number of videos on the seL4 youtube channel and read a few pages on https://docs.sel4.systems/.
I am now trying out sel4cp, and I just managed to build the hello example, resulting in some .img and .elf files. However I don't have a clue how to use them.

1. Could someone provide some pointers?
2. The code only mentions 2 supported boards (which I don't possess). Is it possible to boot in qemu?