Manual: Document ARM Virtualisation

This resolves issue #1083.

Signed-off-by: Indan Zupancic <indan@nul.nu>

libsel4/arch_include/arm/interfaces/sel4arch.xml

@@ -526,7 +526,7 @@
         <method id="ARMVCPUSetTCB" name="SetTCB" manual_name="Set TCB">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Bind a TCB to a virtual CPU
+                Bind a TCB to a virtual CPU.
             </brief>
              <description>
                  There is a 1:1 relationship between a virtual CPU and a TCB. If either (or both) of them is
@@ -549,10 +549,14 @@
         <method id="ARMVCPUInjectIRQ" name="InjectIRQ" manual_name="Inject IRQ">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Inject an IRQ to a virtual CPU
+                Inject an IRQ to a virtual CPU.
             </brief>
             <description>
-                TODO
+                Used to queue IRQs towards the VCPU.
+                Writes <texttt text="ICH_LRn_EL2"/> for GICv3 or <texttt text="LRn"/> for GICv2,
+                where <texttt text="n"/> is determined by <texttt text="index"/>.
+                The list register becomes available again when the guest acknowledges
+                the injected interrupt.
             </description>
             <param dir="in" name="virq" type="seL4_Uint16"
             description="Virtual IRQ ID"/>
@@ -561,10 +565,10 @@
             <param dir="in" name="group" type="seL4_Uint8"
             description="IRQ group"/>
             <param dir="in" name="index" type="seL4_Uint8"
-            description="IRQ index"/>
+            description="VGIC list register"/>
             <error name="seL4_DeleteFirst">
                 <description>
-                    The <texttt text="index"/> is in use.
+                    The <texttt text="index"/> is in use and not yet handled by the guest.
                 </description>
             </error>
             <error name="seL4_IllegalOperation">
@@ -586,12 +590,19 @@
         <method id="ARMVCPUReadReg" name="ReadRegs" manual_name="Read Registers">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Read a virtual CPU register
+                Read a virtual CPU register.
             </brief>
             <description>
-                TODO
+                Provides a way to read EL1 system registers, as well as <texttt text='VMPIDR_EL2'/>.
             </description>
-            <param dir="in" name="field" type="seL4_Word"
+            <return>
+                A <texttt text='seL4_ARM_VCPU_ReadRegs_t'/> struct that contains a
+                <texttt text='seL4_Word value'/>, which holds the value of the system register,
+                and <texttt text='int error'/>, which will be non-zero when an error occurred.
+                <docref>See <autoref label='sec:errors'/> for a description
+                of the message register and tag contents upon error.</docref>
+            </return>
+            <param dir="in" name="field" type="seL4_VCPUReg"
             description="Register to read from a VCPU"/>
             <param dir="out" name="value" type="seL4_Word"
             description="Returned value of the VCPU register"/>
@@ -614,12 +625,12 @@
         <method id="ARMVCPUWriteReg" name="WriteRegs" manual_name="Write Registers">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Write a virtual CPU register
+                Write a virtual CPU register.
             </brief>
             <description>
-                TODO
+                Provides a way to write EL1 system registers, as well as <texttt text='VMPIDR_EL2'/>.
             </description>
-            <param dir="in" name="field" type="seL4_Word"
+            <param dir="in" name="field" type="seL4_VCPUReg"
             description="Register ID to write to a VCPU"/>
             <param dir="in" name="value" type="seL4_Word"
             description="Value to be written to the VCPU register"/>
@@ -642,7 +653,7 @@
         <method id="ARMVCPUAckVPPI" name="AckVPPI" manual_name="Acknowledge Virtual PPI IRQ">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault
+                Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault.
             </brief>
             <description>
                 Acknowledge and unmask the PPI interrupt so that further interrupts can be forwarded

libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h

@@ -53,7 +53,6 @@ typedef enum {
     SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
 } seL4_VMFault_Msg;
 
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
 typedef enum {
     seL4_VGICMaintenance_IDX,
     seL4_VGICMaintenance_Length,
@@ -118,7 +117,6 @@ typedef enum {
     seL4_VCPUReg_Num,
     SEL4_FORCE_LONG_ENUM(seL4_VCPUReg),
 } seL4_VCPUReg;
-#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
 
 #ifdef CONFIG_KERNEL_MCS
 typedef enum {

libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h

@@ -52,8 +52,6 @@ typedef enum {
     SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
 } seL4_VMFault_Msg;
 
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-
 typedef enum {
     seL4_VGICMaintenance_IDX,
     seL4_VGICMaintenance_Length,
@@ -115,8 +113,6 @@ typedef enum {
     SEL4_FORCE_LONG_ENUM(seL4_VCPUReg),
 } seL4_VCPUReg;
 
-#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
-
 #ifdef CONFIG_KERNEL_MCS
 typedef enum {
     seL4_TimeoutReply_FaultIP,

libsel4/tools/syscall_stub_gen.py

@@ -79,7 +79,7 @@
 
 # Headers to include
 INCLUDES = [
-    'sel4/config.h', 'sel4/types.h'
+    'sel4/config.h', 'sel4/types.h', 'sel4/sel4_arch/constants.h'
 ]
 
 TYPES = {
@@ -280,6 +280,7 @@ def init_arch_types(wordsize, args):
             CapType("seL4_ARM_IOSpace", wordsize),
             CapType("seL4_ARM_IOPageTable", wordsize),
             StructType("seL4_UserContext", wordsize * 19, wordsize),
+            Type("seL4_VCPUReg", wordsize, wordsize),
         ] + arm_smmu,
 
         "aarch64": [
@@ -295,6 +296,7 @@ def init_arch_types(wordsize, args):
             CapType("seL4_ARM_SMC", wordsize),
             StructType("seL4_UserContext", wordsize * 36, wordsize),
             StructType("seL4_ARM_SMCContext", wordsize * 8, wordsize),
+            Type("seL4_VCPUReg", wordsize, wordsize),
         ] + arm_smmu,
 
         "arm_hyp": [
@@ -308,6 +310,7 @@ def init_arch_types(wordsize, args):
             CapType("seL4_ARM_IOSpace", wordsize),
             CapType("seL4_ARM_IOPageTable", wordsize),
             StructType("seL4_UserContext", wordsize * 19, wordsize),
+            Type("seL4_VCPUReg", wordsize, wordsize),
         ] + arm_smmu,
 
         "ia32": [

manual/parts/threads.tex

@@ -658,11 +658,34 @@ \section{Virtualisation}
 
 \subsection{Arm}
 
-When a \obj{TCB} has a bound \obj{VCPU} it is allowed to have the mode portion of the
-\texttt{cpsr} register set to values other than \texttt{user}. Specifically it may have any value other than
-\texttt{hypervisor}.
-
-TODO: this section needs more detail
+When a \obj{TCB} has a bound \obj{VCPU} it will have access to (virtualised) system registers,
+cache and TLB maintenance instructions and be able to handle some exceptions itself.
+The virtual GIC will be enabled, allowing virtual interrupt delivery.
+
+The virtualised system registers can be modified with \apifunc{seL4\_ARM\_VCPU\_WriteRegs}{arm_vcpu_write_registers}.
+By configuring the mode portion of the \texttt{SPSR\_EL1} or \texttt{cpsr} register,
+for ARMv8 and ARMv7 respectively, the thread can run in guest kernel mode.
+
+Interrupts are virtualised through the virtual GIC and need to be forwarded with
+\apifunc{seL4\_ARM\_VCPU\_InjectIRQ}{arm_vcpu_inject_irq}, which provides a way to manage
+Virtual GIC List Registers, a queue of pending IRQs to be delivered to the guest. To help
+with managing the list, the Virtual GIC will send GIC maintenance interrupts, which are
+delivered as VGIC Maintenance Faults. List Register state is saved and restored on \obj{VCPU}
+context switch, but there is currently no way to do that manually.
+
+Shared Peripheral Interrupts (SPIs) can be handled like any normal IRQs and forwarded as required.
+
+Virtual Private Peripheral Interrupts (PPI) are trapped and delivered as VPPI Event faults and need
+to be acknowledged with \apifunc{seL4\_ARM\_VCPU\_AckVPPI}{arm_vcpu_acknowledge_virtual_ppi_irq}.
+
+In addition to the above and standard exceptions, others are delivered as VCPU Faults.
+
+Stage 2 translation is enabled when the kernel supports virtualisation. \obj{VCPUs} will have control
+over stage 1 translations and stage 2 translations will be used for the rest of the system.
+As stage 2 translations use VMIDs instead of ASIDs to distinguish address spaces, VMIDs will be used
+to implement seL4 ASIDs. Practically this means that there is an ASID limit of 256 for all threads,
+until 16-bit VMIDs are supported. If more ASIDs are needed, ASIDs will be dynamically re-used, with
+the associated cache flushing and slowdowns.
 
 \subsection{x86}