#
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.
|
#
50b1b0a7 |
|
25-Feb-2019 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
arm: Move SYSTEM_*_WORD macros to armv header file This is needed to avoid circular include dependencies that result from other header files trying to use these macros.
|
#
e11d930b |
|
05-Jul-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Move some lockTLB magic into C. This patch moves the 'outer' chunk of lockTLBEntry into C rather than handwritten assembly. The outer chunk accesses a global counter and does arithmetic. The inner chunk (lockTLBEntryCritical) writes to the registers, must be specially aligned, and is generally special. The change reduces unnecessary handwritten assembly, and also avoids a special case that was problematic for binary verification.
|
#
60aac65c |
|
05-Mar-2018 |
Sebastian Holzapfel <seb.holzapfel@data61.csiro.au> |
ARM/v7-a: Force -O2 compilation of idle thread This fixes a problem with -O0 SMP builds on ARM visible as kernel data aborts whenever the idle thread executes. The idle thread receives no stack pointer. At -O2, this is fine as the wfi() call is inlined and stack operations in idle_thread are optimized out. At -O0, the stack operations remain and wfi() is not inlined, resulting in stack accesses in the idle thread that cause data aborts. Forcing -O2 behaviour was deemed the simplest solution for now. Giving the idle thread a stack would have had larger verification ramifications for what is now a fairly uncommon use case.
|
#
19b89ed1 |
|
14-Jan-2017 |
amrzar <azarrabi@nicta.com.au> |
ARM: Add 32 bit directory for armv8-a
|
#
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.
|
#
57f1352f |
|
21-Aug-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-614: calling halt() on the hikey platform results in infinite data abort SELFOUR-408: halt does not halt Remove assembly files for halt and idle thread and add wfi in armv.
|
#
91b7da86 |
|
17-Jul-2014 |
TrusthworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|