History log of /seL4-l4v-master/seL4/src/arch/x86/64/c_traps.c
Revision Date Author Comments
# 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.


# 56a19e05 13-Feb-2020 Matthew <matt.phillips121@gmail.com>

Kernel-Vtx: Use clang compatible inline assembly

Specifying a function name prefixed with 'm' is not compatible with
clang.

For 32 bit, call vmlaunch_failed explicitly from within the assembly.
Requires adding the USED attribute to vmlaunch_failed as it is only
referenced in a string literal.

For 64 bit, move the address of vmlaunch_failed into rax as an integer
rather than loading it as the address of a function (lea).


# 3207abee 20-Mar-2019 Curtis Millar <curtis.millar@data61.csiro.au>

RFC-3: Update context for x86 to use FS and GS.

TLS_BASE virtual register is replaced with FS_BASE and GS_BASE virtual
registers.

The FS_BASE and GS_BASE virtual registers are moved to the end of the
context so they need not be considered in the kernel exit and entry
implementation.

Removed tracking of ES, DS, FS, and GS segment selectors on kernel entry
and exit.

ES and DS are clobbered on kernel entry with the RPL 3 selector for a
DPL 3 linear data segment.

FS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with FS_BASE as the base. This is done on exit to reload the value from
the GDT.

GS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with GS_BASE as the base. This is done on exit to reload the value from
the GDT.

Kernel entry and exit code is refactored, simplified, and improved in
light of the above changes.

x64: update verified config to use fsgsbase instr

The verification platform for x64 relies on the fsgsbase instruction.


# 7fc45c4e 18-Mar-2019 Anna Lyons <Anna.Lyons@data61.csiro.au>

style: set code width to 120


# 306453e3 18-Mar-2019 Anna Lyons <Anna.Lyons@data61.csiro.au>

style: set min-conditional-indent to 0

Given we use braces all the time conditional indents do not make code
cleaner.


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


# cf113c61 12-Mar-2019 Jasper Lowell <jasper.lowell@data61.csiro.au>

x86_64: Use sys[ret/exit]q instead of rex prefix

Clang does not support the rex.w instruction prefix and instead requires
sys[ret/exit] mnemonics.


# f0594ac9 28-Jan-2018 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Implement IBRS based Spectre mitigations

Provides the ability to enable the IBRS hardware Spectre mitigation strategies, as well
as completes the software mitigation by disabling jump tables in compilation. The
hardware mitigations are largely provided "for completeness" in the hopes that they
eventually become less expensive. For the moment there is no reason to turn on any
beyond STIBP if running in multicore


# 374da850 16-Jan-2018 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 29695d26 07-Jan-2018 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: SKIM window to mitigate Meltdown (CVE-2017-5754) on x86-64

Introduces a kernel option that, when enabled, reduces the kernel window in a user address
space to just be Static Kernel Image and Microstate (SKIM), instead of the full kernel
address space. This isolates the important kernel data from the user preventing a
Meltdown style attack being able to violate secrecy. The kernel text and read only data,
i.e. anything that is static from boot, is not secret and can be allowed in the SKIM window
and potentially read by the user. Additionally to switch to and from the actual kernel
address space a small amount of state needs to also be in the SKIM window.

This is only an implementation for x86-64, although the same design is applicable to ia32


# a9dc424a 05-Jan-2018 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Remove IRQ stack from per core data structure

The IRQ stack represents state that needs to be available in all contexts, both when user
code is running and when kernel code is running. Separating its definition from all the
other mode state provides the option in the future for treating it differently.


# 39987877 06-Jan-2018 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Correctly reset kernel stack on nested interrupt

Previous code assumed that the kernel stack was size aligned and attempted to reset the stack
pointer by masking and adding. The assumption that the kernel stack is size aligned is strictly
not true, and this lead to resetting the kernel stack to 'random' memory, and corrupting it.

The solution used here is to directly pass in a new value for the stack top.


# 2bf586fe 27-Aug-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Correct return type of servicePendingIRQ

This function returns an interrupt_t, and its call sites expect an interrupt_t,
despite the types being written as irq_t.

Closes #66


# ee28936d 18-Jun-2017 Hesham Almatary <hesham.almatary@data61.csiro.au>

SMP: Introduce ENABLE_SMP_SUPPORT

- Make it more readable and less confusing compared to the 'CONFIG_MAX_NUM_NODES > 1' check


# 40c61e5c 18-Jun-2017 Anna Lyons <Anna.Lyons@data61.csiro.au>

Fix licenses (the rest)


# 27b4411e 21-May-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Correct calls to loadAllDisabledBreakpointState

This function was changed to take a tcb_t* instead of a arch_tcb_t* but these
call sites were not updated


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


# 93cc22b2 09-Mar-2017 amrzar <azarrabi@nicta.com.au>

smp: fix bugs when stalling remote core

- Restart TCB from inside the lock if it is waiting for anything other than IRQ
- Only replace the TCB with idle thread if it is in ThreadState_RunningVM state

Also, this makes the design generic to be shared with arm.


# 0707ae87 23-Feb-2017 amrzar <azarrabi@nicta.com.au>

Move arch independent functions to generic files and HAVE_FPU config


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

s/D61/DATA61/ in license headers for consistency


# eae662c7 01-Feb-2017 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# cea45cd1 31-Jan-2017 Jack Suann <Jack.Suann@data61.csiro.au>

x86: Handling pending interrupts in kernel mode

This commit allows x86 to completely handle a pending interrupt without switching
out to user mode. To handle an interrupt on x86 the APIC *must* generate an exception,
prior to you being able to acknowledge it. Previously we only allow exceptions (i.e.
interrupts) to be generated outside of kernel mode when we are in user mode.

This change allows us to 'poll' for an interrupt and transition the APIC whilst in kernel
mode by enabling and taking interrupts at carefully defined points. A pending interrupt
will be stored by the exception handler, allowing us to then handle the interrupt and
acknowledge the hardware APIC. Handling is done by waiting until after we have 'left' the
kernel and are about to switch to user mode and then 'entering' the kernel again by jumping
to the interrupt entry point.

Handling interrupts entirely in kernel mode provides two advantages
* It will allow, in the future, the ability to handle kernel interrupts in situations
where we need to handle the interrupt before actually performing the hardware switch
back to user mode. This case happens where the user thread is using vt-x and so
pending interrupts do not generate an interrupt exception, but rather cause an exception
to be generated telling the system that there is a pending interrupt
* Where there are multiple pending interrupts it is more efficient to avoid additional
switches in and out of the user thread

Whilst this change does not enable pre-emption points to handle the interrupt before
returning out of `handleSyscall` it should be easily implementable with what is provided.


# 233202b3 29-Jan-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Remove more usages of hard coded stack sizes


# 9dba8e67 15-Dec-2016 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# c5a4e4a1 06-Dec-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: VT-x entry/exit routines


# 564b9839 05-Dec-2016 Donny Yang <work@kota.moe>

x86: Avoid writing the fs/gs base if we don't have to


# 78009dd2 28-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-675: x64: Increase message registers from 2 to 4


# d73d0e8f 24-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Write FS and GS base when restoring user context

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


# 1c312610 23-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Switch to NULL FPU state if suspect no one using it

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


# 72f3ea2e 21-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Comment x_x64_handle_interrupt


# 09356a3e 13-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Release lock when returning from kernel


# a0cb9e67 09-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Support multiple kernel stacks

Adds support for per-core kernel stacks through the use of
thread local storage and swapgs. In addition to the main
kernel stack the IRQ stack also needs to be made per core


# 6f908324 06-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Access core local state correctly


# 120a5e54 27-Oct-2016 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 679d28c9 27-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Correct FPU handling code


# 6a86cbf5 26-Oct-2016 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 7fbde1bb 14-Jun-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-287: 32-bit vt-x implementation

This is an implementation of vt-x for x86 kernels running in
ia32 mode.


# cfe0f8e9 12-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Support for hardware debugging when using SYSENTER

Hardware debugging was already supported if using SYSCALL for kernel
invocations, this adds support for when using SYSENTER. SYSENTER
is special because when entering the kernel the TF flag is not masked,
so the case of taking a debug exception in the kernel needs to be
handled. Also, unlike ia32, there is a race between performing
popf and calling sysexit where interrupts can be received. This race
is avoided by performing a full state restore with iret if a thread
is single stepping.


# 0e1a8071 13-Oct-2016 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 235a02ec 12-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Use FLAGS_* defines instead of magic numbers


# b01cf7f0 12-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Make stack.h a mode specific header

The functionality of setKernelEntryStackPointer is all ia32 specific and
this commit moves this to a mode specific include location


# 6d07c443 10-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x64: Partial hardware breakpoint support

This only implementes debug support if using the SYSCALL kernel invocation
method, will not work yet with SYSENTER


# 6294225c 10-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Rename [ER]FLAGS to FLAGS

Having a different name for the FLAGS register creates an unnecessary difference
between ia32 and x86_64 code since regardless of the name/size the bits in the
register mean exactly the same thing


# 7f9970e5 20-Dec-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x64: Add x86_64 support