History log of /seL4-camkes-master/kernel/src/arch/x86/32/kernel/vspace.c
Revision Date Author Comments
# a00c2c16 17-Sep-2020 Curtis Millar <curtis.millar@data61.csiro.au>

Make kernel log buffer derived from cmake config

This removes the explicit CMake configuration for the kernel log buffer
and replaces it with a #define that is enabled for the required
configurations.

Signed-off-by: Curtis Millar <curtis@curtism.me>


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


# 66bc2b17 05-Nov-2019 Victor Phan <Victor.Phan@data61.csiro.au>

rename KDEV_PPTR/PPTR_KDEV to KDEV_BASE

This is the virtual address for the start of the kernel device mapping
region.


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


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


# 8586b7f2 07-May-2019 Anna Lyons <Anna.Lyons@data61.csiro.au>

boot: refactor allocation of rootserver objects

Prior to this change, the boot process would dynamically allocate
memory for root server objects based on the order of initialisation.
Allocation was a best-fit algorithm.

This change preallocates all memory for root server objects to an
aligned untyped just after the user image. By allocating the objects in
order of size, allocation is greatly simplified and the ability to
reproduce the allocation offline based on the kernel and user image
sizes is increased.


# 0cdd0514 02-Apr-2019 Anna Lyons <Anna.Lyons@data61.csiro.au>

ia32: adjustments to pass c-parser

This commit updates the ia32 build to pass the c-parser.

- replaces ++i with i++
- use void in functions with no parameters
- add a missing typecast
- remove a void cast of an unused variable

It does not provide any verification guarantees about ia32 code.


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


# 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


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

x86: Define per node arch global state

Global state in this context is state/datastructures that need to be available at all times,
both in user and kernel mode, by the hardware for correct operation. The purpose of creating
a separate per-node structure for it is so that there is the option of treating it specially
in the future from other per node state


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


# 128829a9 11-Sep-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Rationalize names of paging structures

Changes the name of paging structure entries to more clearly indicate the kind of object
they map to. Generally this is changing a `pde_small` to `pde_pt` to indicate that this
mapping refers to a page table, removing an inconsistency where `pde_large` indicated that
the mapping was for a large page. For the same reason the `ept_pde_4k` type is changed to
`ept_pde_pt` type to reflect what is present in the actual entry.

`pde_large` is left as 'large' and not explicitly given a size as code common between
ia32 and x86-64 manipulates these entities and 'large' is already a used abstraction
over the two potential page sizes so there is need to introduce a formal abstraction layer
and make the names in the structures more specific.


# 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


# bc380859 21-May-2017 Bamboo <bamboo@keg.ertos.in.nicta.com.au>

[STYLE_FIX]


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

Avoid using bitfield generated *_ptr_new functions

These functions can cause slow down during verification C parsing and do not currently
have any proofs about them. More importantly there is no performance impact from just
calling the regular *_new functions instead


# 3e57e647 19-Oct-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

SELFOUR-501: x86 - Remove PAE support


# 968a3d25 19-Jan-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

ia32: SELFOUR-771: Avoid duplicate insertion of PD cap


# 60eef86c 14-Dec-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

Benchmark: Fix error due to fault function name change

s/fault_cap_fault_new/seL4_Fault_CapFault_new


# 511f57f5 22-Nov-2016 amrzar <azarrabi@nicta.com.au>

x86: handle switch to kernel space in smp
If multiple TCBs are the only threads which are running on different cores,
deleting the TCBs would result in switch to idle thread and keeping the bitmask set for those cores.
If one of these TCB remains, then it would always IPI those original cores.


# 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


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


# 056dbf81 02-Nov-2016 amrzar <azarrabi@nicta.com.au>

SELFOUR-634: support for TLB and cache management


# a228c492 30-Oct-2016 amrzar <azarrabi@nicta.com.au>

Incuede TLBBitmap in PD to keep track of cores currently accessing this PD


# 66dfc2e7 29-Jul-2016 Kent McLeod <kent.mcleod@nicta.com.au>

Change ia32 to use fs register for IPC buffer

gs register is used by gcc for TLS and the IPC buffer gets in the way


# 5f7fa2fc 19-Oct-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

Benchmark: Pack arch-independent benchmark-related files into separate directories


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


# d72cd751 28-Sep-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

x86: Rename invalidateTLBentry->invalidateTLBEntry


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


# 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


# d507b2d3 09-Feb-2016 Adrian Danis <Adrian.Danis@nicta.com.au>

SELFOUR-421 Introduce explicit device frames and untypeds

Kernel objects cannot be created from device untypeds, with the
exception of frames, which do not get zeroed and cannot be used
as an IPC buffer. Device untypeds additionally cannot be used
in the construction of ASID pools.

This then changes the API to the rootserver (i.e. bootinfo) to
send device untypeds instead of device frames. On ARM these
device untypeds are the same as the previously exported device
frame regions. On x86 PCI scanning is removed and all physical
memory addresses (that are not important for kernel integrity)
are released to the user.

In order to have bits in the frame and untyped caps on ARM the
number of software ASIDs had to be reduced from 2^18 to 2^17,
and the maximum untyped size reduced from 2^31 to 2^30


# 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


# 35c50cfd 29-Aug-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-556: Rationalize BITS vs INDEX_BITS

s/PD_BITS/PD_INDEX_BITS
Current convention is to say that X_BITS is the log base 2
size of an object, not the log base 2 number of indices


# f251953f 29-Aug-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-556: Rationalize BITS vs INDEX_BITS

s/PT_BITS/PT_INDEX_BITS
Current convention is to say that X_BITS is the log base 2
size of an object, not the log base 2 number of indices


# 935b055c 28-Aug-2016 Adrian Danis <Adrian.Danis@data61.csiro.au>

SELFOUR-556: Rationalize BITS vs INDEX_BITS

s/PDT_BITS/PDPT_INDEX_BITS
Current convention is to say that X_BITS is the log base 2
size of an object, not the log base 2 number of indices


# 16c34811 31-Jul-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

SELFOUR-518: User-level log buffer

Remove global ksLog and use KS_LOG_PPTR instead

Benchmark - Log buffer: use global page table


# 90628a75 11-Aug-2016 Hesham Almatary <hesham.almatary@data61.csiro.au>

Benchmark: share and use KS_LOG_PPTR and PPTR_TOP for x86 and ARM


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

SELFOUR-557: s/isIOSpaceFrame/isIOSpaceFrameCap/


# 09358f9b 23-Jun-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-448 Benchmark: Track thread's CPU utilisation time


# bcf0a235 01-Jun-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-446 Unify code base for trace points and track feature


# 7cbaeb8e 30-May-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-446 Benchmark: Track interrupts and user/vm faults


# fc1feb67 24-May-2016 Hesham Almatary <Hesham.Almatary@nicta.com.au>

SELFOUR-446 Benchmark: Track syscall feature

Benchmark feature that currently:
- Keeps track of system calls info
- Start time
- Duration
- Capability type
- Invocation tag
- Log the number of invocations of each system call*
- Log the number of invocations for each capability type per syscall.
- Has 3 new syscalls (dump, reset, get size).
- This new feature uses the existing log buffer (which is 1MiB for x86
and ARM). Since the number of syscall invocations is not
deterministic, the logged number of invocations is limited by the size
of the buffer. I suggested to enable the users to pass their own
user-level buffer, to enable more flexibility, later.
- ENABLE_BENCHMARKS is now a parent config option of trace points and
system call track features, they can't be used at the same time.


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


# 289bf92b 05-Jan-2016 Anna Lyons <Anna.Lyons@nicta.com.au>

SELFOUR-114: remove bootinfo.h duplication


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

x86: Refactor vspace code to have verification friendly invocations


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

x86: More portable user mode IO port restriction

For x86-64, to disable IO instructions in user mode requires a
IO permission map being set up properly in TSS. Setting the
IO map base field of TSS larger than the TSS works for 32-bit, but
not 64-bit. This commit sets up a IO permission map usable for both
32-bit and 64-bit kernel and changes the TSS to use the mapping.
The IO permission bitmap is appened to the bitfield generated tss_t,
resulting the tss_io_t structure.


# d20ca20a 13-Jan-2016 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Rename ia32->x86

This is a stylistic commit to make names of variables/constants and
functions in the kernel more consistent. That is, things that are
not IA32 specific, but are generic x86, get renamed to having an
x86 name


# cfcaf49c 31-Jan-2016 Adrian Danis <Adrian.Danis@nicta.com.au>

SELFOUR-399: object sizes and globals frame addr should come from the same source


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

x86: FS/GS base MSRs

when FS/GS_BASE_MSR are used to set the base addreses,
user applications should not touch FS/GS regiters; so
the kernel should load proper selectors once, establishing
limits and other attributes for the segments.


# 9b7a8405 22-Jun-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

Change bootinfo to have generic slot region for paging structures

Current bootinfo defines two slot regions for paging structures,
one for page directories and one for page tables. This does not
easily generalise for N levels of paging structures. This change
uses a single region that has a known order of objects for however
many levels exist


# 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


# 2f3b3e75 03-Jul-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Do not map one of kernel page tables with user access


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

trivial: style


# 2271185e 20-Dec-2015 Adrian Danis <Adrian.Danis@nicta.com.au>

x86: Add missing include


# 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