History log of /seL4-camkes-master/kernel/include/arch/x86/arch/kernel/vspace.h
Revision Date Author Comments
# 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.


# a4d6bf85 28-Feb-2016 amrzar <Amirreza.Zarrabi@data61.csiro.au>

SELFOUR-161: Merge Page_Remap with Page_Map

- Remove Remap function from seL4 API for arm, x86, riscv and the
respective invocation implementation.
- Update Map as replacement for Remap
- Update manual

This allows a change of rights if the frame being mapped is already
mapped in at the given vaddr. To map a page to a different address,
unmap it first.

Co-authored-by: Hesham Almatary <hesham.almatary@data61.csiro.au>
Co-authored-by: Anna Lyons <Anna.Lyons@data61.csiro.au>
Co-authored-by: Victor Phan <Victor.Phan@data61.csiro.au>
Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>


# 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


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

style: consistently align pointer with name

Run astyle with align-pointer=name


# 30738188 13-Mar-2018 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: modeUnmapPage returns whether or not tlb needs invalidation

Whilst it is always correct to invalidate the TLB even if no page was unampped this
provides a small optimization and makes the modeUnmapPage behaviour mirror the general
arch behaviour


# 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


# 9c6fb53c 11-Oct-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Have single makeUserPDEInvalid function

makeUserPDEPageTableInvalid and makeUserPDELargePageInvalid were both just creating the same
kind of thing, an invalid mapping, which really should be thought of as the third type of
PDE entry type.


# 26c81b9f 15-Mar-2017 Hesham Almatary <hesham.almatary@data61.csiro.au>

x86: move pdpte_t to 64/mode and delete it for ia32


# 2fea9a0f 18-Jul-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-567: use seL4_CapRights_t from libsel4

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.


# bdf10bb4 22-Nov-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

Refactor includes so trace point support builds

benchmark.h requires a definition of KS_LOG_PPTR, but its previous
placement in machine.h resulted in a circular include. This commit
factors out KS_LOG_PPTR and related definitions to a separate header,
creates the corresponding header for x86, and prevents circular
includes in the x86 builds


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

x86: Pass address space when invalidating ASID

For efficient TLB coherency on x86-64 it will be useful to know
the address space that the ASID being invalidated was last assigned to


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


# 2320d909 29-Sep-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Fixup IOMMU implementation

Adds a mapping type to frame caps that tracks
what kind of hierarchy the cap is mapped into;
an MMU, IOMMU and in the future an EPT structure.

Additionally the IOMMU code is updated to
have correct functionality and be verification
friendly.


# 75299d05 08-Jul-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-557: s/isIOSpaceFrame/isIOSpaceFrameCap/


# 9aeee987 24-May-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-449 Implement user stack trace on double fault


# 1c1e976d 17-May-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Improve translation invalidation

x86_64 (with PCIDs enabled) supports a more fine grained invalidation
approach for the TLB and Page Structure Cache. This change expands
the number and kinds of information passed for certain invalidations,
and provides an implementation of this for ia32.


# 9e35b398 20-Dec-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Refactor vspace code to have verification friendly invocations


# 0b88c562 06-Dec-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Add missing checks when mapping and unmapping paging objects


# 8b280a07 24-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Introduce mode specific unmap and remap operations


# cf6e5c8e 17-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Use typedef for vspace roots instead of void*


# d93699c9 04-Jan-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-114: remove duplication of seL4_MessageInfo_t, adjust naming to avoid cparser mangling


# d827cf33 21-Dec-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

trivial: style


# 9227ee88 21-Jun-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Move 32-bit specific initial address space creation to vspace_32


# 4e81ed05 05-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Extract 32-bit specific vspace functions in mode/vspace.c


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

x86: With multi-kernel support removed make the kernel PDs etc global instead of passing them around


# 646638ef 09-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Do not conditionally compile IOMMU code, use build/run time checks

Guarding code with #ifdef's makes even cursor testing of 'does this code compile'
difficult due to code being hidden by the pre-processor. Using config_set in
regular C if statements is performant as the compiler can trivially detect
dead code at compile time, and at -O1 and above will not even link in symbols
referenced by dead code in these blocks, so this will not bloat image size


# 5d42d014 09-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Do not conditionally compile IRQ controller code, use build/run time checks

Guarding code with #ifdef's makes even cursor testing of 'does this code compile'
difficult due to code being hidden by the pre-processor. Using config_set in
regular C if statements is performant as the compiler can trivially detect
dead code at compile time, and at -O1 and above will not even link in symbols
referenced by dead code in these blocks, so this will not bloat image size


# 4413fd1b 16-Dec-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Make some vspace code and definitions non-static that get used by the PAE vspace code


# 71a45e6b 05-Nov-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Strip multi kernel support from the x86 kernel. This is not used and is conflicting with planned future features


# 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