From d1feeff5d37404708e23948473c911b435e64f11 Mon Sep 17 00:00:00 2001 From: Indan Zupancic Date: Tue, 26 Mar 2024 13:26:41 +0000 Subject: [PATCH 1/3] Manual: Document ARM Virtualisation This resolves issue #1083. Signed-off-by: Indan Zupancic --- .../arch_include/arm/interfaces/sel4arch.xml | 35 ++++++++++++------- libsel4/tools/syscall_stub_gen.py | 3 ++ manual/parts/threads.tex | 25 ++++++++++--- 3 files changed, 47 insertions(+), 16 deletions(-) diff --git a/libsel4/arch_include/arm/interfaces/sel4arch.xml b/libsel4/arch_include/arm/interfaces/sel4arch.xml index a101b0611f0..b6482490104 100644 --- a/libsel4/arch_include/arm/interfaces/sel4arch.xml +++ b/libsel4/arch_include/arm/interfaces/sel4arch.xml @@ -526,7 +526,7 @@ - Bind a TCB to a virtual CPU + Bind a TCB to a virtual CPU. There is a 1:1 relationship between a virtual CPU and a TCB. If either (or both) of them is @@ -549,10 +549,14 @@ - Inject an IRQ to a virtual CPU + Inject an IRQ to a virtual CPU. - TODO + Used to queue IRQs towards the VCPU. + Writes for GICv3 or for GICv2, + where is determined by . + The list register becomes available again when the guest acknowledges + the injected interrupt. @@ -561,10 +565,10 @@ + description="VGIC list register"/> - The is in use. + The is in use and not yet handled by the guest. @@ -586,12 +590,19 @@ - Read a virtual CPU register + Read a virtual CPU register. - TODO + Provides a way to read EL1 system registers, as well as . - + A struct that contains a + , which holds the value of the system register, + and , which will be non-zero when an error occurred. + See for a description + of the message register and tag contents upon error. + + @@ -614,12 +625,12 @@ - Write a virtual CPU register + Write a virtual CPU register. - TODO + Provides a way to write EL1 system registers, as well as . - @@ -642,7 +653,7 @@ - Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault + Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault. Acknowledge and unmask the PPI interrupt so that further interrupts can be forwarded diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py index cbba6e4b43a..d692e85267b 100644 --- a/libsel4/tools/syscall_stub_gen.py +++ b/libsel4/tools/syscall_stub_gen.py @@ -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": [ diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex index b493a00c33f..d6ffef4c48c 100644 --- a/manual/parts/threads.tex +++ b/manual/parts/threads.tex @@ -658,11 +658,28 @@ \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}. +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. -TODO: this section needs more detail +The vitualised 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, which can be done +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 as PPIs. + +Shared Peripheral Interrupts (SPIs) can be handled like any normal IRQs and forwarded as required. + +However, Virtual Private Peripheral Interrupts (PPI) are trapped and delivered as faults instead and +need to be acknowledged with \apifunc{seL4\_ARM\_VCPU\_AckVPPI}{arm_vcpu_acknowledge_virtual_ppi_irq}. + +Stage 2 translation is enabled when the kernel supports virtualisation, but only for \obj{VCPUs}. +Practically this means that there is an ASID limit of 256 for non-virtualised threads running in EL0. +If more ASIDs are used, ASIDs will be dynamically re-used, with the associated cache flushing and +slow downs. \subsection{x86} From ca29c7caec80c7420a22b7d89e8c10116484e6d9 Mon Sep 17 00:00:00 2001 From: Indan Zupancic Date: Tue, 26 Mar 2024 13:36:52 +0000 Subject: [PATCH 2/3] Manual: Params don't have errors Signed-off-by: Indan Zupancic --- libsel4/arch_include/arm/interfaces/sel4arch.xml | 2 +- libsel4/tools/sel4_idl.xsd | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/libsel4/arch_include/arm/interfaces/sel4arch.xml b/libsel4/arch_include/arm/interfaces/sel4arch.xml index b6482490104..911dc5cfa4b 100644 --- a/libsel4/arch_include/arm/interfaces/sel4arch.xml +++ b/libsel4/arch_include/arm/interfaces/sel4arch.xml @@ -26,6 +26,7 @@ VM Attributes for the mapping. Possible values for this type are given in . + A mapping already exists for this level in at @@ -54,7 +55,6 @@ Or, is already mapped in a VSpace. - diff --git a/libsel4/tools/sel4_idl.xsd b/libsel4/tools/sel4_idl.xsd index 187a324cbc0..2118fb238ab 100644 --- a/libsel4/tools/sel4_idl.xsd +++ b/libsel4/tools/sel4_idl.xsd @@ -128,7 +128,6 @@ - From 061c1f1436fa95c3d71b0d9840264cda322fefc9 Mon Sep 17 00:00:00 2001 From: Indan Zupancic Date: Tue, 26 Mar 2024 13:37:42 +0000 Subject: [PATCH 3/3] Manual: Fix Contact Link. Signed-off-by: Indan Zupancic --- manual/manual.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manual/manual.tex b/manual/manual.tex index 2d106954cc7..28924c9f6bb 100644 --- a/manual/manual.tex +++ b/manual/manual.tex @@ -154,7 +154,7 @@ Toby Murray. The authors and contributors can be contacted via the seL4 Developer Mailing -List or the seL4 Discourse Forums. See \url{https://sel4.systems/contact.html} +List or the seL4 Discourse Forums. See \url{https://sel4.systems/contact/} for details. \end{abstract} \thispagestyle{empty}