Completing the manual's ARM virtualisation section

[Ivan-Velickovic]

I'd be keen to have this section finished/fleshed out, but I'm only familiar with virtualising ARM guests on seL4 from a user-space perspective, which is probably not enough to do the manual section properly. This is a list of things I would put in the manual section, but am looking for things that are missing from the list:

• Explanation of each of the ARM-specific invocations (and how they relate to the faults delivered by seL4).
• VCPU starting state (so that it can be reset properly if you wanted to restart a guest/VCPU).
• GIC versions supported and that GIC is not fully virtualised by the hardware and hence needs some software virtualisation.
• Current limitations of virtualising on seL4. So far I only know of one, which is based on this comment from @kent-mcleod libsel4vm: remove unused function is_active() seL4_projects_libs#71 (comment) which says that suspending and resuming a guest requires more information from the kernel than it currently provides.
• Any differences between AArch32 and AArch64 virtualisation
• Virtualising 32-bit guests on 64-bit host and vice versa, I know it's possible on RISC-V but not sure about ARM.

[Ivan-Velickovic]

Now that SMC forwarding is in the kernel, that should also be mentioned.

[Indanz]

Now that SMC forwarding is in the kernel, that should also be mentioned.

I keep saying this, but: SMC forwarding has nothing to do with virtualisation as such and forwarding is a bad name to being with, because it just makes it possible to make SMC calls from user space. So the "forwarding" bit is forwarding SMC calls upwards from the kernel to the system monitor. This should be documented separately for ARM and not in the virtualisation section, because that will be just confusing.

When a guest VM calls SMC, it traps into the VMM, so SMC calls from the guest are a way to communicate with the host. This you could document in the virtualisation section.

The VMM can implement e.g. ARM's standard PSCI calls any way it wants, a reboot could restart the VM for instance. That it wants to implement an SMC call by doing the real SMC call is more or less coincidence (and the chance of that happening increases with obscure platform specific SMC calls needed to make specific hardware work). It's fine to have a reference to the SMC forwarding section.

[Ivan-Velickovic]

When a guest VM calls SMC, it traps into the VMM, so SMC calls from the guest are a way to communicate with the host. This you could document in the virtualisation section.

That's what I meant yes.

[Ivan-Velickovic]

As well as when you have a guest that needs access to some firmware that's only available via SMC and it is not possible/realistic to emulate the SMC call in the VMM.

[Indanz]

Documentation should be limited mostly to what seL4 provides and does, it should not be a generic guide on how to write a virtual monitor for ARM.

As well as when you have a guest that needs access to some firmware that's only available via SMC and it is not possible/realistic to emulate the SMC call in the VMM.

In that case it's obvious that a real SMC call must be done, no need to point it out in the documentation. That will only confuse people by conflating emulated SMC calls with real ones.

[Indanz]

VCPU starting state

Do you mean the default values of all system registers? That seems too much details for the manual. Also, they can be retrieved before starting the VM.

Current limitations of virtualising on seL4.

That List Registers can't be fully read/written by the VMM should be documented.

Any differences between AArch32 and AArch64 virtualisation

I think the only difference is the name of the registers in seL4_VCPUReg and possibly GICv2 versus GICv3.

Virtualising 32-bit guests on 64-bit host and vice versa

ARM does not support hosting 64-bit guests on a 32-bit host (does anyone? How would you read or write 64-bit registers?).

I'm not sure whether seL4 supports 32-bit guests on 64-bit hosts. You can change the mode to 32-bit and I suspect things will probably just work. That said, seL4 doesn't support 32-bit user space on a 64-bit kernel either AFAIK, but whether that's just missing a way of changing the mode to 32-bit I don't know.

[Ivan-Velickovic]

Do you mean the default values of all system registers? That seems too much details for the manual. Also, they can be retrieved before starting the VM.

Yes, agreed.

ARM does not support hosting 64-bit guests on a 32-bit host (does anyone? How would you read or write 64-bit registers?).

Whoops, sorry, don't why I wrote 'vice versa'.