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/ega.c

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> 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
https://sel4.systems/lists/listinfo/devel