We have hit another wall with the seL4 development. We’ve been trying to benchmark the system based on the intra-address space IPC , inter-address space IPC, and memory mapping but we are having trouble in an area that we didn’t think we’d have trouble in.
We have been relying on the built in test structure. This structure relies on a driver file, a parent testing file, the configuration with a regular expression to decide which test to run, and the test code itself. We created a custom test function in the ipc.c file which holds all of the default ipc tests, and that all works fine. The problem is when we run the test, there is no output without allowing the debug in the configuration. We have come up with several ideas as to why, but have yet to really fix it to where we can printf() from inside of a test. It seems to be squelched.
One theory why this is happening is because the capability for printing is not being passed to the spawned child process from the main driver. The function (aptly named something along the lines of …_spawn_process) creates the process after first setting up capabilities for the process to be created. We do not see any capabilities for printing in these arguments, but that doesn’t explain why it would work if kernel debugging is set to true.
The other reason we are considering is that there is an area of code that is surrounded by an #ifdef that is a putchar sort of function. This function calls a systemcall that contains assembly code to put a character to the screen, a.k.a. print. The problem is that when we define this function explicitly without the debug conditional statement, an error shows that it is an invalid system call. This could be because of an uninitialized driver. The driver for the screen itself may be disabled or inaccessible by that specific function if debugging is not active. Of course this requires more investigation.
Finally we also are unable to get the image to print anything on bare metal. We have created a stable image using Syslinux, but the only output is related to the boot process before the rest of the diagnostic is sent through serial. We have tried various settings in Syslinux and have just about ruled that out. The issue may be similar to the one mentioned above to where all of the test output is being routed to serial either through direct code saying to go through serial if it is the test program, or through some sort of VGA/EGA definition in a system call that defines the output path as the serial port rather than the console. Either way, it is impossible to get real numbers on Qemu.
Comments