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