Re: [seL4] using camkesvm with qemu

10 Mar 2016

      No docs I'm afraid :)

The thing with these examples is that the whole point of them is to 
describe a system that is set up with the particular hardware of the 
given platform.

We could come up with an example description for a vmware (as it 
supports both vt-x and vt-d) target, but this would likely be very 
unstable as there is no guarantee that two slightly different versions 
of an emulator won't put hardware resources at slightly different 
locations, rendering the configuration invalid.

In an ideal world we would have a tool that you run from Linux on your 
target machine (be it virtual or otherwise) and this scrapes the 
relevant hardware information and generates an appropriate default 
configuration. This is, unfortunately, something we simply have not had 
the resources to look into yet.

Adrian

On Thu 10-Mar-2016 12:31 PM, Julien Delange wrote:
...
Thanks all - it explains a lot now! Is there any paper or doc that 
explains how to test the VM example with an emulator or does these 
examples run only on the real hardware?
On Wed, Mar 9, 2016 at 5:09 PM, Adrian Danis 
mailto:adrian.danis@nicta.com.au> wrote:
The x86 VMM requires both vt-x and vt-d support. vt-x support is
    easy enough with qemu+kvm, but I'm not sure what the vt-d support
    is like. I know vmware supports emulating both vt-x and vt-d.
That is the easy part though. Due to the the way CAmkES and capDL
    presently work all hardware resources (interrupts, memory mapped
    IO regions, PCI IOSpaces, etc) must all be described statically
    offline. For this reason I would not recommend starting with the
    c162 configuration, as it has many devices described all from a
    particular hardware board.
I would suggest starting with the optiplex9020_onevm
    configuration, as the only additional resources specified are for
    additional memory. See the 'vm0_config.ram = ...' line in
    apps/optiplex9020_onevm/optiplex9020.camkes. This describes a list
    of physical memory regions of the form (paddr, n) where the size
    of the region = 2^n bytes.
Adrian
On Thu 10-Mar-2016 7:26 AM, Corey Richardson wrote:
...
On Wed, Mar 09, 2016 at 03:10:58PM -0500, Julien Delange wrote:
...
Any idea about how to run this example with qemu and/or how to test it?
Assuming you're on Linux, to run hypervisors in qemu you'll need to enable
    nested vmx. There's some basic instructions here:
http://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/tree/Document...
Additionally, you can nest deeper than the two levels described in that
    document, but it will get *extremely* slow, so I would not recommend trying
    it.
(There may be other nuances in testing that particular project, but I am not
    personally aware of them.)
_______________________________________________
    Devel mailing list
    Devel@sel4.systems mailto: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.
_______________________________________________
    Devel mailing list
    Devel@sel4.systems
    https://sel4.systems/lists/listinfo/devel