#
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
|