#
512a0200 |
|
19-Mar-2020 |
Qian Ge <qian.ge@data61.csiro.au> |
replacing all ifndef with pargma once All the kernel header files now use pargma once rather than the ifndef, as the pre-processed C files do not change while header files are protected with pargma once. This will also solve any naming issues caused by ifndef.
|
#
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.
|
#
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.
|
#
142bf9b1 |
|
21-Mar-2019 |
Sylvain Gauthier <sylvain.gauthier@data61.csiro.au> |
More standard constant name, moved ASID constants to arch generic files
|
#
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.
|
#
d0930f67 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently attach return type Add attach-return-type to astyle
|
#
761006e0 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently align pointer with name Run astyle with align-pointer=name
|
#
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.
|
#
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
|
#
43b4c551 |
|
06-Jan-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Separate definition for kernel vspace root Introduces a separate definition for vspace root that the kernel runs on. Having this be distinct from the global vspace root allows for potential future distinction between the global root (that is copied into all user address spaces) and the address space that the kernel runs in.
|
#
6d1c8883 |
|
05-Jan-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x64: Rename global paging structures to kernel Currently the kernel address space and paging structures are used as the global ones. This commit renames the paging structures from Global to Kernel to reflect this and allows for separate global structures to be introduced in the future.
|
#
65ab9fd9 |
|
02-Oct-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Return instead of failing in mode cap functions Verification will guarantee that all usages of the parent cap_get* functions will be correct and that this case does not happen. However, it is difficult to prove that the `fail` cannot happen in isolation, and is ultimately not neccessary.
|
#
f85fb62f |
|
21-Aug-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-1062: Hide all VT-x related code behind #ifdef guards The VT-x implementation is not going to be verified at the moment, and so the code for it needs to be hidden from verification, which we do by #ifdef'ing it out if the VT-x is not enabled. As a result the VT-x configuration depends on a non verification target
|
#
40c61e5c |
|
18-Jun-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
Fix licenses (the rest)
|
#
9ca253a3 |
|
07-May-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-879: expose index and entry constants
|
#
34fe58a3 |
|
21-Feb-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
Fix: add pdpt stuff removed from shared x86 code to x86_64
|
#
eccaae51 |
|
20-Feb-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
s/D61/DATA61/ in license headers for consistency
|
#
017d7863 |
|
05-Dec-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x64: VT-x related cap and object definitions * 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
|
#
2c49729d |
|
08-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Refactor tlb_bitmap to be mode generic Refactors the TLB bitmap code to be generic across ia32 and x86-64.
|
#
9c91fc8f |
|
08-Nov-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Refactor generic x86 pte/pde manipulation Previously generic functions for manipulating page table and page directory entries were placed in mode/structures.h. These are moved to a mode/vspace.h instead so that they can use existing functions defined in arch/vspace.h. The x86_make_pde_mapping function is dropped in this move as it is not used. Instead it is replaced with a function for creating an empty mapping for whatever is the vspace root.
|
#
da409659 |
|
27-Oct-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x64: Match ASID changes on ia32
|
#
b90238d0 |
|
19-Oct-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Replace #pragma once with include guards
|
#
f062dcdc |
|
11-Oct-2016 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
7f9970e5 |
|
20-Dec-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
x64: Add x86_64 support
|