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> 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.