#
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.
|
#
554f812d |
|
08-Nov-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
mcs: scheduling context donation over ipc After this commit, threads blocked on an endpoint can recieve a scheduling context from the thread that wakes the blocked thread.
|
#
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.
|
#
f6e5e218 |
|
20-Mar-2019 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
Remove symlinked libsel4 files from include dir These files can be included normally using libsel4 include paths. This removes situations where the same file is available under different include paths due to symlinking into different directory structures.
|
#
7fc45c4e |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: set code width to 120
|
#
d0930f67 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently attach return type Add attach-return-type to astyle
|
#
a3253623 |
|
18-Feb-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
x86: check vcpu is set on seL4_VMEnter Prio to this change the kernel would crash if a thread with no VCPU attempted to seL4_VMEnter. As of this commit, an unknown syscall exception will be raised and the kernel will not crash.
|
#
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
|
#
be458800 |
|
28-Jan-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Prevent RSB based speculation on vmexit A guest, due to its ability to run at the same virtual addresses as the kernel, may have left return values in the RSB that could cause uncontrolled speculation for a Spectre like attack. In all scenarios, with or without IBRS, we need to flush the RSB to guard against this.
|
#
fc0f1eec |
|
04-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
kernel entry tracking: track VMExit and VCPUfault
|
#
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.
|
#
98963c60 |
|
29-Mar-2017 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
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
|
#
9f67d21c |
|
14-Feb-2017 |
Jack Suann <Jack.Suann@data61.csiro.au> |
x86: Handle pending interrupt before scheduling thread in handleSyscall In handleSyscall the current thread may be preempted to handle a pending interrupt. With kernel mode interrupts in x86 this handling was delayed until we were about to switch back to user mode. This change unifies the handling with ARM, where the interrupt is handled prior to calling the thread scheduler.
|
#
76901363 |
|
07-Feb-2017 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
x86 fastpath: save FaultIP on fastpath Otherwise there is no way for user level threads to access the fault ip if threads blocked by the fastpath are resumed by user level.
|
#
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.
|
#
3acbd295 |
|
03-Jan-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Correct fastpath entry logging ksEntry was previously refactored to ksKernelEntry, this old usage was hidden by a previously incorrect #ifdef guard that was corrected in 706eca6ae268496aeba10873d8646089b396c0d7
|
#
706eca6a |
|
02-Jan-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
trivial: correct usage of TRACK_KERNEL_ENTRIES
|
#
c364a243 |
|
12-Dec-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Fix bug where FS and GS clobbered after running VCPU
|
#
d4b1faa8 |
|
12-Dec-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Comment on missing `NODE_LOCK`
|
#
95f40176 |
|
12-Dec-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Add missing `c_entry_hook`
|
#
f658276a |
|
03-Aug-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Remove many DONT_TRANSLATE markers. 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.
|
#
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
|
#
ffd0f34b |
|
08-Nov-2016 |
amrzar <azarrabi@nicta.com.au> |
Clean up x86KScurInterrupt: 1. Remove the locking dependancy on the value of x86KScurInterrupt 2. Remove confusing set/unset of x86KScurInterrupt
|
#
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.
|
#
5f7fa2fc |
|
19-Oct-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
Benchmark: Pack arch-independent benchmark-related files into separate directories
|
#
4c94f43c |
|
26-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x64: Fastpath
|
#
3f9eb7c8 |
|
06-Oct-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-632: implement cores non-architecture dependent structres
|
#
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.
|
#
74cb86c2 |
|
26-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Support for syscall syscall/sysret is an additional way of performing kernel entry/exits. Whilst the instructions themselves are not supported when running in 32-bit mode, this commit provides the config choice for them as well as the generic support code for them.
|
#
2cbc7123 |
|
28-Sep-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-630:preliminary booting application processors - update core detection code and Kconfig file - update kernel stack managment so that BSP does not use boot stack before IPI APs - move arch dependant data to a single structure - add cache line size to Kconfig - add cpu indexing and apic id mapping - boot APs to halting state - add guard for kernel stack if there is only one core
|
#
4044e204 |
|
21-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Revert "Merge pull request #358 in SEL4/sel4 from ~AZARRABI/sel4:multicore to master" This reverts commit ce2f666bb811c5e4c779829fcb09d5a189ebcdbb, reversing changes made to dc183f96b81f2344d7d0d910fc430f924eaae940.
|
#
fbc071b4 |
|
12-Sep-2016 |
amrzar <azarrabi@nicta.com.au> |
SELFOUR-630:preliminary booting application processors - update core detection code and Kconfig file - update kernel stack managment so that BSP does not use boot stack before IPI APs - move arch dependant data to a single structure - add cache line size to Kconfig - add cpu indexing and apic id mapping - boot APs to halting state - add guard for kernel stack if there is only one core
|
#
ef00e986 |
|
21-Aug-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-615: arm entry point stubs
|
#
a217102b |
|
27-Jul-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Consolidate benchmark entry/exit Move the benchmark pre/post ambles into the now existing entry/exit hook functions
|
#
3c05b79a |
|
27-Jul-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Provide generic C entry/exit hook routines It can be deseriable to run code before/after user mode, but not have to write it in assembly. This commit adds such stubs that get called as the first/last C code when coming in and out of the kernel
|
#
5bd050f4 |
|
22-Aug-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
trivial: x86 remove unused lock.[c|h]
|
#
c6247d36 |
|
27-Jul-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-526: Refactor benchmark/debug syscall kernel entry
|
#
f9ea6383 |
|
07-Jul-2016 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
SELFOUR-545: x86 - cleanup c_traps.c file and use new traps.h Closes SELFOUR-545
|
#
b648b297 |
|
22-May-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Reorder c_handle_syscall arguments
|
#
c6139ce4 |
|
01-Jul-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
x86: Rename ia32KScurInterrupt -> x86KScurInterrupt
|
#
37cc3bec |
|
01-Jul-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
x86: Move functions from c_traps_32 to c_traps that are not 32-bit specific
|
#
a99a1040 |
|
09-Nov-2015 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
SELFOUR-279: rename Wait -> Recv, add wrappers for seL4_Poll and seL4_Wait for notification objects. This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely, and changes the return type of seL4_Wait to void (seL4_Wait should be used for notification objects, and seL4_Recv should be used where seL4_Wait was used previously for endpoints).
|
#
5554954b |
|
18-Nov-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
x86: Replace various direct use of __attribute__ with util.h abstractions. Use of these abstractions aids compiler portability, as only a single place in the kernel needs to be adapted. This commit is not intended to affect either verification or generated code.
|
#
88d73db0 |
|
15-Oct-2015 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
refactor tcb_t to remove duplication between x86 and arm header files
|
#
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
|