portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

aarch32: Move tpidruro from vcpu to tcb context

Browse source 
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>
This commit is contained in:
Kent McLeod 2020-05-13 15:08:12 +10:00
parent 8b595ec9de
commit 00a9ba9123
10 changed files with 30 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
CHANGES
View file

@ -22,10 +22,12 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
Further information about [seL4 releases](https://docs.sel4.systems/sel4_release/) is available.
---
Upcoming release: BINARY COMPATIBLE
Upcoming release: BREAKING
## Changes
* aarch32: Moved TPIDRURO (PL0 Read-Only Thread ID register) to TCB register context from VCPU registers. This means
changes to this register from user level have to go via seL4_TCB_Write Registers instead of seL4_ARM_VCPU_WriteRegs.
## Upgrade Notes
---

18
include/arch/arm/arch/32/mode/machine.h
View file

@ -212,6 +212,19 @@ static inline word_t readTPIDRURW(void)
#endif
}
static inline void writeTPIDRURO(word_t reg)
{
asm volatile("mcr p15, 0, %0, c13, c0, 3" :: "r"(reg));
}
static inline word_t readTPIDRURO(void)
{
word_t reg;
asm volatile("mrc p15, 0, %0, c13, c0, 3" : "=r"(reg));
return reg;
}
static inline void writeTPIDRPRW(word_t reg)
{
asm volatile("mcr p15, 0, %0, c13, c0, 4" :: "r"(reg));
@ -229,12 +242,17 @@ static void arm_save_thread_id(tcb_t *thread)
#ifndef CONFIG_KERNEL_GLOBALS_FRAME
/* TPIDRURW is writeable from EL0 but not with globals frame. */
setRegister(thread, TPIDRURW, readTPIDRURW());
/* This register is read only from userlevel, but could still be updated
* if the thread is running in a higher priveleged level with a VCPU attached.
*/
setRegister(thread, TPIDRURO, readTPIDRURO());
#endif /* CONFIG_KERNEL_GLOBALS_FRAME */
}
static void arm_load_thread_id(tcb_t *thread)
{
writeTPIDRURW(getRegister(thread, TPIDRURW));
writeTPIDRURO(getRegister(thread, TPIDRURO));
}
static inline word_t readMPIDR(void)

6
include/arch/arm/arch/32/mode/machine/registerset.h
View file

@ -108,7 +108,9 @@ enum _register {
* name comes from the ARM manual */
TPIDRURW = 18,
TLS_BASE = TPIDRURW,
n_contextRegisters = 19,
/* user readonly thread ID register. */
TPIDRURO = 19,
n_contextRegisters = 20,
};
#define NEXT_PC_REG NextIP
@ -126,7 +128,7 @@ typedef word_t register_t;
enum messageSizes {
n_msgRegisters = seL4_FastMessageRegisters,
n_frameRegisters = 10,
n_gpRegisters = 8,
n_gpRegisters = 9,
n_exceptionMessage = 3,
n_syscallMessage = 12,
#ifdef CONFIG_KERNEL_MCS

12
include/arch/arm/arch/32/mode/machine_pl2.h
View file

@ -168,18 +168,6 @@ static inline void setSCTLR(word_t sctlr)
asm volatile("mcr p15, 0, %0, c1, c0, 0" :: "r"(sctlr));
}
static inline void writeTPIDRURO(word_t reg)
{
asm volatile("mcr p15, 0, %0, c13, c0, 3" :: "r"(reg));
}
static inline word_t readTPIDRURO(void)
{
word_t reg;
asm volatile("mrc p15, 0, %0, c13, c0, 3" : "=r"(reg));
return reg;
}
static inline void writeHTPIDR(word_t reg)
{
asm volatile("mcr p15, 4, %0, c13, c0, 2" :: "r"(reg));

8
include/arch/arm/armv/armv7-a/armv/vcpu.h
View file

@ -434,8 +434,6 @@ static word_t vcpu_hw_read_reg(word_t reg_index)
return getCIDR();
case seL4_VCPUReg_TPIDRPRW:
return readTPIDRPRW();
case seL4_VCPUReg_TPIDRURO:
return readTPIDRURO();
case seL4_VCPUReg_FPEXC:
return reg;
case seL4_VCPUReg_LRsvc:
@ -548,9 +546,6 @@ static void vcpu_hw_write_reg(word_t reg_index, word_t reg)
case seL4_VCPUReg_TPIDRPRW:
writeTPIDRPRW(reg);
break;
case seL4_VCPUReg_TPIDRURO:
writeTPIDRURO(reg);
break;
case seL4_VCPUReg_FPEXC:
break;
case seL4_VCPUReg_LRsvc:
@ -711,7 +706,6 @@ static inline void armv_vcpu_save(vcpu_t *vcpu, bool_t active)
static inline void vcpu_enable(vcpu_t *vcpu)
{
vcpu_restore_reg(vcpu, seL4_VCPUReg_SCTLR);
vcpu_restore_reg(vcpu, seL4_VCPUReg_TPIDRURO);
setHCR(HCR_VCPU);
isb();
@ -792,8 +786,6 @@ static inline void vcpu_disable(vcpu_t *vcpu)
uint32_t hcr;
dsb();
if (likely(vcpu)) {
vcpu_save_reg(vcpu, seL4_VCPUReg_TPIDRURO);
vcpu_hw_write_reg(seL4_VCPUReg_TPIDRURO, 0);
hcr = get_gic_vcpu_ctrl_hcr();
vcpu->vgic.hcr = hcr;
vcpu_save_reg(vcpu, seL4_VCPUReg_SCTLR);

1
libsel4/sel4_arch_include/aarch32/interfaces/sel4arch.xml
View file

@ -25,6 +25,7 @@
<member name="r7"/>
<member name="r14"/>
<member name="tpidrurw"/>
<member name="tpidruro"/>
</struct>
<interface name="seL4_ARM_PageDirectory" manual_name="Page Directory"
cap_description="Capability to the page directory being operated on.">

1
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h
View file

@ -94,7 +94,6 @@ enum {
seL4_VCPUReg_NMRR,
seL4_VCPUReg_CIDR,
seL4_VCPUReg_TPIDRPRW,
seL4_VCPUReg_TPIDRURO,
seL4_VCPUReg_FPEXC,
seL4_VCPUReg_LRsvc,
seL4_VCPUReg_SPsvc,

2
libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/types.h
View file

@ -20,6 +20,6 @@ typedef struct seL4_UserContext_ {
/* other integer registers */
seL4_Word r2, r3, r4, r5, r6, r7, r14;
/* Thread ID registers */
seL4_Word tpidrurw;
seL4_Word tpidrurw, tpidruro;
} seL4_UserContext;

4
libsel4/tools/syscall_stub_gen.py
View file

@ -271,7 +271,7 @@ def init_arch_types(wordsize):
CapType("seL4_ARM_VCPU", wordsize),
CapType("seL4_ARM_IOSpace", wordsize),
CapType("seL4_ARM_IOPageTable", wordsize),
StructType("seL4_UserContext", wordsize * 18, wordsize),
StructType("seL4_UserContext", wordsize * 19, wordsize),
],
"aarch64": [
@ -300,7 +300,7 @@ def init_arch_types(wordsize):
CapType("seL4_ARM_VCPU", wordsize),
CapType("seL4_ARM_IOSpace", wordsize),
CapType("seL4_ARM_IOPageTable", wordsize),
StructType("seL4_UserContext", wordsize * 18, wordsize),
StructType("seL4_UserContext", wordsize * 19, wordsize),
],
"ia32": [

2
src/arch/arm/32/machine/registerset.c
View file

@ -26,7 +26,7 @@ compile_assert(
const register_t gpRegisters[] = {
R2, R3, R4, R5, R6, R7, R14,
TPIDRURW,
TPIDRURW, TPIDRURO
};
compile_assert(
consistent_gp_registers,