search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
68 stars 37 forks source link

seL4 floating point compilation support #139

Open Bojan-Lukic opened 1 week ago

Bojan-Lukic commented 1 week ago

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 protected 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 commented 1 week ago

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.