Hi,
I just want to share some information which I needed to run camkes-vm
with qemu, especially addressing one issue which prevented the guest vm
to boot. I basically follow the recommendations of Adrian in [1] and
only focus on the simple case without vt-d.
1. use the 'optiplex9020_onevm' configuration as it basically just
specifies physical RAM.
2. enable nested KVM [2,3]
3. run QEMU with enough RAM:
qemu-system-i386 -nographic \
-m 3GB \
-enable-kvm \
-cpu host \
-kernel images/kernel-ia32-pc99 -initrd
images/capdl-loader-experimental-image-ia32-pc99
Following the above steps gives you a booting camkes vmm, however it
fails to eventually activate Intel vt-x, needed to run the guest vm. The
reason for that is that the seL4 kernel requires the
IA32_FEATURE_CONTROL MSR to have VMXON enabled (bit 2) and locked (bit
0) (i.e. a value of 5). Normally, it's the job of the BIOS to do so,
however I couldn't find an appropriate QEMU BIOS ROM which does so. The
quick workaround is to enable VMXON within the seL4 kernel itself. The
corresponding diff is attached. With this minor change, the recompiled
kernel works like a charm.
PS:
One could consider making a separate option in Kconfig for that purpose.
Best,
Sammey
[1] https://sel4.systems/pipermail/devel/2016-March/000717.html
[2] http://www.rdoxenham.com/?p=275
[3] https://wiki.archlinux.org/index.php/QEMU#Enabling_KVM
diff --git a/src/arch/x86/object/vtx.c b/src/arch/x86/object/vtx.c
index 10b02a4..805070d 100644
--- a/src/arch/x86/object/vtx.c
+++ b/src/arch/x86/object/vtx.c
@@ -66,6 +66,10 @@ BOOT_CODE void vtx_enable(void)
if (is_vtx_supported()) {
uint64_t feature_control = ((uint64_t)x86_rdmsr_high(MSR_FEATURE_CONTROL)) << 32 | (uint64_t)x86_rdmsr_low(MSR_FEATURE_CONTROL);
uint64_t vm_basic = ((uint64_t)x86_rdmsr_high(MSR_VM_BASIC)) << 32 | (uint64_t)x86_rdmsr_low(MSR_VM_BASIC);
+
+ feature_control |= FEATURE_CONTROL_MASK;
+ x86_wrmsr(MSR_FEATURE_CONTROL, feature_control | FEATURE_CONTROL_MASK);
+
vmcs_revision = vm_basic;
if ((feature_control & FEATURE_CONTROL_MASK) == FEATURE_CONTROL_MASK) {
uint32_t vm_basic_high = vm_basic >> 32;
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
