seL4
seL4 floating point compilation support
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?
What platform are you using, what errors do you get and did you check if your seL4 compile/config options match the ones you use for user space and the QEMU launch options?
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.
