History log of /seL4-l4v-10.1.1/seL4/include/arch/arm/arch/32/mode/hardware.h
Revision Date Author Comments
# 40c61e5c 18-Jun-2017 Anna Lyons <Anna.Lyons@data61.csiro.au>

Fix licenses (the rest)


# eccaae51 20-Feb-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

s/D61/DATA61/ in license headers for consistency


# 5d146463 18-Jan-2017 Hesham Almatary <hesham.almatary@data61.csiro.au>

ARM: Refactor how we get/set seL4 kernel stack

This commit makes seL4 hold the stack address on TPIDRPRW register (PL1 only
Thread ID Register, VMSA, see B4.1.150 section of ARMv7-A and ARMv7-R
edition reference manual).

Originally, the kernel stack was (re-)mapped to a fixed kernel virtual address and
on traps sp is loaded with this virtual address. Reason is to shave up some
cycles/instructions on (fast) traps path instead of having two instructions
(loading global variable pointer and then memory-load stack address from
it).

With ARM pipelining getting smart/complex (from ARMv7 onwards), there is
no noticeable difference in performance between the two implementations.
Furthermore, this change makes it easy for SMP to load different stacks
for each core and do CPU ID arithmetic efficiently. It also avoids the
issues involving (re-)mapping stacks for different cores if we
followed the original design.

Note: the main side-effect to this change is that the kernel stack for
ARM is no longer mapped with execute-never attribute.


# bdf10bb4 22-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

Refactor includes so trace point support builds

benchmark.h requires a definition of KS_LOG_PPTR, but its previous
placement in machine.h resulted in a circular include. This commit
factors out KS_LOG_PPTR and related definitions to a separate header,
creates the corresponding header for x86, and prevents circular
includes in the x86 builds