I looked into the Rump Kernel Hypervisor thread briefly in conjunction with the seL4 multi-microkernel documentation. Typical usage of seL4 is as a hypervisor for embedded Linux or another kernel. The license of seL4 is 2-clause BSD for user-mode code (or frontside kernel presumably) isolated from its GPL2 interior by a syscall linkage exception.
My question involves driver implementation speed: would having a hypervisor based on seL4 help prevent crashes when writing custom drivers? According to the docs, DMAs are beyond the control of the MMU on the CPU so they can still crash the system. But other drivers on the frontside kernel could assumably still benefit.
I don’t expect this to drop in until after beta 5 but it might give me something useful to look into. I was initially thinking of building it on @trungnt2910 's Hyclone project but using Haiku’s own kernel might even be possible (I hope).
I think the point was Hyclone is user land code, debugging driver level code is a little pointless. Hyclone I presume just uses the Linux as installed. Certainly, if Hyclone ran under Windows, it would also be pretty pointless. Jack Burton did have the be api working partly under Windows back in the noughties.
Knowing that Fuchsia used a hypervisor in the Zircon kernel is helpful. Knowing if it helped driver development would be more helpful but at least we wouldn’t be out on a limb.
Since the only categories of drivers missing for Haiku now are Bluetooth and GPU drivers, I’m beginning to have second-thoughts about the hypervisor. GPUs often have an IOMMU independent of the CPU’s MMU and would not benefit much from this kind of hypervisor. Bluetooth is a wireless extension of the USB standard also so it might still benefit but at what cost?
Genode already uses many of the L4 microkernels and leverages Linux drivers. If I’m going to try to use L4Re instead of seL4, I’ll be learning some other system than what I wanted to get familiar with. Is there any compatibility chart with respect to different L4 kernels?
