#
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.
|
#
2dd4a59a |
|
09-Feb-2020 |
Luca(Wei) Chen <Wei@cvluca.com> |
fastpath: force inline fastpath_restore This inline function doesn't get inlined with -O3. It affects the cold cache performance, so use always_inline attribute to tell compiler always get it inlined.
|
#
0e62bc3a |
|
01-Dec-2019 |
Victor Phan <Victor.Phan@data61.csiro.au> |
Move vcpu_switch into Arch_switchToThread Currently the vcpu_switch function is called in the setVMRoot function after possible early returns. In order to make sure the vcpu is always switched, the call is moved into Arch_switchToThread before the call to setVMRoot.
|
#
554f812d |
|
08-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: scheduling context donation over ipc After this commit, threads blocked on an endpoint can recieve a scheduling context from the thread that wakes the blocked thread.
|
#
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.
|
#
fd83c0a3 |
|
20-Mar-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Replace IPC_BUF_GLOBALS_FRAME with KERNEL_GLOBALS_FRAME The globals frame no longer serves its original purpose of informing a thread of its IPC buffer address, and instead as a virtual implementation of thread ID registers.
|
#
01b73622 |
|
27-May-2019 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Consistent naming of FaultIP and NextIP in kernel Always refer to the virtual register that stores the address of a fault as FaultIP and the register that stores the return for a fault NextIP.
|
#
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.
|
#
b2030263 |
|
19-Oct-2018 |
Curtis Millar <curtis.millar@data61.csiro.au> |
Store TLS_BASE in globals frame on fastpath switch. The TLS_BASE stored in the globals frame needs to refer to the TLS_BASE of the current thread and so must be maintained across all context switches. (This was only being maintained on the slow path).
|
#
7d7f338b |
|
07-Aug-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm: Provide TLS_BASE virtual register This commit provides a universal TLS_BASE virtual register on ARM, similar to as exists on x86. Depending on the precise configuration this virtual register maps to a different register * aarch64: TPIDRURW is used for the TLS_BASE and is already declared and being saved and restored on context switches, so this just adds TLS_BASE as an alias of it * armv6: Has no hardware register for use for a TLS_BASE, and so the virtual register gets stored into the globals frame * armv7+: TPIDURO is used for TLS_BASE and so the restore paths are modified to load TLS_BASE into it
|
#
bff71896 |
|
26-Jun-2018 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
arm: remove assumption that CONFIG_IPC_BUF_* must be set Previously arm code assumed that either CONFIG_IPC_BUF_TPIDRURW or CONFIG_IPC_BUF_GLOBALS_FRAME needed to be set. Given that neither of these options are required for aarch64, remove this assumption and only guard code with #ifdefs are required.
|
#
57fa0e0f |
|
07-Aug-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
Share linker.h between architectures
|
#
64d576fb |
|
12-Jun-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-806: aarch32 - Implement lazy FP save/restore This commit implements lazy FP save/restore mechanism, required for user threads when they use the FPU. The following caveats take place: * Only support synchronous exceptions. No support for asynchronous ones. * VFP opcodes are used instead of normal instructions to discard compiler warnings/errors. * Support is limited to specific ARM subarchitectures we support and tested this commit on. * Disable the FPU by default if users are not using it to avoid channels. * FPU support is not verified yet. * Will not work properly if using a VM that's running besides other VMs/threads that are using the FPU.
|
#
0f068083 |
|
29-Apr-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm fastpath: reorder vcpu_switch / armv_contextSwitch_HWASID In the original slow path, armv_contextSwitch_HWASID shoots first. Verification can't reorder machine operations on hardware state we don't model. This puts the fastpath into the same order as the slow path.
|
#
4b491dcf |
|
23-Mar-2017 |
Kofi Doku Atuah <kofidoku.atuah@data61.csiro.au> |
SELFOUR-836: arm-hyp: Config option for saving/loading vs trapping debug state Provides a configuration option for enabling HDCR.TD* traps, or saving and loading debug state on VCPU switches. Currently verification only plans to support the trap setting. As this option complicates all of the #ifdef's related to debug registers even further, abstractions for enabling/disabling each individual piece of the debug code for different configuration options are also implemented. Part of these refactored #ifdef guards was to remove the guards completely from libsel4 around the definitions of the number of breakpoints and watchpoints.
|
#
de6d4772 |
|
30-Mar-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
rename arch_tcb.vcpu -> arch_tcb.tcbVCPU, vcpu.tcb -> vcpu.vcpuTCB struct vcpu { struct tcb* tcb; ... struct arch_tcb { struct vcpu* vcpu; ... and struct tcb { struct arch_tcb tcbArch; ... These conspire to generate a type error on verification side due to assumptions about non-colliding names.
|
#
e8d3672c |
|
01-Mar-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-745: ARM/SMP - Add lock/unlock code to kernel entry/exit points
|
#
48d17e1f |
|
16-Jan-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
ARM/SMP: Prepare for ARM SMP adding stubs Currently building ARM/SMP is broken. This commit: 1- Makes it possible to build ARM/SMP with stubs. Run-time SMP for ARM DOES NOT WORK. 2- Can be a reference for future SMP targets to follow in order to layout/add the minimal required files and functions needed to support SMP. 3- Builds for Sabre only. In order to support other platforms, ipi interrupt ID should be defined in machine.h
|
#
40e89b5d |
|
17-Jan-2017 |
amrzar <azarrabi@nicta.com.au> |
ARM: Move fastpath_restore to mode specific folder
|
#
df977382 |
|
09-Jan-2017 |
Donny Yang <work@kota.moe> |
x64: Rearrange endpoint_cap structure to improve fastpath speed This looks like we're just swapping the positions of capEPBadge and capEPPtr, but it turns out that the bitwise op being performed on capEPPtr to set the high bits were part of the data dependency critical path, so this actually does improve the speed by moving the bitwise op to capEPBadge (albeit it's now an AND instead of an OR) I initially set the field size to 32 bits, but it turns out that causes gcc to emit an instruction (mov r32, r32) that causes the instruction decoder to switch to the legacy decode path for the rest of the fast path for some reason.
|
#
c68a69f8 |
|
19-Dec-2016 |
Donny Yang <work@kota.moe> |
x64: Rearrange cnode_cap structure to improve fastpath speed
|
#
97bac234 |
|
08-Dec-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Remove many MODIFIES annotations. These are redundant for any function which the C-to-Isabelle parser actually analyses, which is now the vast majority of functions.
|
#
fbafb777 |
|
28-Nov-2016 |
Donny Yang <work@kota.moe> |
x64: Always set the high bits of certain pointers in the fastpath seL4 is always in the top of memory, so the high bits of pointers are always 1. The autogenerated unpacking code doesn't know that, however, so will try to conditionally sign extend (in 64-bit mode), which wastes cycles in the fast path. Instead, we can do the unpacking ourselves and explicitly set the high bits.
|
#
e78cdf9b |
|
27-Jul-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-553: Support alternate IPC buffer locations without globals frame This commit adds support for using the ThreadID registers of the ARM MPCore platforms for storing the address of the IPC buffer instead of the globals frame. The choice of using the user readable/writeable ThreadID register is chosen, even though it means the user cannot use it for its own purposes, as it leaves room in the future for doing TLS support in the user read only register, where compilers expect it.
|
#
39c692cc |
|
05-Jul-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-526: ARM - Unify C entry point for system calls
|
#
09358f9b |
|
23-Jun-2016 |
Hesham Almatary <Hesham.Almatary@nicta.com.au> |
SELFOUR-448 Benchmark: Track thread's CPU utilisation time
|
#
5f0ae410 |
|
02-Jun-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
arm-hyp: Minor cleanups Cleanup some small licensing, whitespace and configuration details
|
#
67bcf235 |
|
02-Mar-2016 |
Yanyan Shen <yanyan.shen@nicta.com.au> |
arm_hyp: rm ARM_HYP ifdefs; func inline assembly vcpu.c: encapsulate inline assembly into inline functions that added to device_pl2.h file. other files: replace #ifdef ARM_HYP with config_set(ARM_HYP)
|
#
8e2e8db9 |
|
02-Mar-2016 |
Yanyan Shen <yanyan.shen@nicta.com.au> |
arm_hyp: rm ARM_HYP ifdefs; func inline assembly vcpu.c: encapsulate inline assembly into inline functions that added to device_pl2.h file. other files: replace #ifdef ARM_HYP with config_set(ARM_HYP)
|
#
e61a1056 |
|
03-Feb-2016 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
SELFOUR-56: Remove diminish rights from IPC Diminish rights were to prevent a user from sending a writeable cap over a read only endpoint. It turns out this 'security' can be worked around without difficulty (by putting caps in a cnode and sending the cnode) making the current diminish rights implementation functionally useless. Removing diminish rights has the benefit of simplifying all the IPC paths.
|
#
3fc76c25 |
|
15-Jan-2016 |
amrzar <azarrabi@nicta.com.au> |
Rearranging headers for aarch32 to 32/mode/*
|