History log of /seL4-camkes-master/kernel/src/arch/x86/object/tcb.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.


# f4c41f39 30-Aug-2018 Anna Lyons <Anna.Lyons@data61.csiro.au>

x86-smp: remove check on Arch_migrateTCB

This check is not required and aligns the code back with master.


# e04cba09 22-Nov-2016 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: update to build on SMP

Before this commit SMP + MCS did not build.


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

Remove platform IPC buffer register.

This removes the assumption that each platform sotres the IPC buffer
address in a platform-specific register. The IPC buffer address is
instead stored in a thread-local variable in libsel4 which must be
initialised by the runtime.


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

style: consistently attach return type

Add attach-return-type to astyle


# 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


# 2c398b7b 14-Mar-2017 Stephen Sherratt <Stephen.Sherratt@data61.csiro.au>

Abstract setting ipc buffer register into arch fn


# 67cdff7b 14-Feb-2017 Hesham Almatary <hesham.almatary@data61.csiro.au>

SMP: Move/rename migrateTCB() arch tcb.c


# b827ad37 15-Jul-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-413: refactor libsel4 fault API

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


# 33a771d3 12-Jul-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

Split fault types into arch/generic

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.


# 90f6a986 31-Oct-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Initial support for SMP vt-x

Enables vt-x code to compile when CONFIG_MAX_NUM_NODES is set to
greater than 1 and adds code to manage VMCS state on different cores


# 5324972e 09-Nov-2016 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 38b28116 09-Nov-2016 Anna Lyons <Anna.Lyons@data61.csiro.au>

trivial: remove assumption in that x86 has 2 mrs

The fault code for x86 assumes 2 mrs. This change brings the x86 code
inline with arm and uses setMR rather than explicit setRegister.

Note this change will be redundant once arch-fault is merged.


# 44fc989c 03-Nov-2016 amrzar <azarrabi@nicta.com.au>

Store remote FPU state


# a85472a9 02-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Always consider FPU owernship of threads core

When checking if a thread is using the FPU or not we now check on that
threads core, under the assumption that if a thread migrates its FPU
state is explicitly (and not lazily) migrated.


# 3652e827 30-Oct-2016 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


# 25bb9437 24-Oct-2016 amrzar <azarrabi@nicta.com.au>

SELFOUR-635: support for TCB operations
This will update TCB invocations to consider multicore environment, this may include:
- adds the affinity invocation to transfer TCB between different cores and update TCB structure for core ID
- checking the thread/core state before performing TCB operation, e.g. deleting the runnable TCB, etc


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


# 2d462d4a 17-Oct-2016 amrzar <azarrabi@nicta.com.au>

add basic api for setting affinity


# bebfcf6d 23-Jun-2016 Kofi Doku Atuah <kofi.dokuatuah@nicta.com.au>

SELFOUR-499: X86, ARM: Add userspace invocations for hardware debugging

This commit implements the body of SELFOUR-499. The API exposes the x86 DR0-7
and ARM coprocessor 14 features to userspace by virtualizing them as context-
switched registers in the TCB. Implemented as TCB invocations. This feature is
only built when CONFIG_HARDWARE_DEBUG_API is selected.

* Add low-level support routines for setting, unsetting, getting, enabling
and disabling breakpoints.
* Add support for single-stepping as well.
^ Single-stepping is not supported on ARMv6 since the hardware
doesn't have support.
^ ARM implements single-stepping as instruction breakpoints
configured to fault on every instruction -- this is achieved through
the "mismatch" mode, which is only supported from ARMv7 onwards.
* Also support explicit software break requests, a la "BKPT" and "INT $3".

* New invocations:
* seL4_TCB_SetBreakpoint().
* seL4_TCB_GetBreakpoint().
* seL4_TCB_UnsetBreakpoint().
* seL4_TCB_ConfigureSingleStepping().
* New constants:
^ Event types:
^ seL4_InstructionBreakpoint.
^ seL4_DataBreakpoint.
^ seL4_SoftwareBreakRequest.
^ Access types:
^ seL4_BreakOnRead.
^ seL4_BreakOnWrite.
^ seL4_BreakOnReadWrite.
^ Exports:
^ seL4_NumHWBreakpoints.
^ seL4_NumExclusiveBreakpoints.
^ seL4_NumExclusiveWatchpoints.
^ seL4_NumDualFunctionMonitors.
^ seL4_FirstBreakpoint.
^ seL4_FirstWatchpoint.
^ seL4_FirstDualFunctionMonitor.

See documentation in the seL4 API manual.


# 69f140a2 11-Jul-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

trivial: remove duplicated setMRs_syscall_error


# 171824f7 07-Dec-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

Change additional int->word_t due to interraction with the C parser to ease verification


# 0ecff9f3 09-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

unsigned int -> word_t


# 914741ea 27-May-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Make x86 the name of the architecture instead of IA32

IA32 is 32bit version of the x86 architecture. Whilst only IA32
is supported, much of the code is generic x86. Using a generic
x86 architecture will aid in future 64bit support