seL4 floating point compilation support

[Bojan-Lukic]

We are running the sel4 microkit with QEMU on NixOS 23.11 to implement a proof of concept system.

One of our applications requires trigonometric functions, hence we are using the math.h library in the c file of one of our protection domains. When trying to do a simple calculation with the sine function we get errors when building and running the system. Therefore, we assume that there are issues with either the library we are using or with certain types of floating point operations in seL4.

What floating point compilation does seL4 support and what is the right approach for using floating point operations?

[Ivan-Velickovic]

The qemu_virt_aarch64 platform has a kernel compiled with the CONFIG_HAVE_FPU configuration option and so the FPU and hence floating point operations should be available as far as I know.

Perhaps there is some FPU initialisation that seL4 is not doing and instead relying on the previous boot-loading stage to set it up.

Do you have one of the supported hardware platforms to run the proof of concept systems on? It would confirm whether it's a general issue or just specific to QEMU.

These are my initial thoughts but I will have a deeper look within the next couple of days.

[Bojan-Lukic]

Some more insights into the problem

We are using the environment from the microkit tutorial for the examples here. In this case, we tested the client protection domain. We encountered the same problems on two separate computers. When running the proof of concept on actual hardware we don't encounter any problems and can use functions from the math.h library. This gives us confidence that the problem is specific to QEMU.

Our platform information:

BOARD := qemu_arm_virt
MICROKIT_CONFIG := debug
BUILD_DIR := build

CPU := cortex-a53

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

Initially, we encountered following error when trying to compile:

aarch64-unknown-linux-gnu-ld -L/nix/store/zlzs9p7lj44yq3967x50fj0b6inxmcwk-microkit-sdk-unstable-2024-04-18/board/qemu_arm_virt/debug/lib build/printf.o build/util.o build/client.o -lmicrokit -Tmicrokit.ld -o build/client.elf
/nix/store/1ipzwr9yjnipk3j0b1ar801s0xlwi9yq-aarch64-unknown-linux-gnu-binutils-2.40/bin/aarch64-unknown-linux-gnu-ld: build/client.o: in function init':
/home/jans_vn/Documents/Wanjas_Lösung_Microkit/microkit-tutorial/tutorial/client.c:188: undefined reference tosin'
make: *** [Makefile:107: build/client.elf] Error 1

Thanks to @Vincer239 and with this solution, we figured out that adding the -lm flag to the build line in the Makfile resolves the problem:

$(BUILD_DIR)/client.elf: $(addprefix $(BUILD_DIR)/, $(CLIENT_OBJS))
    $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ -lm

The program compiles without errors. However, when trying to run the program after compiling, we now get a different error:

WORDLE SERVER: starting
CLIENT: starting
Welcome to the Wordle client!

Instruction before calculating exp()

MON|ERROR: received message 0x00000006 badge: 0x0000000000000002 tcb cap: 0x8000000000002909
MON|ERROR: faulting PD: client
Registers:
pc : 0x0000000000000000
spsr : 0x0000000060000040
x0 : 0x0000000000000026
x1 : 0x0000000000207150
x2 : 0x0000000000000026
x3 : 0xffffffffffffffff
x4 : 0x000000000020007c
x5 : 0x0000000000000000
x6 : 0x0000000000000000
x7 : 0xfffffffffffffff4
MON|ERROR: VMFault: ip=0x0000000000000000 fault_addr=0x0000000000000000 fsr=0x0000000082000006 (instruction fault)
MON|ERROR: ec: 0x00000020 Instruction Abort from a lower Exception level il: 1 iss: 0x00000006
<<seL4(CPU 0) [receiveIPC/142 T0x80bffe7400 "rootserver" @8a000310]: Reply object already has unexecuted reply!>>

Note that instead of sin(), we now tried a different function from the math.h library, namely exp(). The "Instruction before calculating exp()" line in the previous output is printed right before using the exp() function. It doesn't seem to make a difference which function is used, that is, both sin() as well as exp() lead to errors.

[Ivan-Velickovic]

Something strange seems to be going on as the instruction pointer and the fault address is zero.

I modified the 'hello' example for QEMU to use exp() and everything seems to work.

I'll try reproduce your test and see what happens.

[Ivan-Velickovic]

Okay, I can reproduce the issue.

The problem seems to be the toolchain, I am not sure if aarch64-unknown-linux-gnu will work as using GNU libmath/libc from that will mean it is expecting a Linux environment, which we do not have.

The aarch64-none-elf toolchain that is used to compile Microkit itself and is used in the example programs distributed with the Microkit SDK have newlibc packaged with them which is intended to be used in a freestanding environment.

The reason aarch64-unknown-linux-gnu or the other -*linux toolchains work in the first place is because we are not using any libc/OS functionality from the toolchain.

The reason the tutorial uses that toolchain is because it is available in package managers, unlike aarch64-none-elf.

If you want to keep using GCC and not bring your own libc/libmath, I believe it would be better to use aarch64-none-elf.

[Ivan-Velickovic]

@Bojan-Lukic did you run the same program on hardware as on QEMU, using the same toolchain?

[Bojan-Lukic]

@Ivan-Velickovic, yes. It was pretty much the same program on hardware as we ran on QEMU. We configured the system file with the board UART addresses and updated the Makefile with the board name/number instead of the qemu_arm_virt option. We loaded the separate ELF files on the board.
AFAIK the board required some configuration. If that is of interest, I can look into the details.