Virtualization makes it easier to run simultaneous platform-specific operating systems (Linux, RTOS, VxWorks, RTEMS, other) in virtual machines that emulate, virtualize, or use virtualization hardware extensions to provide the necessary hardware they require. These VMs are supported by a hypervisor running on a single device.
Virtualization support for 64-bit x86 architecture available for the seL4 hypervisor increases the feasibility of porting legacy systems.
Now developers can run 64-bit builds of centOS or Ubuntu while gaining the security benefits of virtualization and seL4. This milestone also brings improved performance to virtualization on seL4-based systems, and enables a few new features:
The CAmkES-VM for x86 previously only supported 32-bit VMs. This does not take full advantage of the hardware resources. DornerWorks added support in the seL4 kernel and VMM libraries to boot 64-bit VMs, which has been tested with a basic buildroot and centOS.
While there is not a limit to the number of VMs the CAmkES-VM can support, each VM is only given a single core. This does not take full advantage of modern processors, which have numerous cores and built-in support for multicore. DornerWorks added support in the VMM to boot VMs with multiple cores.
When running the CAmkES-VM, the filesystem has previously been mounted on RAM. While pass-through of a SATA device is possible, many processors may not have access to more than 1 SATA device. This forces secondary VMs to run in volatile memory, losing any information on a reboot. By partitioning access to a SATA device, multiple VMs can share the hardware resource, allowing for the file system to mount on non-volatile storage and persist between boots. Storage partitions on a SATA drive are virtualized out to the VMs, and each VM is given access to those partition through configuration.