Implementation of batch vspace operations #6
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add a `--form_file <file>` option to the bitfield generator for printing a `/* generated from <file> */` message in a comment. Use this option in cmake to provide the original source .bf file before preprocessing so it's easier to find out where the corresponding definitions are. Signed-off-by: Gerwin Klein <[email protected]>
Mention that it can be Ok for regions to overflow. State explicitly that the end is exclusive. Signed-off-by: Gerwin Klein <[email protected]>
Document in `create_untypeds_for_region` what makes region overflow for device untypeds work. Signed-off-by: Gerwin Klein <[email protected]>
Add compile time checks for conditions on physBase that are necessary
for verification of multikernel builds to succeed -- if these fail, the
proofs will fail.
If these succeed, and nothing else has changed compared to a verified
kernel other than physBase, then the proofs will succeed. This does not
mean that all platform requirements are validated, it just means that
all requirements for the proofs to be consistent are met.
The conditions correspond to those in
spec/machine/*/Arch_Kernel_Config_Lemmas.thy
in the verification repository.
Signed-off-by: Gerwin Klein <[email protected]>
* boot: sanity checks for provide_untyped_cap Check arguments for alignment, size, and kernel window (if not device untyped). This provides sanity checks in case any of the memory region computations are wrong. Since this code is not performance critical and can return failure, these are not assertions, but normal conditions with user feedback. I.e. they are on in release and verified configurations. Signed-off-by: Gerwin Klein <[email protected]>
GICD_IROUTERn is at the offset 0x6100 for SPI 32. SGIs and PPIs do not have a target since they are private to CPUs. Signed-off-by: JorgeMVP <[email protected]>
Signed-off-by: Axel Heider <[email protected]>
These are the prefixes used by the official Arm GNU Toolchain [1] It would be convenient if seL4 would recognise it out of the box. [1] https://developer.arm.com/downloads/-/arm-gnu-toolchain-downloads Signed-off-by: Mathieu Mirmont <[email protected]>
- "When an address translation instruction is executed, explicit synchronization is required to guarantee the result is visible to subsequent direct reads of PAR_EL1." Signed-off-by: JorgeMVP <[email protected]>
- dmb() no longer works for GICv3, and consequently a stronger barrier like dsb() has to be used. A weaker variant of dsb is used to ensure the observability of complete stores in the same inner-shareable domain. Signed-off-by: JorgeMVP <[email protected]>
Signed-off-by: Axel Heider <[email protected]>
Improve the documentation to describe about the potential pitfall in SMP boot and the non-recommended barrier that is used. Signed-off-by: Axel Heider <[email protected]>
The cache maintenance is needed on AARCH32, so check explicitly for this architecture instead of doing this everywhere except AARCH64. Signed-off-by: Axel Heider <[email protected]>
Signed-off-by: Axel Heider <[email protected]>
Include sel4/config.h instead of autoconf.h in the generated code. Signed-off-by: Axel Heider <[email protected]>
Make sel4/config.h the only file to eventually include autoconf.h Signed-off-by: Axel Heider <[email protected]>
Including the configuration first ensure consistent behavior. Signed-off-by: Axel Heider <[email protected]>
Signed-off-by: Kent McLeod <[email protected]>
Add a config option, KernelAArch64UserCacheEnable, that enables user level access to DC CVAU, DC CIVAC, DC CVAC, and IC IVAU which are cache maintenance operations for the data caches and instruction caches underlying Normal memory and also access to the read-only cache-type register CTR_EL0 that provides cache type information. The ArmV8-A architecture allows access from EL0 as fast cache maintenance operations improves DMA performance in user-level device drivers. These instructions are a subset of the available cache maintenance instructions as they can only address lines by virtual address (VA). They also require that the VA provided referrs to a valid mapping with at least read permissions. This corresponds to lines that the EL0 could already affect via regular operation and so it's not expected to break any cache-partitioning scheme. The config option allows this policy to be selected for a particular kernel configuration, but it is default enabled as this has been the existing behavior for current aarch64,hyp configurations and have not been explicitly disabled in non-hyp configurations. Signed-off-by: Kent McLeod <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Add a user manual for the bitfield generator that documents syntax, semantics and basic concepts. Should also be able to serve as main spec for what the tool is supposed to do. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
- CNTFRQ is a constant value, and does not work for this case, while CNT_CT is the one that should be used as 64-bit physical counter. Signed-off-by: JorgeMVP <[email protected]>
The `--multifile_base` option is unused in the seL4 build and has comments indicating that it is broken. Signed-off-by: Gerwin Klein <[email protected]>
* Add help texts for all CLI options. * Point to the manual in file header. * Remove obsolete `--multifile_base` and `--c_defs` options. The former is unused and the logic for it was removed in the previous commit. The latter is not referenced in the code and has no effect. ` * Remove unused `mode` variable. Signed-off-by: Gerwin Klein <[email protected]>
* describe CLI * describe pruning * mention where in seL4 generated code and source are Signed-off-by: Gerwin Klein <[email protected]>
The verified configs have a typo in the name of the KernelMaxNumBootinfoUntypedCaps setting, which is then ignored by the build system and the default is used if not otherwise set. Remove the instances that have been ignored so far and replace with the default value if they are not otherwise set. This means there is no actual config change. Signed-off-by: Gerwin Klein <[email protected]>
- In non-secure world, group 1 IRQs are used instead of group 0. Signed-off-by: JorgeMVP <[email protected]>
Avoid redundancy. Signed-off-by: Axel Heider <[email protected]>
Signed-off-by: Ivan-Velickovic <[email protected]>
Prefer compile_assert over _Static_assert. The latter is only available in C11, and the verification demands C99. Signed-off-by: Gerwin Klein <[email protected]>
__builtin_offsetof is not part of the verification C subset -- avoid accidental use by not declaring a macro for it and filter out the single use by explicitly marking it as invisible to verification. Signed-off-by: Gerwin Klein <[email protected]>
There are multiple variants of the RPi4B SBC with different sizes of RAM. There exists 1GB, 2GB, 4GB, and 8GB models. This patch adds the `RPI4_MEMORY` CMake configuration option in order to be able to specify the RAM size when building the kernel. Based on the RAM size provided, an appropriate device tree overlay is selected. The default memory size of 8GB remains the same as to not introduce breaking changes. Signed-off-by: Ivan-Velickovic <[email protected]>
Signed-off-by: Ivan-Velickovic <[email protected]>
Make FPU possible for "ARM" verification targets. Signed-off-by: Rafal Kolanski <[email protected]>
Turn FPU off by default for the verification builds we have so far. Only the imx8mm branch currently supports FPU for AArch32. Signed-off-by: Gerwin Klein <[email protected]>
Use `ARM_verified.cmake` from branch imx8-fpu-ver as `ARM_imx8mm_verified.cmake` on master, so both can be used by verification CI without switching branches. Signed-off-by: Gerwin Klein <[email protected]>
Use `ARM_HYP_verified.cmake` from branch exynos5-ver as `ARM_HYP_exynos5_verified.cmake` on master, so both can be used by verification CI without switching branches. Signed-off-by: Gerwin Klein <[email protected]>
The verification C parser is failing to translate this function, but it does not actually need to since this is behind the machine interface anyway. Mark the function as dont-translate to avoid the problem. Signed-off-by: Gerwin Klein <[email protected]>
CCDC-GVSC DISTRIBUTION A. Approved for public release; distribution unlimited. OPSEC#4481. Signed-off-by: Gerwin Klein <[email protected]>
This commit combines a number of smaller commits which do the following:
* Enter IA-32e mode when running a 64-bit host
* Handle additional general purpose registers in 64-bit mode
* Handle 64-bit specific MSR events
* Properly save and restore FS, GS, and Shadow GS registers
CCDC-GVSC DISTRIBUTION A. Approved for public release; distribution
unlimited. OPSEC#4481.
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Chris Guikema <[email protected]>
Guard the new implementation of 64-bit x86 guests behind a config option. This is done so that existing projects that use x86_64 hosts with ia32-bit guests can continue to be supported until either the old feature is preferred to be deprecated, or support can be added to support both simmultaneously. Signed-off-by: Kent McLeod <[email protected]>
Removes duplication of the vmlaunch/vmresume code. Signed-off-by: Jingyao Zhou <[email protected]>
Co-authored-by: Ivan-Velickovic <[email protected]> Signed-off-by: Axel Heider <[email protected]>
Signed-off-by: Ivan-Velickovic <[email protected]>
These are only called when CONFIG_DEBUG_BUILD is on, which *usually* means that CONIFG_PRINTING is also enabled, but, it's not necessarily the case. Signed-off-by: Ivan-Velickovic <[email protected]>
Without this patch, user-level programs have the ability to map in the core-local interrupt controller on RISC-V platforms which contains the memory-mapped registers for the core-local timer the kernel uses. This is a level of privilege that user-level programs should not have. Writing to the `mtime` register is possible which can then affect the timer interrupts are delivered to the kernel. Signed-off-by: Ivan-Velickovic <[email protected]>
Signed-off-by: Axel Heider <[email protected]>
Commit f4c41f3 removed a check that dereferenced tcbSchedContext. It should have removed this assert() also then. Signed-off-by: Axel Heider <[email protected]>
It does the same on all architectures, so the contents can be moved into the generic code. Signed-off-by: Axel Heider <[email protected]>
seL4#1065 introduces a compilation error from refactoring. Also apply some missed feedback from seL4#1065 Signed-off-by: Kent McLeod <[email protected]>
Signed-off-by: Alwin Joshy <[email protected]>
Signed-off-by: Alwin Joshy <[email protected]>
Signed-off-by: Alwin Joshy <[email protected]>
alwin-joshy
force-pushed
the
batch_vspace
branch
from
0cbfce6
to
6a7e26c
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This pull request includes prototype implementations of the vspace_[remap|unmap]_range operations for the NCSC March 2023 deliverable. Currently demonstrates around 4x the performance of single page operations over moderately large regions in microbenchmarks.
Possible improvements include: