Hi Anton,

I'm trying to understand how hypervisor functionality support is working in seL4 for aarch32/aarch64. In the documentation there is a list of platforms [1] for some of them ARM_HYP is said to be supported for some not. I was trying to grep through the kernel, but it seemed to me that ARM_HYP can be enabled on any ARM-based platform.

I've tried to compile sel4test for exynos5422 (for which ARM_HYP is said to be enabled) and odroidc2 (for which it is said that it's not supported) with -DARM_HYP=ON manually set, and for both compilation succeeded. It failed for hikey, that should support it, but that's a different story.

The kernel arm hypervisor support is mostly tied to a particular Arm micro-architecture. Currently CortexA15, CortexA57 or CortexA53 are the supported ones. Platforms that use one of these cores will generally be able to be configured with hypervisor support enabled.

So my questions are - How is it defined whether ARM_HYP is supported for a board/SoC, provided that processor architecture supports it? What the platform support code should provide for hypervisor to work? - For platforms not supported by camkes-arm-vm (like, most of the platforms) how ARM_HYP can be tested?

We typically only document support for platforms that the camkes-arm-vm supports: tk1, tx1, tx2, odroid-xu, odroid-xu4 and qemu-arm-virt. Other platforms, such as imx8 and odroidc2 are theoretically supported by seL4, but without the camkes-arm-vm support, we don't test that the hyp support works.

Thanks a lot, Anton Gerasimov

[1] https://docs.sel4.systems/Hardware/

Hope this answers your questions. Kent.