Re: [seL4] Running 2 VM Linux on Camkes

9 Jan 2019

      Hello Amit,

I have successfully gotten two VMs running, so it is possible.

Your configuration looks good, but you have a lot of untyped resources, and the heap, and the guest RAM to allocate. You've only given your QEMU model 2GB of RAM to use. Could you try giving QEMU 4GB? The error you're getting is from the capdl loader, so it seems like you've run out of memory to retype.

Let me know if you have any other questions, I'd be glad to help.

Chris Guikema

-----Original Message-----
From: Devel <devel-bounces@sel4.systems> On Behalf Of Amit Goyal
Sent: Tuesday, January 8, 2019 5:42 AM
To: devel@sel4.systems
Subject: [seL4] Running 2 VM Linux on Camkes

CAUTION: This email originated from outside the organization. Do not click links or open attachments unless you recognize the sender and know the content is safe.

Hi,

I am using Ubuntu 16.04 on 64 Bit, i7 machine and following CAmkES x86 VM instructions available at:
https://docs.sel4.systems/CAmkESVM

I am able to successfully run single guest vm. I am now trying to run 2 guest vms at the same time. For this, I changed

a) minimal.camkes as follows:
--------------------------------------------------------------------------------------------------------------------------------
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif
import <VM/vm.camkes>;

#include <configurations/vm.h>

#define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \ i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem"

component Init0 {
     VM_INIT_DEF()
}

component Init1 {
     VM_INIT_DEF()
}

assembly {
     composition {
         VM_COMPOSITION_DEF()
         VM_PER_VM_COMP_DEF(0)
         VM_PER_VM_COMP_DEF(1)
     }

     configuration {
         VM_CONFIGURATION_DEF()
         VM_PER_VM_CONFIG_DEF(0)
         VM_PER_VM_CONFIG_DEF(1)

         vm0.simple_untyped23_pool = 20;
         vm0.heap_size = 0x2000000;
         vm0.guest_ram_mb = 128;
         vm0.kernel_cmdline = VM_GUEST_CMDLINE;
         vm0.kernel_image = "bzimage";
         vm0.kernel_relocs = "bzimage";
         vm0.initrd_image = "rootfs.cpio";
         vm0.iospace_domain = 0x0f;

         vm1.simple_untyped23_pool = 20;
         vm1.heap_size = 0x2000000;
         vm1.guest_ram_mb = 128;
         vm1.kernel_cmdline = VM_GUEST_CMDLINE;
         vm1.kernel_image = "bzimage";
         vm1.kernel_relocs = "bzimage";
         vm1.initrd_image = "rootfs.cpio";
         vm1.iospace_domain = 0x0f;
     }
}
---------------------------------------------------------------------------------------------------------------------------------

b) CMakeLists.txt as follows:
---------------------------------------------------------------------------------------------------------------------------------
cmake_minimum_required(VERSION 3.8.2)

project(minimal)

# Include CAmkES VM helper functions
include("../../vm/camkes_vm_helpers.cmake")
include("../../vm-linux/vm-linux-helpers.cmake")

# Declare VM component: Init0
DeclareCAmkESVM(Init0)
DeclareCAmkESVM(Init1)

# Get Default Linux VM files
GetDefaultLinuxKernelFile(kernel_file)
GetDefaultLinuxRootfsFile(rootfs_file)

# Decompress Linux Kernel image and add to file server DecompressLinuxKernel(extract_linux_kernel decompressed_kernel
${kernel_file})
AddToFileServer("bzimage" ${decompressed_kernel} DEPENDS
extract_linux_kernel)

# Add rootfs images into file server
AddToFileServer("rootfs.cpio" ${rootfs_file})

# Initialise CAmkES Root Server with addition CPP includes
DeclareCAmkESVMRootServer(minimal.camkes)
---------------------------------------------------------------------------------------------------------------------------------

I can successfully build the system and 2 vm images are being created
namely:
vm0_group.bin, vm1_group.bin

On running the system using:
sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=true --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -net
nic,model=e1000 -net tap,script=no,ifname=tap0"

I get the following error:
---------------------------------------------------------------------------------------------------------------------------------
<<seL4(CPU 0) [decodeUntypedInvocation/209 T0xffbfec00 "rootserver"
@804853d]: Untyped Retype: Insufficient memory (1 * 4194304 bytes needed, 2048 bytes available).>> <<seL4(CPU 0) [decodeInvocation/542 T0xffbfec00 "rootserver" @804853d]:
Attempted to invoke a null cap #0.>>
create_objects@main.c:767 [Err seL4_InvalidCapability]:
        Untyped retype failed with unexpected error
seL4 root server abort()ed
Debug halt syscall from user thread 0xffbfec00 "rootserver"
halting...
Kernel entry via Unknown syscall, word: 523QEMU: Terminated
---------------------------------------------------------------------------------------------------------------------------------

I have 2 doubts:
a) Can someone suggest a possible way to get this running.
b) Is it possible to see the 2 VMs running on separate terminals at the same time.

--
Thanks and Regards,
Amit Goyal

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel