Hi Michal, Based on this line here, https://github.com/GaloisInc/seL4/commit/caac4b936f2f2f0fb349bd5fdb4ea8d87f000758#diff-46870bfbe328bb80298d94be2e817e4eR122 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#L202 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 <[email protected]> on behalf of Michal Podhradsky <[email protected]> Sent: 31 August 2017 04:26 To: [email protected] 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#L101 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, <[email protected]<mailto:[email protected]>> 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) 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 <[email protected]> on behalf of Michal Podhradsky <[email protected]<mailto:[email protected]>> Sent: 09 August 2017 07:09 To: [email protected] 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 <[email protected]<mailto:[email protected]>> wrote: On 8/2/17, [email protected]<mailto:[email protected]> <[email protected]<mailto:[email protected]>> 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 [email protected] https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
