Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.
Hi Yevgeny, seL4 generally does not display anything on VGA devices, but rather is always sending to a serial port. In qemu you either had -nographic set or had setup some other kind of serial redirection. For example the 'simulate-ia32' target in sel4test does the following: qemu-system-i386 -m 512 -nographic -kernel images/kernel-ia32-pc99 -initrd images/${apps}-image-ia32-pc99 The -nographic means the VGA output is disabled and serial output is shown directly on the console. If you don't have access to the serial port on the machine you want to run on you can attempt to get some by doing the following in 'make menuconfig' * uncheck seL4 libraries -> libsel4platsupport -> Redirect putchar() to seL4_DebugPutchar() (this option won't exist if not building a debug seL4 kernel, in which case ignore this step) * set seL4 libraries -> libplatsupport -> X86 console device to '80x25 text mode EGA screen' Now doing 'make simulate-ia32' will still yield some output, but not as much. And if you enable the VGA screen by doing qemu-system-i386 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/sel4test-driver-image-ia32-pc99 -serial stdio You should see some output on the simulated VGA screen, and some on the serial. The split of output comes from the fact that only one part of sel4test has the ability to redirect its output, and the kernel has no ability to use anything other than the serial device. If you do see both kinds of output in qemu then try the image again on hardware and hopefully you see something :) Adrian On Tue 14-Jun-2016 3:52 PM, Yevgeny Lavrov wrote: Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
"Yevgeny" == Yevgeny Lavrov
writes:
Yevgeny> I end up with no output at all and no error msgs that can Yevgeny> give me a clue on where something went wrong. The output is sent to the serial port, COM1. Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://www.data61.csiro.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA/Data61
participants (3)
-
Adrian Danis
-
Peter Chubb
-
Yevgeny Lavrov