On 7/28/17, Michal Podhradsky mpodhradsky@galois.com wrote:
Hello,
I have a question about standard output. I have a camkes component than can write into text-mode VGA buffer (basically it follows this simple example http://wiki.osdev.org/Bare_Bones#Writing_a_kernel_in_C ) but I would like to be able to redirect the kernel messages during startup to be printed on screen using VGA buffer.
Once another component (either Linux in a VM, or some other camkes app) will initialize, it will be able to take control over the screen output (and for example show login window etc).
My questions is - is this possible with seL4? And if so, what would it entail?
I guess in the minimal version, I would have to provide a different implementation of seL4_DebugPutChar, is that correct?
The VGA standard seems to define the buffer to be at 0xB8000, so it should be consistent between x86 platforms.
Regards Michal
I'm planning to add an early video console to seL4 for UX/RT, the OS that I'm writing (it's going to be a pure Unix-like OS with a design similar to QNX, unlike all other L4-based OSes I'm aware of). It will be a desktop OS in addition to being an embedded OS, so I don't want to require people to hook up a serial console to figure out what's going on if something fails before the root server is loaded (the most likely failure would be a kernel that requires features not supported by the processor, which would probably almost never happen with embedded systems since the entire system image will be specifically cross-compiled for the correct microarchitecture whereas a desktop OS has to run on many different machines with different CPU features). My early console implementation will be an extremely minimal dumb terminal that will disable itself immediately before the root server is started and will provide no real API to user space. There will be no support for hardware text mode and no support for modesetting, meaning that the bootloader will have to set the mode and pass the framebuffer address to the kernel in order to use the early video console. I am also going to add a patch that writes the early kernel messages (up to when the root server is loaded) to some extra reserved pages in the bootinfo area so that user-mode code can access the early boot messages (as is possible on most other OSes).
Unrelated to this I'm also patching seL4 to support a boot process similar to that of QNX and Minix, where the kernel, root server, and all other required files for boot are contained within a single boot filesystem (or archive-like) image, rather than requiring stuff other than the kernel and root server to be embedded within an ELF section in the root server. I think a QNX/Minix-style boot process is a cleaner design, and it doesn't require development tools to be installed to build system images. The patch will change the kernel to assume the modules are located in a contiguous area following the kernel and make the kernel include this area as part of the "root server executable" region (the image will have two headers, one for the kernel and root server area and one for everything else). It will also add support for a variant of Multiboot2 adapted for modules within a single container image.