Hello,
I am at the George Washington University working on benchmarking the seL4 system. I am new to systems, and I am having a hard time building a bootable USB image On Ubuntu 14.04 x86. I understand that there is a Grub2 stanza on the Downloads page https://sel4.systems/Download/ on the SeL4 website, but I cannot find the sel4kernel and sel4rootserver files in the system to build into a boot image.
I would like to build an image using a process similar to the one in Pistachio (see https://www.l4ka.org/120.php) except for using Grub2 of course.
Are there instructions for booting on full hardware such as a PC?
Regards,
Matthew Scaperoth
Jr. Programmer Analyst
The George Washington University
Academic Technologies
Tel: 202-994-6907
"Matthew" == Matthew Scaperoth mscapero@gwu.edu writes:
Matthew> I am at the George Washington University working on Matthew> benchmarking the seL4 system. I am new to systems, and I am Matthew> having a hard time building a bootable USB image On Ubuntu Matthew> 14.04 x86. I understand that there is a Grub2 stanza on the Matthew> Downloads page https://sel4.systems/Download/ on the SeL4 Matthew> website, but I cannot find the sel4kernel and sel4rootserver Matthew> files in the system to build into a boot image.
If you have built a seL4-based systemaccording to the instructions, the kernel and root server are in .../images/ They have different names according to what you've built.
For example, sel4test names the root server sel4test-driver-image-ia32-pc99 and the kernel kernel-ia32-pc99
I generally use syslinux to create a bootable USB stick, as the grub on my system wants to use EFI.
Like this, assuming your flash drive is at /dev/sdb with a FAT partition at /dev/sdb1:
install-mbr /dev/sdb syslinux --install /dev/sdb1 mount /dev/sdb1 /mnt cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver cp images/kernel-ia32-pc99 /mnt/sel4kernel cat > /mnt/syslinux.cfg <<EOF SERIAL 0 115200 DEFAULT seL4test LABEL seL4test kernel mboot.c32 append sel4kernel --- rootserver EOF cp /usr/lib/syslinux/modules/bios/mboot.c32 /mnt cp /usr/lib/syslinux/modules/bios/libcom32.c32 /mnt umount /mnt
use fdisk to make sure the first partition is bootable.
And you're done. Output will come on the serial port
Hope this helps.
Hi,
Above steps given by Peter Chubb worked fine. I was able to get the output through serial port.
But it executes the test suite and then stops. How can I get a shell prompt so that I can test the kernel for virtualization?
My question may be completely wrong here but I'm new to this field. How can one use seL4 kernel to install virtual OS on top of it on x86 architecture?
On Fri, Sep 5, 2014 at 5:10 AM, Peter Chubb peter.chubb@nicta.com.au wrote:
"Matthew" == Matthew Scaperoth mscapero@gwu.edu writes:
Matthew> I am at the George Washington University working on Matthew> benchmarking the seL4 system. I am new to systems, and I am Matthew> having a hard time building a bootable USB image On Ubuntu Matthew> 14.04 x86. I understand that there is a Grub2 stanza on the Matthew> Downloads page https://sel4.systems/Download/ on the SeL4 Matthew> website, but I cannot find the sel4kernel and sel4rootserver Matthew> files in the system to build into a boot image.
If you have built a seL4-based systemaccording to the instructions, the kernel and root server are in .../images/ They have different names according to what you've built.
For example, sel4test names the root server sel4test-driver-image-ia32-pc99 and the kernel kernel-ia32-pc99
I generally use syslinux to create a bootable USB stick, as the grub on my system wants to use EFI.
Like this, assuming your flash drive is at /dev/sdb with a FAT partition at /dev/sdb1:
install-mbr /dev/sdb syslinux --install /dev/sdb1 mount /dev/sdb1 /mnt cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver cp images/kernel-ia32-pc99 /mnt/sel4kernel cat > /mnt/syslinux.cfg <<EOF SERIAL 0 115200 DEFAULT seL4test LABEL seL4test kernel mboot.c32 append sel4kernel --- rootserver EOF cp /usr/lib/syslinux/modules/bios/mboot.c32 /mnt cp /usr/lib/syslinux/modules/bios/libcom32.c32 /mnt umount /mnt
use fdisk to make sure the first partition is bootable.
And you're done. Output will come on the serial port
Hope this helps.
Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi,
I am at Tongji University (China, http://www.tongji.edu.cn/english/ ), I want to build a Fault Tolerant Operating System for high speed railway.
The seL4 is just a micro-kernel operating system, there is still no centre-service to let it work as a PC operating system, and it still can’t work as a virtual-machine, such as VirtualBox. There are a lot of works should be done before seL4 used as a really operating system.
Xilong Pei
2014/9/18
发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 Aniruddha Bhide 发送时间: 2014年9月18日 14:27 收件人: Peter Chubb 抄送: devel@sel4.systems 主题: Re: [seL4] x86 Bootable USB install
Hi,
Above steps given by Peter Chubb worked fine. I was able to get the output through serial port.
But it executes the test suite and then stops. How can I get a shell prompt so that I can test the kernel for virtualization?
My question may be completely wrong here but I'm new to this field. How can one use seL4 kernel to install virtual OS on top of it on x86 architecture?
On Fri, Sep 5, 2014 at 5:10 AM, Peter Chubb peter.chubb@nicta.com.au wrote:
"Matthew" == Matthew Scaperoth mscapero@gwu.edu writes:
Matthew> I am at the George Washington University working on Matthew> benchmarking the seL4 system. I am new to systems, and I am Matthew> having a hard time building a bootable USB image On Ubuntu Matthew> 14.04 x86. I understand that there is a Grub2 stanza on the Matthew> Downloads page https://sel4.systems/Download/ on the SeL4 Matthew> website, but I cannot find the sel4kernel and sel4rootserver Matthew> files in the system to build into a boot image.
If you have built a seL4-based systemaccording to the instructions, the kernel and root server are in .../images/ They have different names according to what you've built.
For example, sel4test names the root server sel4test-driver-image-ia32-pc99 and the kernel kernel-ia32-pc99
I generally use syslinux to create a bootable USB stick, as the grub on my system wants to use EFI.
Like this, assuming your flash drive is at /dev/sdb with a FAT partition at /dev/sdb1:
install-mbr /dev/sdb syslinux --install /dev/sdb1 mount /dev/sdb1 /mnt cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver cp images/kernel-ia32-pc99 /mnt/sel4kernel cat > /mnt/syslinux.cfg <<EOF SERIAL 0 115200 DEFAULT seL4test LABEL seL4test kernel mboot.c32 append sel4kernel --- rootserver EOF cp /usr/lib/syslinux/modules/bios/mboot.c32 /mnt cp /usr/lib/syslinux/modules/bios/libcom32.c32 /mnt umount /mnt
use fdisk to make sure the first partition is bootable.
And you're done. Output will come on the serial port
Hope this helps. -- Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi,
I am at Tongji University (China, http://www.tongji.edu.cn/english/ ), I want to build a Fault Tolerant Operating System for high speed railway.
The seL4 is just a micro-kernel operating system, there is still no centre-service to let it work as a PC operating system, and it still can’t work as a virtual-machine, such as VirtualBox. There are a lot of works should be done before seL4 used as a really operating system.
Xilong Pei
2014/9/18
发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 Aniruddha Bhide 发送时间: 2014年9月18日 14:27 收件人: Peter Chubb 抄送: devel@sel4.systems 主题: Re: [seL4] x86 Bootable USB install
Hi,
Above steps given by Peter Chubb worked fine. I was able to get the output through serial port.
But it executes the test suite and then stops. How can I get a shell prompt so that I can test the kernel for virtualization?
My question may be completely wrong here but I'm new to this field. How can one use seL4 kernel to install virtual OS on top of it on x86 architecture?
On Fri, Sep 5, 2014 at 5:10 AM, Peter Chubb peter.chubb@nicta.com.au wrote:
"Matthew" == Matthew Scaperoth mscapero@gwu.edu writes:
Matthew> I am at the George Washington University working on Matthew> benchmarking the seL4 system. I am new to systems, and I am Matthew> having a hard time building a bootable USB image On Ubuntu Matthew> 14.04 x86. I understand that there is a Grub2 stanza on the Matthew> Downloads page https://sel4.systems/Download/ on the SeL4 Matthew> website, but I cannot find the sel4kernel and sel4rootserver Matthew> files in the system to build into a boot image.
If you have built a seL4-based systemaccording to the instructions, the kernel and root server are in .../images/ They have different names according to what you've built.
For example, sel4test names the root server sel4test-driver-image-ia32-pc99 and the kernel kernel-ia32-pc99
I generally use syslinux to create a bootable USB stick, as the grub on my system wants to use EFI.
Like this, assuming your flash drive is at /dev/sdb with a FAT partition at /dev/sdb1:
install-mbr /dev/sdb syslinux --install /dev/sdb1 mount /dev/sdb1 /mnt cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver cp images/kernel-ia32-pc99 /mnt/sel4kernel cat > /mnt/syslinux.cfg <<EOF SERIAL 0 115200 DEFAULT seL4test LABEL seL4test kernel mboot.c32 append sel4kernel --- rootserver EOF cp /usr/lib/syslinux/modules/bios/mboot.c32 /mnt cp /usr/lib/syslinux/modules/bios/libcom32.c32 /mnt umount /mnt
use fdisk to make sure the first partition is bootable.
And you're done. Output will come on the serial port
Hope this helps. -- Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Dr. Chubb,
Thanks so much for your reply. This did the trick! I have another question that I will ask on another thread.
Thanks again,
Matthew Scaperoth
Jr. Programmer Analyst
The George Washington University
Academic Technologies
Tel: 202-994-6907
On Thu, Sep 4, 2014 at 7:40 PM, Peter Chubb peter.chubb@nicta.com.au wrote:
"Matthew" == Matthew Scaperoth mscapero@gwu.edu writes:
Matthew> I am at the George Washington University working on Matthew> benchmarking the seL4 system. I am new to systems, and I am Matthew> having a hard time building a bootable USB image On Ubuntu Matthew> 14.04 x86. I understand that there is a Grub2 stanza on the Matthew> Downloads page https://sel4.systems/Download/ on the SeL4 Matthew> website, but I cannot find the sel4kernel and sel4rootserver Matthew> files in the system to build into a boot image.
If you have built a seL4-based systemaccording to the instructions, the kernel and root server are in .../images/ They have different names according to what you've built.
For example, sel4test names the root server sel4test-driver-image-ia32-pc99 and the kernel kernel-ia32-pc99
I generally use syslinux to create a bootable USB stick, as the grub on my system wants to use EFI.
Like this, assuming your flash drive is at /dev/sdb with a FAT partition at /dev/sdb1:
install-mbr /dev/sdb syslinux --install /dev/sdb1 mount /dev/sdb1 /mnt cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver cp images/kernel-ia32-pc99 /mnt/sel4kernel cat > /mnt/syslinux.cfg <<EOF SERIAL 0 115200 DEFAULT seL4test LABEL seL4test kernel mboot.c32 append sel4kernel --- rootserver EOF cp /usr/lib/syslinux/modules/bios/mboot.c32 /mnt cp /usr/lib/syslinux/modules/bios/libcom32.c32 /mnt umount /mnt
use fdisk to make sure the first partition is bootable.
And you're done. Output will come on the serial port
Hope this helps.
Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA
Hi Peter,
Your method is great. But I meet some problems. The bootable usb works very well on laptop. But when I move to a large machine which has two sockets, and each socket has six cores(my laptop only has 2 cores), syslinux can only print out something like "loading kernel is ok", and after some seconds, the machine reboot. It just keeps rebooting again and again. I do not know why it is. Is it possible for syslinyx to reboot the machine if I have some incorrect configuration of it? Is it possible for the sel4 kernel to reboot the machine if it detects some error or I do not config sel4 correctly? Does it need some special configuration for sel4 with a machine which has mult-sockets multi-cores? If so, how to do it? Could anyone give me some hints?
Thank you very much. Yuixn
On Thu, Sep 4, 2014 at 3:40 PM, Peter Chubb peter.chubb@nicta.com.au wrote:
"Matthew" == Matthew Scaperoth mscapero@gwu.edu writes:
Matthew> I am at the George Washington University working on Matthew> benchmarking the seL4 system. I am new to systems, and I am Matthew> having a hard time building a bootable USB image On Ubuntu Matthew> 14.04 x86. I understand that there is a Grub2 stanza on the Matthew> Downloads page https://sel4.systems/Download/ on the SeL4 Matthew> website, but I cannot find the sel4kernel and sel4rootserver Matthew> files in the system to build into a boot image.
If you have built a seL4-based systemaccording to the instructions, the kernel and root server are in .../images/ They have different names according to what you've built.
For example, sel4test names the root server sel4test-driver-image-ia32-pc99 and the kernel kernel-ia32-pc99
I generally use syslinux to create a bootable USB stick, as the grub on my system wants to use EFI.
Like this, assuming your flash drive is at /dev/sdb with a FAT partition at /dev/sdb1:
install-mbr /dev/sdb syslinux --install /dev/sdb1 mount /dev/sdb1 /mnt cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver cp images/kernel-ia32-pc99 /mnt/sel4kernel cat > /mnt/syslinux.cfg <<EOF SERIAL 0 115200 DEFAULT seL4test LABEL seL4test kernel mboot.c32 append sel4kernel --- rootserver EOF cp /usr/lib/syslinux/modules/bios/mboot.c32 /mnt cp /usr/lib/syslinux/modules/bios/libcom32.c32 /mnt umount /mnt
use fdisk to make sure the first partition is bootable.
And you're done. Output will come on the serial port
Hope this helps.
Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
"Yuxin" == Yuxin Ren ryx@gwmail.gwu.edu writes:
Yuxin> Your method is great. But I meet some problems. The bootable Yuxin> usb works very well on laptop. But when I move to a large Yuxin> machine which has two sockets, and each socket has six cores(my Yuxin> laptop only has 2 cores), syslinux can only print out something Yuxin> like "loading kernel is ok", and after some seconds, the Yuxin> machine reboot. It just keeps rebooting again and again. I do Yuxin> not know why it is. Is it possible for syslinyx to reboot the Yuxin> machine if I have some incorrect configuration of it? Is it Yuxin> possible for the sel4 kernel to reboot the machine if it Yuxin> detects some error or I do not config sel4 correctly? Does it Yuxin> need some special configuration for sel4 with a machine which Yuxin> has mult-sockets multi-cores? If so, how to do it? Could Yuxin> anyone give me some hints?
You can get debug output from the kernel by: 1. using one of the `debug' configurations, and 2. Specifying which console ports to use for debugging on the multiboot command line. You need to specify one per node.
Something like: console_port=0x3f8,0x3f8
On a machine of that class, you may be able to look in the BMC logs to find the reboot cause.
-
Aniruddha Bhide -
Matthew Scaperoth -
Peter Chubb -
XilongPei(裴喜龙) -
Yuxin Ren