Running seL4 on bare-metal x86_64 PC
Hi, I am very new to sel4 and I am trying to run it bare-metal on an Intel Xeon x86_64 machine. I am following the instructions here PC99 | seL4 docs. I can run seL4 using the ./simulate script which runs the kernel under QEMU. However, I would like the run seL4 natively on my machine. After the build, I have the following images in the images/ directory. kernel-x86_64-pc99 sel4test-driver-image-x86_64-pc99 I have created a Grub2 menu entry by copying these images under /boot. However, when I boot using the created menu entry I get a black screen and I also see no output on the serial port. My Grub2 menu entry is as follows menuentry “Load seL4 VM” --class os { load_video insmod gzio insmod part_msdos insmod ext2 set root=‘(hd0,msdos2)’ multiboot /boot/kernel-x86_64-pc99 module /boot/sel4test-driver-image-x86_64-pc99 } I have also tried the multiboot2 protocol as I have an UEFI-supported system but it also doesn’t work. After booting into the seL4 VM I get a black screen and there is no output on the serial port. Any Idea what I am doing wrong?
Hello! Not sure if you're still working on this but I'm also running seL4 bare metal on x86-64. My first recommendation which helped me a lot is to try to get it to run on qemu using your disk image rather than using the ./simulate script (I'm assuming you're currently flashing the image to a usb and booting it off a physical machine) because it qemu provides additional debug info especially if a triple fault is happening. You can use OVMF from tianocore to enable qemu to boot uefi images. Here's my grub entry as well: menuentry "Load seL4 VM" --class os { insmod gzio insmod video insmod video_bochs insmod video_cirrus insmod efi_gop insmod efi_uga set root='(hd0,gpt1)' multiboot2 /Fennec/kernel module2 /Fennec/root_task } My other suggestions are to set the cmake variable KernelHugePage to OFF (call cmake with -DKernelHugePage=OFF) as I found it got in the way of booting, for whatever reason. Also, see if padding your root task image out to 1MB helps. Seriously, just add 0s to the end of the file out to a MB or two. Different sections of the kernel are loaded at different addresses, and for me, grub was trying to squeeze the root task image in between two of these sections rather than at the very end, which was causing an assert to fail. Padding the image forces grub to place it after all kernel sections. That assertion fail should show up in the serial log though. Finally, here's the github to my project I'm working on which should boot fine if you follow the steps in the README. The code is a bit of a mess because it was a learning experience for me too. The grub file is under bootloader/grub.cfg and the root task is under sel4/projects/root_task. Output image can be burned to a usb or simulated in qemu (the OVMF files are provided). It should have both serial and graphical output if booted correctly. https://github.com/FennelFoxxo/Fennec/
participants (2)
-
fennelfoxxo＠gmail.com -
saftab.rashid＠gmail.com