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
Hey Michal,
(1) The IBM-PC compatible build of the kernel currently uses the ?serial via the IO port interface. To use the VGA buffer, you'd have to do the work of getting the VGA alphanumeric-mode buffer mapped in at boot, and then write the code to print to the buffer.
(1a) I'd recommend doing this in userspace as part of your root task though, since there's no real advantage (that I can glean) to adding a VGA framebuffer driver to the kernel, unless you have no machines with serial ports, which is probably why you're trying to do this, I'd guess.
(2) Serializing access to hardware between the kernel and other entities is a difficult problem if you also need to preserve trustworthiness proprerties of the kernel. If you use a shared lock between the kernel and userspace for example, you open up a very obvious DoS attack against the kernel.
(3) It is possible, but you'd have to do a the plumbing yourself, yes. Consider doing this in your root task or as part of your userspace environment on top of seL4.
(4) It looks like you'd have to implement both putConsoleChar and putDebugChar, although they do exactly the same thing
(5) Yes, the VGA function is exposed at the same address on all IBM-PC compatibles, no worries
--Hope I helped,
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
________________________________ From: Devel devel-bounces@sel4.systems on behalf of Michal Podhradsky mpodhradsky@galois.com Sent: 29 July 2017 07:42 To: devel@sel4.systems Subject: [seL4] VGA buffer as stdout
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
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.
Well, I don't see any reason why the current kernel design would prohibit any of those goals, aside from the fact that we don't have a VGA driver in the kernel currently -- more power to you
Let me know if you happen upon any roadblocks, and thanks for bringing this kernel log design issue back into my attention. I suspect that this desire to pass the kernel's log messages on to userspace is something that will be requested a bit more in the future as people begin implementing more OS environments on top of seL4. Good looking out~
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
________________________________________ From: Devel devel-bounces@sel4.systems on behalf of Andrew Warkentin andreww591@gmail.com Sent: 31 July 2017 17:23 To: devel@sel4.systems Subject: Re: [seL4] VGA buffer as stdout
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
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.commailto: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.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 8/2/17, Adrian.Danis@data61.csiro.au Adrian.Danis@data61.csiro.au wrote:
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.
Like I said before I am planning to exclusively use a linear framebuffer rather than hardware text mode (which is a relic from an era when hardware wasn't powerful enough to do software text modes with reasonable performance, and I believe it's not supported at all under UEFI), and I'm planning to have it just emulate a dumb terminal (i.e. no escape codes; I don't want to bloat the kernel with a VT100 emulator just for displaying early boot messages). I was thinking of using the framebuffer console code from coreboot's libpayload (which only emulates a dumb terminal and is very lightweight).
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.
I was going to have the kernel automatically disable the early console immediately before it loads the root server, so there would be no need for an API (at least not under UX/RT). UX/RT's root server will contain its own early console emulator (possibly also based on that of libpayload) that will provide a minimal subset of a Unix terminal device to programs run during early boot (initializing the console emulator will be the first thing that the root server does). A full-featured DRM/DRI graphics driver and console emulator will take over before the root volume is mounted.
Hi Adrian, Kofi,
I followed your advice, and just as a proof of concept I redefined putConsoleChar from here: https://github.com/seL4/seL4/blob/master/src/plat/pc99/machine/io.c#L38 On top of printing on serial port, I added a line with text_ega_putchar((int) a); - so now the character is printed both on serial out and VGA screen.
I added the scrolling etc functions from https://github.com/seL4/util_libs/blob/master/libplatsupport/src/plat/pc99/e... to take care of line wraps and control characters (\n, \t, etc). Then I compiled the basic keyboard camkes example: https://github.com/seL4/camkes/tree/master/apps/keyboard and I run the program in qemu with -vga -std option.
I can see the kernel booting up on the screen as well as the serial out, but as soon as sel4 drops into userspace ("Starting node #0 with APIC ID 0") , it stops outputting anything (user program not running?);
The screenshot is here: https://drive.google.com/file/d/0B8h93vAE2c4ibmRKQkdZU3EtcUk/view?usp=sharin...
Any ideas what am I missing?
Regards M
On Wed, Aug 2, 2017 at 4:18 AM, Andrew Warkentin andreww591@gmail.com wrote:
On 8/2/17, Adrian.Danis@data61.csiro.au Adrian.Danis@data61.csiro.au wrote:
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.
Like I said before I am planning to exclusively use a linear framebuffer rather than hardware text mode (which is a relic from an era when hardware wasn't powerful enough to do software text modes with reasonable performance, and I believe it's not supported at all under UEFI), and I'm planning to have it just emulate a dumb terminal (i.e. no escape codes; I don't want to bloat the kernel with a VT100 emulator just for displaying early boot messages). I was thinking of using the framebuffer console code from coreboot's libpayload (which only emulates a dumb terminal and is very lightweight).
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.
I was going to have the kernel automatically disable the early console immediately before it loads the root server, so there would be no need for an API (at least not under UX/RT). UX/RT's root server will contain its own early console emulator (possibly also based on that of libpayload) that will provide a minimal subset of a Unix terminal device to programs run during early boot (initializing the console emulator will be the first thing that the root server does). A full-featured DRM/DRI graphics driver and console emulator will take over before the root volume is mounted.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hello,
I tested the code on a real hardware, and it ends at the same point - no output after "Starting node #0..."
Can you replicate the results?
M
On Tue, Aug 8, 2017 at 2:09 PM, Michal Podhradsky mpodhradsky@galois.com wrote:
Hi Adrian, Kofi,
I followed your advice, and just as a proof of concept I redefined putConsoleChar from here: https://github.com/seL4/seL4/ blob/master/src/plat/pc99/machine/io.c#L38 On top of printing on serial port, I added a line with text_ega_putchar((int) a); - so now the character is printed both on serial out and VGA screen.
I added the scrolling etc functions from https://github.com/seL4/util_ libs/blob/master/libplatsupport/src/plat/pc99/ega.c to take care of line wraps and control characters (\n, \t, etc). Then I compiled the basic keyboard camkes example: https://github.com/seL4/camkes/tree/master/apps/keyboard and I run the program in qemu with -vga -std option.
I can see the kernel booting up on the screen as well as the serial out, but as soon as sel4 drops into userspace ("Starting node #0 with APIC ID 0") , it stops outputting anything (user program not running?);
The screenshot is here: https://drive.google.com/file/d/ 0B8h93vAE2c4ibmRKQkdZU3EtcUk/view?usp=sharing
Any ideas what am I missing?
Regards M
On Wed, Aug 2, 2017 at 4:18 AM, Andrew Warkentin andreww591@gmail.com wrote:
On 8/2/17, Adrian.Danis@data61.csiro.au Adrian.Danis@data61.csiro.au wrote:
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.
Like I said before I am planning to exclusively use a linear framebuffer rather than hardware text mode (which is a relic from an era when hardware wasn't powerful enough to do software text modes with reasonable performance, and I believe it's not supported at all under UEFI), and I'm planning to have it just emulate a dumb terminal (i.e. no escape codes; I don't want to bloat the kernel with a VT100 emulator just for displaying early boot messages). I was thinking of using the framebuffer console code from coreboot's libpayload (which only emulates a dumb terminal and is very lightweight).
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.
I was going to have the kernel automatically disable the early console immediately before it loads the root server, so there would be no need for an API (at least not under UX/RT). UX/RT's root server will contain its own early console emulator (possibly also based on that of libpayload) that will provide a minimal subset of a Unix terminal device to programs run during early boot (initializing the console emulator will be the first thing that the root server does). A full-featured DRM/DRI graphics driver and console emulator will take over before the root volume is mounted.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
As far as I know, to interface with the VGA hardware, all you'd need is
* Physical memory access capabilities that allow your driver thread access to video memory and perhaps also the video bios
* I/O access capabilities that will let you access the VGA's I/O ports (0x3B0 through 0x3DF if I remember correctly).
Beyond that, just read the VGA specs so you know how to actually interface with the hardware itself. From seL4's perspective you just need to be sure your driver has the proper capabilities to do so.
On Tue, Aug 15, 2017 at 12:11 PM, Michal Podhradsky mpodhradsky@galois.com wrote:
Hello,
I tested the code on a real hardware, and it ends at the same point - no output after "Starting node #0..."
Can you replicate the results?
M
On Tue, Aug 8, 2017 at 2:09 PM, Michal Podhradsky mpodhradsky@galois.com wrote:
Hi Adrian, Kofi,
I followed your advice, and just as a proof of concept I redefined putConsoleChar from here: https://github.com/seL4/seL4/b lob/master/src/plat/pc99/machine/io.c#L38 On top of printing on serial port, I added a line with text_ega_putchar((int) a); - so now the character is printed both on serial out and VGA screen.
I added the scrolling etc functions from https://github.com/seL4/util_l ibs/blob/master/libplatsupport/src/plat/pc99/ega.c to take care of line wraps and control characters (\n, \t, etc). Then I compiled the basic keyboard camkes example: https://github.com/seL4/camkes/tree/master/apps/keyboard and I run the program in qemu with -vga -std option.
I can see the kernel booting up on the screen as well as the serial out, but as soon as sel4 drops into userspace ("Starting node #0 with APIC ID 0") , it stops outputting anything (user program not running?);
The screenshot is here: https://drive.google.com/file/ d/0B8h93vAE2c4ibmRKQkdZU3EtcUk/view?usp=sharing
Any ideas what am I missing?
Regards M
On Wed, Aug 2, 2017 at 4:18 AM, Andrew Warkentin andreww591@gmail.com wrote:
On 8/2/17, Adrian.Danis@data61.csiro.au Adrian.Danis@data61.csiro.au wrote:
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.
Like I said before I am planning to exclusively use a linear framebuffer rather than hardware text mode (which is a relic from an era when hardware wasn't powerful enough to do software text modes with reasonable performance, and I believe it's not supported at all under UEFI), and I'm planning to have it just emulate a dumb terminal (i.e. no escape codes; I don't want to bloat the kernel with a VT100 emulator just for displaying early boot messages). I was thinking of using the framebuffer console code from coreboot's libpayload (which only emulates a dumb terminal and is very lightweight).
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.
I was going to have the kernel automatically disable the early console immediately before it loads the root server, so there would be no need for an API (at least not under UX/RT). UX/RT's root server will contain its own early console emulator (possibly also based on that of libpayload) that will provide a minimal subset of a Unix terminal device to programs run during early boot (initializing the console emulator will be the first thing that the root server does). A full-featured DRM/DRI graphics driver and console emulator will take over before the root volume is mounted.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hey Michal,
Sorry I'm so late in getting back to you:
So the message you see there is printed by the kernel in smp_sys.c (https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/smp_sys.c#L66), and this function is called by (https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/boot_sys.c#L610...).
Just beneath that, there's another printf() that says, "Booting all finished, dropped to user space\n". Since this message isn't printed, it appears that the kernel is freezing sometime between `start_boot_aps`, and that final printf. If we look at the line here (https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/smp_sys.c#L76%E...) it appears the kernel uses a loop with no timeout when waiting for AP cpus to wake up from their dormant state. It seems that the CPU the kernel is trying to boot isn't responding, or isn't entering the kernel.
I'd need more information about your configuration process, the repository you're using (seL4test? seL4Bench? Some custom infrastructure?), and maybe a link to a github repository where I can view the diff of your changes to the kernelso I can try your modified kernel myself.
Would you be able to provide me with any of these things?
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
________________________________ From: Devel devel-bounces@sel4.systems on behalf of Michal Podhradsky mpodhradsky@galois.com Sent: 09 August 2017 07:09 To: devel@sel4.systems Subject: Re: [seL4] VGA buffer as stdout
Hi Adrian, Kofi,
I followed your advice, and just as a proof of concept I redefined putConsoleChar from here: https://github.com/seL4/seL4/blob/master/src/plat/pc99/machine/io.c#L38 On top of printing on serial port, I added a line with text_ega_putchar((int) a); - so now the character is printed both on serial out and VGA screen.
I added the scrolling etc functions from https://github.com/seL4/util_libs/blob/master/libplatsupport/src/plat/pc99/e... to take care of line wraps and control characters (\n, \t, etc). Then I compiled the basic keyboard camkes example: https://github.com/seL4/camkes/tree/master/apps/keyboard and I run the program in qemu with -vga -std option.
I can see the kernel booting up on the screen as well as the serial out, but as soon as sel4 drops into userspace ("Starting node #0 with APIC ID 0") , it stops outputting anything (user program not running?);
The screenshot is here: https://drive.google.com/file/d/0B8h93vAE2c4ibmRKQkdZU3EtcUk/view?usp=sharin...
Any ideas what am I missing?
Regards M
On Wed, Aug 2, 2017 at 4:18 AM, Andrew Warkentin <andreww591@gmail.commailto:andreww591@gmail.com> wrote: On 8/2/17, Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au <Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au> wrote:
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.
Like I said before I am planning to exclusively use a linear framebuffer rather than hardware text mode (which is a relic from an era when hardware wasn't powerful enough to do software text modes with reasonable performance, and I believe it's not supported at all under UEFI), and I'm planning to have it just emulate a dumb terminal (i.e. no escape codes; I don't want to bloat the kernel with a VT100 emulator just for displaying early boot messages). I was thinking of using the framebuffer console code from coreboot's libpayload (which only emulates a dumb terminal and is very lightweight).
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.
I was going to have the kernel automatically disable the early console immediately before it loads the root server, so there would be no need for an API (at least not under UX/RT). UX/RT's root server will contain its own early console emulator (possibly also based on that of libpayload) that will provide a minimal subset of a Unix terminal device to programs run during early boot (initializing the console emulator will be the first thing that the root server does). A full-featured DRM/DRI graphics driver and console emulator will take over before the root volume is mounted.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Kofi,
I pushed the changes into vga_test branch: https://github.com/GaloisInc/seL4/tree/vga_test
Specifically see https://github.com/GaloisInc/seL4/blob/vga_test/src/plat/pc99/machine/io.c#L...
You can either add our fork of sel4 kernel as a remote and then compile any camkes app, or you can use our manifest
repo init -u https://github.com/GaloisInc/camkes-manifest -m devel-no-ssh.xml -b devel
repo sync
and then change the kernel to vga_test branch
Thanks for looking into it.
Regards Michal
On Tue, Aug 29, 2017 at 6:35 PM, Kofidoku.Atuah@data61.csiro.au wrote:
Hey Michal,
Sorry I'm so late in getting back to you:
So the message you see there is printed by the kernel in smp_sys.c ( https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/smp_sys.c#L66), and this function is called by (https://github.com/seL4/seL4/ blob/master/src/arch/x86/kernel/boot_sys.c#L610).
Just beneath that, there's another printf() that says, "Booting all finished, dropped to user space\n". Since this message isn't printed, it appears that the kernel is freezing sometime between `start_boot_aps`, and that final printf. If we look at the line here ( https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/smp_sys.c#L76%E...) it appears the kernel uses a loop with no timeout when waiting for AP cpus to wake up from their dormant state. It seems that the CPU the kernel is trying to boot isn't responding, or isn't entering the kernel.
I'd need more information about your configuration process, the repository you're using (seL4test? seL4Bench? Some custom infrastructure?), and maybe a link to a github repository where I can view the diff of your changes to the kernelso I can try your modified kernel myself.
Would you be able to provide me with any of these things?
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
*From:* Devel devel-bounces@sel4.systems on behalf of Michal Podhradsky mpodhradsky@galois.com *Sent:* 09 August 2017 07:09 *To:* devel@sel4.systems *Subject:* Re: [seL4] VGA buffer as stdout
Hi Adrian, Kofi,
I followed your advice, and just as a proof of concept I redefined putConsoleChar from here: https://github.com/seL4/seL4/ blob/master/src/plat/pc99/machine/io.c#L38 On top of printing on serial port, I added a line with text_ega_putchar((int) a); - so now the character is printed both on serial out and VGA screen.
I added the scrolling etc functions from https://github.com/seL4/util_ libs/blob/master/libplatsupport/src/plat/pc99/ega.c to take care of line wraps and control characters (\n, \t, etc). Then I compiled the basic keyboard camkes example: https://github.com/seL4/camkes/tree/master/apps/keyboard and I run the program in qemu with -vga -std option.
I can see the kernel booting up on the screen as well as the serial out, but as soon as sel4 drops into userspace ("Starting node #0 with APIC ID 0") , it stops outputting anything (user program not running?);
The screenshot is here: https://drive.google.com/file/d/ 0B8h93vAE2c4ibmRKQkdZU3EtcUk/view?usp=sharing
Any ideas what am I missing?
Regards M
On Wed, Aug 2, 2017 at 4:18 AM, Andrew Warkentin andreww591@gmail.com wrote:
On 8/2/17, Adrian.Danis@data61.csiro.au Adrian.Danis@data61.csiro.au wrote:
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.
Like I said before I am planning to exclusively use a linear framebuffer rather than hardware text mode (which is a relic from an era when hardware wasn't powerful enough to do software text modes with reasonable performance, and I believe it's not supported at all under UEFI), and I'm planning to have it just emulate a dumb terminal (i.e. no escape codes; I don't want to bloat the kernel with a VT100 emulator just for displaying early boot messages). I was thinking of using the framebuffer console code from coreboot's libpayload (which only emulates a dumb terminal and is very lightweight).
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.
I was going to have the kernel automatically disable the early console immediately before it loads the root server, so there would be no need for an API (at least not under UX/RT). UX/RT's root server will contain its own early console emulator (possibly also based on that of libpayload) that will provide a minimal subset of a Unix terminal device to programs run during early boot (initializing the console emulator will be the first thing that the root server does). A full-featured DRM/DRI graphics driver and console emulator will take over before the root volume is mounted.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Michal,
Based on this line here, https://github.com/GaloisInc/seL4/commit/caac4b936f2f2f0fb349bd5fdb4ea8d87f0... you use the VGA alphanumeric mode framebuffer's raw physical address for your mini driver. This is fine in the kernel boot process for as long as the kernel maintains its identity mapping of RAM.
Unfortunately, eventually during boot, since it's wasteful for the kernel to maintain the identity mapping, the kernel gets rid of it during `map_kernel_window()`, while it is establishing the kernel window mapping. From that point onward, the kernel has to access RAM as offsets into the kernel's window mapping.
The point at which the code on your branch fails is specifically here: https://github.com/GaloisInc/seL4/blob/master/src/arch/x86/kernel/boot_sys.c...
If you insert the following code:
printf("This line is executed successfully.\n"); for (;;);
Before line 202, it will work fine and you'll see your printf output and execution will halt as the infinite loop gets executed. If you put it after line 202, the kernel will crash. This is because `map_kernel_window()` gets called just before line 202, and the processor "sees" the changes that were made by line `map_kernel_window()` only after line 202.
To solve your issue, you can make your VGA driver work such that inside of map_kernel_window(), you dynamically change the address the driver writes to from 0xB8000 to an address in the kernel window. To get a kernel window address, you can use `ptrFromPAddr()`.
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
________________________________ From: Devel devel-bounces@sel4.systems on behalf of Michal Podhradsky mpodhradsky@galois.com Sent: 31 August 2017 04:26 To: devel@sel4.systems Subject: Re: [seL4] VGA buffer as stdout
Hi Kofi,
I pushed the changes into vga_test branch: https://github.com/GaloisInc/seL4/tree/vga_test
Specifically see https://github.com/GaloisInc/seL4/blob/vga_test/src/plat/pc99/machine/io.c#L...
You can either add our fork of sel4 kernel as a remote and then compile any camkes app, or you can use our manifest
repo init -u https://github.com/GaloisInc/camkes-manifest -m devel-no-ssh.xml -b devel
repo sync
and then change the kernel to vga_test branch
Thanks for looking into it.
Regards Michal
On Tue, Aug 29, 2017 at 6:35 PM, <Kofidoku.Atuah@data61.csiro.aumailto:Kofidoku.Atuah@data61.csiro.au> wrote:
Hey Michal,
Sorry I'm so late in getting back to you:
So the message you see there is printed by the kernel in smp_sys.c (https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/smp_sys.c#L66), and this function is called by (https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/boot_sys.c#L610...).
Just beneath that, there's another printf() that says, "Booting all finished, dropped to user space\n". Since this message isn't printed, it appears that the kernel is freezing sometime between `start_boot_aps`, and that final printf. If we look at the line here (https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/smp_sys.c#L76%E...) it appears the kernel uses a loop with no timeout when waiting for AP cpus to wake up from their dormant state. It seems that the CPU the kernel is trying to boot isn't responding, or isn't entering the kernel.
I'd need more information about your configuration process, the repository you're using (seL4test? seL4Bench? Some custom infrastructure?), and maybe a link to a github repository where I can view the diff of your changes to the kernelso I can try your modified kernel myself.
Would you be able to provide me with any of these things?
-- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
________________________________ From: Devel devel-bounces@sel4.systems on behalf of Michal Podhradsky <mpodhradsky@galois.commailto:mpodhradsky@galois.com> Sent: 09 August 2017 07:09 To: devel@sel4.systems Subject: Re: [seL4] VGA buffer as stdout
Hi Adrian, Kofi,
I followed your advice, and just as a proof of concept I redefined putConsoleChar from here: https://github.com/seL4/seL4/blob/master/src/plat/pc99/machine/io.c#L38 On top of printing on serial port, I added a line with text_ega_putchar((int) a); - so now the character is printed both on serial out and VGA screen.
I added the scrolling etc functions from https://github.com/seL4/util_libs/blob/master/libplatsupport/src/plat/pc99/e... to take care of line wraps and control characters (\n, \t, etc). Then I compiled the basic keyboard camkes example: https://github.com/seL4/camkes/tree/master/apps/keyboard and I run the program in qemu with -vga -std option.
I can see the kernel booting up on the screen as well as the serial out, but as soon as sel4 drops into userspace ("Starting node #0 with APIC ID 0") , it stops outputting anything (user program not running?);
The screenshot is here: https://drive.google.com/file/d/0B8h93vAE2c4ibmRKQkdZU3EtcUk/view?usp=sharin...
Any ideas what am I missing?
Regards M
On Wed, Aug 2, 2017 at 4:18 AM, Andrew Warkentin <andreww591@gmail.commailto:andreww591@gmail.com> wrote: On 8/2/17, Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au <Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au> wrote:
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.
Like I said before I am planning to exclusively use a linear framebuffer rather than hardware text mode (which is a relic from an era when hardware wasn't powerful enough to do software text modes with reasonable performance, and I believe it's not supported at all under UEFI), and I'm planning to have it just emulate a dumb terminal (i.e. no escape codes; I don't want to bloat the kernel with a VT100 emulator just for displaying early boot messages). I was thinking of using the framebuffer console code from coreboot's libpayload (which only emulates a dumb terminal and is very lightweight).
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.
I was going to have the kernel automatically disable the early console immediately before it loads the root server, so there would be no need for an API (at least not under UX/RT). UX/RT's root server will contain its own early console emulator (possibly also based on that of libpayload) that will provide a minimal subset of a Unix terminal device to programs run during early boot (initializing the console emulator will be the first thing that the root server does). A full-featured DRM/DRI graphics driver and console emulator will take over before the root volume is mounted.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Adrian.Danis＠data61.csiro.au -
Andrew Warkentin -
Kofidoku.Atuah＠data61.csiro.au -
Michal Podhradsky -
Raymond Jennings