On Thu, May 20, 2021 at 6:13 AM Ben Fiedler <sel4(a)bfiedler.ch> wrote:
I've recently found an interesting bug that only occurs when compiling in release
Use of the ZF_LOG library (for normal log output) leads to syscalls being made when the
These are invoked via musllibc's __stdio_write, which relies on __sysinfo being set
correctly for syscalls to
work. When compiling with RELEASE=OFF this works fine, however when compiling with
RELEASE=ON, __sysinfo is
not set (yet?), and subsequently leads to an illegal prefetch exception when
__stdio_write tries to invoke
Setting __sysinfo to sel4_vsyscall using gdb during runtime fixes this. I don't
really know the correct
place to fix this in the code, but I hope that you can provide some hints on where to fix
If you look in the CMake file capdl-loader-app/helpers.cmake you will
see that libsel4muslcsys is only linked into the capdl-loader-app
under debug builds. This library implements the registration of a set
of syscalls under __sysinfo and any printing would need to go through
that. Thus, the capdl-loader-app doesn't support log output via
ZF_LOG while RELEASE=ON.
RELEASE=ON essentially does 2 things currently: Turn off kernel debug
syscalls, and turn up optimization levels for the compiler. The
printing in the capdl-loader-app needs the seL4_DebugPutChar syscall,
so you would still need that syscall to turn on printing.
If you wanted to add printing when RELEASE=ON then you would need to
link libsel4muslcsys unconditionally, and edit main.c to call
init_bootinfo also, and you would need to also set KernelPrinting=ON.
Hope this helps.
Thanks a lot for your help!
Devel mailing list -- devel(a)sel4.systems
To unsubscribe send an email to devel-leave(a)sel4.systems