Assuming you are talking about text mode VGA then having the kernel render to such a buffer is not particularly difficult. Instead of the 0xB8000 address though I would consider using the supposed multiboot video mode, and perhaps falling back to the buffer at 0xB8000 if no multiboot video mode provided, that would provide the most reliability. You will need to * Emulate the vt100 codes in the seL4 messages, or disable colored output (which I believe is all we use control codes for) * Handle end of line detection and scrolling Whilst not using multiboot an old slightly bitrotted user level example of what you are proposing is https://github.com/seL4/util_libs/blob/master/libplatsupport/src/plat/pc99/e... If you want to use a linear graphics mode though (and you don't want to change display modes later on) then obviously it's a little more complicated as you'll have to do font rendering. Not that rendering the equivalent of a monospaced text mode onto a linear graphics mode is particularly difficult though. Note that we currently have not written graphics support beyond the multiboot graphics mode that the kernel can request from its loader, in particular we do not have any code that would allow you to change the screen mode later on at user level. Asking the kernel to stop using its debug output device, to allow the user to start using wholly for its own purposes, is something that could be useful to add. Probably would have to be another 'debug' syscall, and could function as a dynamic enabling/disabling of kernel printing. Adrian On Mon 31-Jul-2017 5:23 PM, Andrew Warkentin wrote: On 7/28/17, Michal Podhradsky <mpodhradsky@galois.com><mailto: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. _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel