You dont really need any kernel support to run multiple kernels on an SMP system. Multiple kernels can operate without a hypervisor or anything complicated like that.
The firmware can prep the kernel boot so that the kernels operate on distinct address spaces, processors and I/O resources. Whereupon you have the challenge to communicate betweeen the kernels which led to various forms of "ethernet" drives communicating via shard memory. This has been done for decades. I have stuff run stuff like this on SGI hardware and Sparc/Neon back in 2003. ARM should also do this without too much fuss. There is even a device driver to share memory between those kernels called XPMEM (which was developed on SGI machines decades ago for exactly this purpose). Its ancient. There is nothing new under the sun as already expressed over 2000 years ago in Ecclesiastes 1:9. ;-) The improvement here is that the burden of implementation away from firmware and we can then have a memory based "ethernet" shared memory implementation indepedent of the architecture. The reason this was done by SGI is to avoid scaling issues. Machines with high numbers of cores can slow down because of serialization overhead in the kernel. The segmentation of the cores into various kernel images reduces the scaling problem (but then lead to a communication bottleneck). The rationale for Sparc/Neon were hardware limitations that resulted in broken cache coherency between cores from multiple sockets. A kernel expected coherent memory and thus one kernel for each coherency domain was a solution. ;-) AFAICT various contemporary Android deployments do the multiple kernel approach in one way or another already for security purposes and for specialized controllers. However, the multi kernel approaches are often depending on specialized and dedicated hardware. It may be difficult to support with a generic approach developed here.
