Manual: Document ARM Virtualisation

[Indanz]

This resolves issue #1083.

[lsf37]

Modulo the compile error, this looks good from my side.

[Ivan-Velickovic]

Cool, thank you for doing this.

Looking back at the issue I made, some of the things mentioned probably don't belong in the manual.

What about things like vGIC version supported? Right now VMMs have emulated GICv2 and GICv3 but not GICv4. Is virtualising the ITS for GICv4 just in the VMM, or is some support from seL4 needed? Either way, I think it is not harmful to be clear about what vGIC versions are supported.

[Indanz]

Looking back at the issue I made, some of the things mentioned probably don't belong in the manual.

I must admit I wrote the documentation before re-reading your wish list. There are some items there that would be good to add.

Finding the right balance of what makes sense in the manual and what not is hard.

What about things like vGIC version supported? Right now VMMs have emulated GICv2 and GICv3 but not GICv4. Is virtualising the ITS for GICv4 just in the VMM, or is some support from seL4 needed? Either way, I think it is not harmful to be clear about what vGIC versions are supported.

I would say virtual GIC support follows the platform GIC support. We don't specify what platforms are supported in the manual either. Furthermore, documenting which vGIC versions seL4 supports doesn't help the user. Also, this documentation can get out of date easily when the kernel gets updated.

The difference in the kernel's implementation of virtual GICv2 and GICv3 is small enough that it's not worth mentioning. AFAIK the only user visible change is the amount of list registers. When we add vGICv4 support things may change enough that it needs pointing out, but if it's all hidden away in registers and ITS programming in user space, the kernel API stays the same.

The main goal of the manual is to document what functionality seL4 provides to write a VMM and virtual GIC driver in user space. Its goal is not to document how to write a VMM or virtual GIC driver in general. Basically, it's assumed that the reader will or has read the ARM documentation and needs to know how to apply that to an seL4 system. That said, perhaps it's good to say this explicitly and give a broader overview how ARM virtualisation works and to define the scope of seL4's part. Would that be helpful?

[Ivan-Velickovic]

Its goal is not to document how to write a VMM or virtual GIC driver in general. Basically, it's assumed that the reader will or has read the ARM documentation and needs to know how to apply that to an seL4 system

Sure, makes sense.

That said, perhaps it's good to say this explicitly and give a broader overview how ARM virtualisation works and to define the scope of seL4's part. Would that be helpful?

I think so. I guess I was mainly looking for somewhere that describes seL4's capabilities as a hypervisor on ARM, in a way that could be potentially compared to other hypervisors. This is why I thought it would be good to document things like current limitations.

Whether this belongs in the manual, I do not know.