Does seL4 provide an initrd with a shell?
I have been following the instructions "Fetching, Configuring and Building seL4test" on this page https://docs.sel4.systems/GettingStarted.html. Everything seems to work, but the initrd provided only runs a bunch of tests and then exits. Is there another project that provides a shell or a way for me to launch my own programs? I have tried to follow the instructions on these pages https://docs.sel4.systems/Hardware/Qemu/ and https://docs.sel4.systems/CAmkESVM but the repo init command fails (404). Thanks, Baptiste.
Hi Baptiste, When you run the repo init command, is the 404 command similar to the following? Get https://github.com/seL4/camkes-vm-manifest.git % Total % Received % Xferd Average Speed Time Time Time Current Dload Upload Total Spent Left Speed 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 curl: (22) The requested URL returned error: 404 Not Found Server does not provide clone.bundle; ignoring. If so, this shouldn't be an issue. The 404 error is informing that the server does not clone.bundles. You should be able to proceed with a "repo sync". If not the error, would you be able to share 404 message? Kind Regards, Adam ________________________________ From: Devel <devel-bounces@sel4.systems> on behalf of Baptiste Lepers <baptiste.lepers@gmail.com> Sent: Thursday, 27 September 2018 2:28 PM To: devel@sel4.systems Subject: [seL4] Does seL4 provide an initrd with a shell? I have been following the instructions "Fetching, Configuring and Building seL4test" on this page https://docs.sel4.systems/GettingStarted.html. Everything seems to work, but the initrd provided only runs a bunch of tests and then exits. Is there another project that provides a shell or a way for me to launch my own programs? I have tried to follow the instructions on these pages https://docs.sel4.systems/Hardware/Qemu/ and https://docs.sel4.systems/CAmkESVM but the repo init command fails (404). Thanks, Baptiste.
Hi Baptiste, Aside from running a Linux guest, we do not currently have a native shell. The x86 VM should work though. Cheers Anna. ________________________________ From: Devel <devel-bounces@sel4.systems> on behalf of Baptiste Lepers <baptiste.lepers@gmail.com> Sent: Thursday, 27 September 2018 2:28 PM To: devel@sel4.systems Subject: [seL4] Does seL4 provide an initrd with a shell? I have been following the instructions "Fetching, Configuring and Building seL4test" on this page https://docs.sel4.systems/GettingStarted.html. Everything seems to work, but the initrd provided only runs a bunch of tests and then exits. Is there another project that provides a shell or a way for me to launch my own programs? I have tried to follow the instructions on these pages https://docs.sel4.systems/Hardware/Qemu/ and https://docs.sel4.systems/CAmkESVM but the repo init command fails (404). Thanks, Baptiste.
Thanks for the quick answers! Indeed, the error messages were not an issue. I was able to build some VMs and initrd, but I'm not sure how to launch them... E.g., when I build the optiplex9020 VM: $ ../init-build.sh -DCAMKES_VM_APP=optiplex9020 -DPLATFORM=x86_64 -DSIMULATION=TRUE -DSIMULATE=1 $ ninja $ qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,+xsave,-xsaveopt,-xsavec,+fsgsbase,-invpcid,enforce -nographic -serial mon:stdio -m size=512M -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 I get the following error: "Requested feature mask is 0x3, but only 0x0 supported seL4 called fail at /home/blepers/git.clone/sel4vm/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :(" Any idea why? (The SIMULATION and SIMULATE flags do not seem to have an effect, I just added them because in some projects that seem to create a "simulate" file with the right qemu parameters. I'm not sure what's the right way to create an image that runs in qemu here.) Thanks, Baptiste. On Wed, Oct 3, 2018 at 9:55 AM <Anna.Lyons@data61.csiro.au> wrote:
Hi Baptiste,
Aside from running a Linux guest, we do not currently have a native shell. The x86 VM should work though.
Cheers
Anna.
------------------------------ *From:* Devel <devel-bounces@sel4.systems> on behalf of Baptiste Lepers < baptiste.lepers@gmail.com> *Sent:* Thursday, 27 September 2018 2:28 PM *To:* devel@sel4.systems *Subject:* [seL4] Does seL4 provide an initrd with a shell?
I have been following the instructions "Fetching, Configuring and Building seL4test" on this page https://docs.sel4.systems/GettingStarted.html. Everything seems to work, but the initrd provided only runs a bunch of tests and then exits. Is there another project that provides a shell or a way for me to launch my own programs?
I have tried to follow the instructions on these pages https://docs.sel4.systems/Hardware/Qemu/ and https://docs.sel4.systems/CAmkESVM but the repo init command fails (404).
Thanks, Baptiste.
Hi Baptiste, You are correct, the SIMULATION flags currently don't have effect in the CAmkES VM project (will look into fixing). In order to simulate the CAmkES VM I would recommend using KVM. This is due to the VM project relying on hardware virtualization features (e.g VT-x). The following command should boot the optiplex example in QEMU: sudo qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Haswell,+vme,+pdpe1gb,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 In addition, you may need to make sure your KVM driver has nested virtualization enabled (https://wiki.archlinux.org/index.php/KVM#Nested_virtualization). Regards, Adam ________________________________ From: Devel <devel-bounces@sel4.systems> on behalf of Baptiste Lepers <baptiste.lepers@gmail.com> Sent: Wednesday, 3 October 2018 10:17 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] Does seL4 provide an initrd with a shell? Thanks for the quick answers! Indeed, the error messages were not an issue. I was able to build some VMs and initrd, but I'm not sure how to launch them... E.g., when I build the optiplex9020 VM: $ ../init-build.sh -DCAMKES_VM_APP=optiplex9020 -DPLATFORM=x86_64 -DSIMULATION=TRUE -DSIMULATE=1 $ ninja $ qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,+xsave,-xsaveopt,-xsavec,+fsgsbase,-invpcid,enforce -nographic -serial mon:stdio -m size=512M -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 I get the following error: "Requested feature mask is 0x3, but only 0x0 supported seL4 called fail at /home/blepers/git.clone/sel4vm/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :(" Any idea why? (The SIMULATION and SIMULATE flags do not seem to have an effect, I just added them because in some projects that seem to create a "simulate" file with the right qemu parameters. I'm not sure what's the right way to create an image that runs in qemu here.) Thanks, Baptiste. On Wed, Oct 3, 2018 at 9:55 AM <Anna.Lyons@data61.csiro.au<mailto:Anna.Lyons@data61.csiro.au>> wrote: Hi Baptiste, Aside from running a Linux guest, we do not currently have a native shell. The x86 VM should work though. Cheers Anna. ________________________________ From: Devel <devel-bounces@sel4.systems> on behalf of Baptiste Lepers <baptiste.lepers@gmail.com<mailto:baptiste.lepers@gmail.com>> Sent: Thursday, 27 September 2018 2:28 PM To: devel@sel4.systems Subject: [seL4] Does seL4 provide an initrd with a shell? I have been following the instructions "Fetching, Configuring and Building seL4test" on this page https://docs.sel4.systems/GettingStarted.html. Everything seems to work, but the initrd provided only runs a bunch of tests and then exits. Is there another project that provides a shell or a way for me to launch my own programs? I have tried to follow the instructions on these pages https://docs.sel4.systems/Hardware/Qemu/ and https://docs.sel4.systems/CAmkESVM but the repo init command fails (404). Thanks, Baptiste.
participants (3)
-
Adam.Felizzi＠data61.csiro.au -
Anna.Lyons＠data61.csiro.au -
Baptiste Lepers