Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Manual Improvements #1233

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Manual Improvements #1233

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d1feeff
Manual: Document ARM Virtualisation
Indanz Mar 26, 2024
ca29c7c
Manual: Params don't have errors
Indanz Mar 26, 2024
061c1f1
Manual: Fix Contact Link.
Indanz Mar 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
37 changes: 24 additions & 13 deletions libsel4/arch_include/arm/interfaces/sel4arch.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
<description>
VM Attributes for the mapping. <docref>Possible values for this type are given in <autoref label="ch:vspace"/> .</docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
Expand Down Expand Up @@ -54,7 +55,6 @@
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</param>
</method>
<method id="ARMPageTableUnmap" name="Unmap" manual_label="pagetable_unmap">
<brief>
Expand Down Expand Up @@ -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
Expand All @@ -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"/>
Expand All @@ -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">
Expand All @@ -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"/>
Expand All @@ -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"/>
Expand All @@ -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
Expand Down
1 change: 0 additions & 1 deletion libsel4/tools/sel4_idl.xsd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,6 @@
<xsd:complexType name="ParamType">
<xsd:sequence>
<xsd:element name="description" minOccurs="0" maxOccurs="1" type="DescriptionType"/>
<xsd:element name="error" minOccurs="0" maxOccurs="unbounded" type="ErrorType"/>
</xsd:sequence>
<xsd:attribute name="type" type="xsd:string" use="required"/>
<xsd:attribute name="name" type="xsd:string" use="required"/>
Expand Down
3 changes: 3 additions & 0 deletions libsel4/tools/syscall_stub_gen.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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": [
Expand All @@ -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": [
Expand All @@ -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": [
Expand Down
2 changes: 1 addition & 1 deletion manual/manual.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
25 changes: 21 additions & 4 deletions manual/parts/threads.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

typo: vitualised -> virtualised

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, but it's a bit too early for review, this is a placeholder for future commits. I currently have a mess of local modifications I'm still in the process of untangling, but didn't got to yet. I plan to do that the coming weeks.

That typo was part of a work-in-progress commit that shouldn't be part of this PR, would you like to review #1232 which covers ARM virtualisation?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I can do that (not being an expert for ARM).

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}

Expand Down