History log of /seL4-test-master/kernel/include/arch/arm/armv/armv8-a/32/armv/vcpu.h
Revision Date Author Comments
# 2ff45c3c 13-Aug-2020 Siwei Zhuang <siwei.zhuang@data61.csiro.au>

zynqmp: Add support for aarch32 hyp

Enable building AArch32 HYP kernel for ZCU102.

Signed-off-by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>


# 00a9ba91 12-May-2020 Kent McLeod <Kent.Mcleod@data61.csiro.au>

aarch32: Move tpidruro from vcpu to tcb context

This register is visible to software executing at PL0 but not writeable.
Storing it in the VCPU context required custom save/restore handling as
it had to be explicitly handled when switching from a VCPU thread to a
non-VCPU thread so that it didn't become a channel. It is possible to
now update this register via seL4_TCB_WriteRegisters for software
executing at PL0.

This also fixes a bug where if a vcpu-thread is switched for a
non-vcpu-thread and then switched to a different vcpu-thread the
original vcpu-thread's copy of this register will get set to 0.

Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>


# 512a0200 19-Mar-2020 Qian Ge <qian.ge@data61.csiro.au>

replacing all ifndef with pargma once

All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.


# 79da0792 01-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

Convert license tags to SPDX identifiers

This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.


# bddd4054 27-Jan-2020 Alison Felizzi <Alison.Felizzi@data61.csiro.au>

arm: Added define for VMPIDR and VMPIDR_EL2

Added constant definitions for the VMPIDR (arm32) and VMPIDR_EL2
(arm64) registers. These being vcpu registers that can be
written, read, saved and restored. The 'Virtualization Multiprocessor
ID Register' (VMPIDR) is needed to program a vcpu's affinity during
initialisation. This is currently only exposed on SMP configurations.

Co-authored-by: Anna Lyons <anna@gh.st>


# 01514662 22-Jan-2020 Rafal Kolanski <rafal.kolanski@data61.csiro.au>

arm-hyp: provide MODIFIES info for DONT_TRANSLATE

C parser cascades up DONT_TRANSLATE blocking modifies proofs, unless
some kind of spec is provided. This makes the claim that the timer
register getters don't modify any global state, and the setters modify
only state verification does not care about.


# 0e05f416 23-Jun-2019 Alison Felizzi <Alison.Felizzi@data61.csiro.au>

arm: Configure traps on vcpu WFE/WFI calls

Configure the ability to trap on vcpu WFE/WFI calls. If enabled,
user-level would need to schedule a future interrupt when a given
vcpu invokes a WFE/WFI instruction. This otherwise leaving the
vcpu in a disabled state. An application can choose to
disable the trap if it doesn't want to handle the instruction and
schedule a future interrupt.


# 71d636f8 20-Jun-2019 Alison Felizzi <Alison.Felizzi@data61.csiro.au>

arm_hyp: Save and restore vtimer state on switches

Added support for reading and writing additional virtual timer
registers for vcpu hw read and write accesses. These include the
compare value register (CNTV_CVAL) and offset register (CNTV_OFF),
each represented as two 32 bit (high and low) registers on aarch32 and
as single 64 bit registers on aarch64.

Added support for explicitly saving and restoring the virtual
timer registers when the vcpu is enabled and disabled. This
ensures when the vcpu is switched in and out, the virtual timer
registers are restored to a state that is consistent to when
it was last run.

By default the CNTVOFF register will be updated by the kernel to
accumulate the time the VCPU is not running. From the guest this will
result in the VCNT register not increasing when the VCPU is suspended.
This behavior can be turned off by disabling the
KernelArmVtimerUpdateVOffset config option.


# 16bedb98 14-Oct-2019 Kent McLeod <Kent.Mcleod@data61.csiro.au>

arm_hyp: Remove some vcpu_* wrapper functions

These functions have entirely arch specific implementations so remove
function wrapping indirection to ease maintainability.


# 94c7800e 14-Oct-2019 Kent McLeod <Kent.Mcleod@data61.csiro.au>

arm_hyp: Refactor code into arch headers

Move vcpu functions that are specific to a particular Arm architecture
version into the relevant header files. Also move some generic functions
into the generic vcpu header file for use by arch specific headers.


# 5646f774 20-Mar-2019 Curtis Millar <curtis.millar@data61.csiro.au>

RFC-3: Update user context for ARM with thread IDs

Switched appropriate naming conventions.
Was using the aarch64, have switched to aarch64 names.

TIPDRURW -> tpidr_el0
TPIDRURO -> tpidrro_el0
TPIDRPRW -> tpidr_el1

Switch TLS register on aarch32 from TPIDURO (tpidrro_el0) to tpidr_ro so
that it can be written to from user-land.

Thread ID registers tpidr_el0 have been added to the user context for
aarch32 and aarch64.

Only the thread ID that is writeable from EL0 is saved in the TCB and
saved/restored on context switch.

Thread IDs that are only changed within a VM (the read-only thread ID
for exception level 0 and the thread ID for exception level 1) are
stored in the VCPU and saved and stored as part of VM enable/disable.

Thread IDs that are only changed with VMs have been separated out into
hypervisor code.


# d0930f67 18-Mar-2019 Anna Lyons <Anna.Lyons@data61.csiro.au>

style: consistently attach return type

Add attach-return-type to astyle


# 3d10ef0c 18-Mar-2019 Anna Lyons <Anna.Lyons@data61.csiro.au>

style: correct parenthesis padding

Use astyle's unpad-paren to unpad all parentheses that are not included
by pad-header, pad-oper, and pad-comma.


# 723aa0ea 04-Jul-2018 Adrian Danis <Adrian.Danis@data61.csiro.au>

arm: Use TCB version of TPIDRUR[OW] state

These registers are part of the 'regular' TCB state and are saved and restored as part
of normal thread switching. As such it is conflicting to have a duplicate idea of the value
of these registers, especially as it is not kept in sync with the version in the TCB,
which is what is actually being loaded into the hardware.


# 693f7cf2 31-May-2018 Yanyan Shen <yanyan.shen@data61.csiro.au>

armv7/hyp: use break in vcpu_hw_write_reg

C parser does not like void functions attempting to return
with a parameter, even if the parameter has type void.


# 7e8bbcc5 06-Apr-2018 Yanyan Shen <yanyan.shen@data61.csiro.au>

armv7/hyp: Move armv7 code armv7-a/armv/vcpu.h


# 997f508f 06-Apr-2018 Yanyan Shen <yanyan.shen@data61.csiro.au>

arm/hyp: Add timer functions


# da4af028 06-Apr-2018 Yanyan Shen <yanyan.shen@data61.csiro.au>

arm/hyp: Add setters/getters for SPSR registers


# bc162cae 04-Apr-2018 Yanyan Shen <yanyan.shen@data61.csiro.au>

armv7/hyp: Move v7 hyp code to armv7-a/armv/vcpu.h