This commit is a re-arrangement of SMP directory structure to make it
easier for other architectures/platforms (in general) and ARM (in
particular) to add SMP support.
* new include/smp directory to act as a centralised container of
"shared" architecture-independent SMP headers.
This makes it clearer what's needed for other architecture/platform to
support SMP.
* Each platform can define its own unique ipi.[h|c] that make sense,
since ipi implementation is SoC/platform dependent.
Circular dependency prevents extern definition of benchmark_log_utilisation_enabled from
getting included in include/arch/arm/arch/benchmark_overflowHandler.h.
arch-level headers shouldn't depend on arch-independent headers to avoid
such circular dependency issues (in the future).
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.
Previous code to return to user level performed
popf
sysexit
The popf was just before the sysexit as there is a one instruction
delay on the trap flag taking effect and ensured we did not attempt
to single step the kernel. Unfortunately there is not a one instruction
delay on enabling the interrupt flag, and as a result an interrupt
can be taken prior to executing the sysexit instruction. It is
possible to exploit this to escalate a user level thread such that
it is running with CPL0
This commit changes the restore paths to perform
sti
sysexit
Which will correctly delay interrupts until the completion of sysexit.
As the popf is now being done earlier to prevent single stepping the
kernel we return via an iret, instead of sysexit, for threads that
have single stepping enabled. To achieve this we
* When loading debug state if we enable the Trap flag we also manipulate
the register state such that the iret return path will be picked
* As fastpath_restore does not have an iret return path we forbid
the fastpath from switching to threads that have single stepping
enabled
* Adds object and cap definitions for VT-x structures (VCPU and EPT).
* Extends the asid_map implementation to support ASIDs in the EPT
* Adds size definitions for VCPU and EPT objects
* commit '6cd485204f0b3ca09a42770c545f0724189e7b78':
x86: Add Skylake-related info
x86: Add support for more architectures in reading the TSC frequency
This actually leads to better code. Copies of the halt loop inlined
in various places will instead be single instructions 'bl halt'. It's
also important for the translation validation to avoid having
pointless loops everywhere, especially inside the bodies of other
loops.
The vast majority of the DONT_TRANSLATE markers in the kernel are used
to hide __asm__ statements and builtin functions
(e.g. __builtin_unreachable ()) from the C-to-Isabelle parser.
The parser now supports underscore identifiers and many __asm__ statements,
and the builtin functions are prototyped, meaning the vast majority of the
DONT_TRANSLATE markers can be dropped. The remaining markers cover functions
that must be treated specially.
Add compatible prototypes for compiler builtins
__builtin_unreachable, __builtin_ctzl, __builtin_clzl,
and __builtin_popcountl.
The compiler ignores these, but they are necessary for the Isabelle
C parser to handle them. This is needed to drop DONT_TRANSLATE markers
from various functions which call these builtins.
Previously we threw away any modifications the kernel may have made
to the EFER when a VM exit happens. In x86-64 there are modifications
to the EFER that must be preserved
This unifies the interface provided by ia32 and x86-64. This interface
is neccessary as it is not always sufficient to talk about the current
PD (or vspace root), as CR3 can contain more than just the root.
x86-64 has better ways (`swapgs`) of managing per core kernel stacks.
This commit hides the `kernelSP` member of a `vcpu_t` under x86-64
so as not to cause confusion and accidental attempted usage
Previously the GP registers for a VCPU were defined in the 32-bit
arch registerset. This does not actually make sense as the mode
for the VCPU should be decoupled (and well defined) regardless of
the execution mode of the kernel. This commit provides an explicit
definition and register order for VCPU GP registers.
Uninitialized data structures in BOOT and PHYS code currently get
placed in sections that are allocated in the file of the final image.
Whilst these sections will get reclaimed during kernel boot, so no
runtime memory is being wasted, it results in kernel images that
are much larger to load and transport than necesary.
This change adds explicit BSS regions for both BOOT and PHYS code
and moves all appropriate data structures into them
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.
This commit moves the write to FS and GS base, allowing for a much
more efficient write to GS base under x86-64 SMP. When writing
GS base was in Arch_switchToThread it was neccessary to write to
an MSR such that when swapgs was performed on kernel exit the new
value of GS base would be retrieved. Unfortunately writing to an
MSR is very expensive and we would much prefer to use the writegsbase
instructions instead. By moving this code to restore user context
we are able to call swapgs earlier and then use the normal
writegsbase instruction
When using, SSE (and other variants), mxcsr would assume similar role as
control word in i387 FPU. When initializing the FPU, it should have valid value.
In the common case this function expands to a single check, with a blank
body. Whilst forcively inling will cause code bloat, will be code bloat
in the uncommon code path, which we do not care about
config_default was intended to either evaluated to the passed configuration
value, or the a default value if the config didn't exist. For integer values
this does not actually work, and the default value always gets returned.
This commit reimplements the desired functionality as config_ternary, which
takes 3 arguments, a config to switch on and a desired true and false expansion
* commit 'ed95f84a438aea6365762a180cc493113e9282e0':
SELFOUR-413: changes for verification
SELFOUR-567: use seL4_CapRights_t from libsel4
SELFOUR-413: refactor libsel4 fault API
Split fault types into arch/generic
This change
* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4
Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.
This is a *breaking API change*
This commit:
* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
the user calling seL4_SetTag() first (seL4_MessageInfo is passed
in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes
Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.
Adds a heuristic to switch to a NULL fpu state if we think the FPU
is not presently in use. A NULL fpu state is more efficient as
we do not have to enable/disable the FPU when switching threads
