Disabling hypervisor support

[IkerGalardi]

When using certain virtual machines the EL2 execution level is not supported (for example on the raspberry PI). Is there any way to use a kernel that does not have any virtualization support enabled?

[Ivan-Velickovic]

When using certain virtual machines the EL2 execution level is not supported (for example on the raspberry PI)

Can you give more details on the environment? I don't know what you mean by this (e.g is this with QEMU on the Raspberry Pi, something else?)

Is there any way to use a kernel that does not have any virtualization support enabled?

There would be some code changes required, but since we used to default to non-hypervisor kernel builds it would probably only be minor changes in the tool to get it working again.

[IkerGalardi]

Can you give more details on the environment? I don't know what you mean by this (e.g is this with QEMU on the Raspberry Pi, something else?)

For context, I am creating a small webserver to host static html pages. For that I am using a Raspberry Pi 4 and trying to create a virtual machine using qemu and kvm. Apparently, the processor does not support nested virtualization (what I guess reading the error message qemu gives):

qemu-system-aarch64: mach-virt: KVM does not support providing Virtualization extensions to the guest CPU

The thing is that the project does not use those virtualization extensions, so I decided to remove the guest virtualization extensions by removing the virtualization=on flag on the -machine flags passed to qemu.

Curious thing is that yesterday seL4 complained about not enabling the virtualization extensions and failing to enable the MMU, but today the OS freezes with the next output:

LDR|INFO: Setting all interrupts to Group 1

Should I open another issue about this?

There would be some code changes required, but since we used to default to non-hypervisor kernel builds it would probably only be minor changes in the tool to get it working again.

Currently stuck on another place, but is there an easy way to use a non-hypervisor kernel with the tool? Or are modifications to the source code necesary?

[Ivan-Velickovic]

If you just boot QEMU without KVM, what do you get? Is there a particular reason you are using KVM?

[IkerGalardi]

I need to use KVM mainly for performance reasons.

When booting without KVM the next output:

LDR|INFO|CPU0: active CPUs to start: 0x00000001
LDR|INFO|CPU0: enabling MMU
LDR|INFO|CPU0: CurrentEL=EL1
LDR|ERROR|CPU0: seL4 configured as a hypervisor, but not in EL2
LDR|ERROR|CPU0: failed to enable MMU: 0x00000001

[Ivan-Velickovic]

Can you post the QEMU command you used? I'll try reproduce on a Raspberry Pi 4B locally.

[Ivan-Velickovic]

Currently stuck on another place, but is there an easy way to use a non-hypervisor kernel with the tool? Or are modifications to the source code necesary?

Requires changes to the source code, whether or not seL4 is a hypervisor is set at build time which is why it's a bit harder to have it configurable. To turn off hypervisor you'd need to turn this kernel option off

microkit/build_sdk.py

Line 52 in 2d5a1a6

"KernelArmHypervisorSupport": True,

. There may be some assumptions in the tool that are broken by the kernel not being built as a hypervisor mode.

[Ivan-Velickovic]

(It might be virtualization=on missing from the QEMU command)

[IkerGalardi]

Can you post the QEMU command you used? I'll try reproduce on a Raspberry Pi 4B locally.

The command used with KVM is the next:

qemu-system-aarch64 -machine virt -cpu host -nographic -serial mon:stdio -m size=2G \
                    -smp 1 -netdev user,id=mynet0,hostfwd=tcp::8080-:80 \
                    -device virtio-net-device,netdev=mynet0,mac=52:55:00:d1:55:01 \
                    -global virtio-mmio.force-legacy=false -accel kvm \
                    -device loader,file=build/loader.img,addr=0x70000000,cpu-num=0

(It might be virtualization=on missing from the QEMU command)
Adding that flag displays the next output from qemu:

qemu-system-aarch64: mach-virt: KVM does not support providing Virtualization extensions to the guest CPU

Guess KVM does not support giving virtualization extensions to guest CPUs, so not getting anywere near native performance.

I'll try to build the tool with virtualization disabled and see if anything breaks. If not I could prepare a small PR if I have enough time.

[Ivan-Velickovic]

Sorry, I meant the QEMU command without KVM.

[IkerGalardi]

qemu-system-aarch64 -machine virt -cpu cortex-a72 -nographic -serial mon:stdio -m size=2G \
                    -smp 1 -netdev user,id=mynet0,hostfwd=tcp::8080-:80 \
                    -device virtio-net-device,netdev=mynet0,mac=52:55:00:d1:55:01 \
                    -global virtio-mmio.force-legacy=false -accel kvm \
                    -device loader,file=build/loader.img,addr=0x70000000,cpu-num=0

I am trying to compile the tool on the raspberry pi, but I am unable to get a functioning aarch64-none-elf toolchain. The pipeline uses a prebuilt binary for x86_64, do you also provide an aarch64 version? Debian does not include those on the package manager :/

[IkerGalardi]

I've compiled the microkit SDK by disabling hypervisor support and changing the gcc_cpu of the virt board to cortex-a72 (the one supported by raspberry KVM). Now the kernel freezes with the next log:

LDR|INFO: Setting all interrupts to Group 1

The non-KVM version advances a bit more, but still gets stuck:

LDR|INFO: Setting all interrupts to Group 1
LDR|INFO: GICv2 ITLinesNumber: 0x00000008
LDR|INFO: disabling MMU (if it was enabled)
LDR|INFO: altloader for seL4 starting

Were can I enable more logs to further investigate this?

[IkerGalardi]

I have the loader working on #423, but jumping to the kernel results on an instruction abort exception. If you wanna take a look at it.