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 <gerwin.klein@proofcraft.systems>
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 <gerwin.klein@proofcraft.systems>
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 <i.velickovic@unsw.edu.au>
__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 <gerwin.klein@proofcraft.systems>
Prefer compile_assert over _Static_assert. The latter is only available
in C11, and the verification demands C99.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Enable the timer only at initialization and since it is always
enabled. It is not needed to be re-enabled.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
Generic Timer IRQs are level-sensitive, when the CNT_TVAL
is updated the trigger condition is de-asserted and the
change is propagated to the GIC in a finite time to clear
the pending state.
However, we have to make sure the timer deasserts before
EOIR/DIR, otherwise the interrupt happens again. Therefore,
we need an isb() to cause the timer to de-assert before EOIR/DIR.
There is also a chance of spurious IRQ. A spurious IRQ can be
generated, in the case we have a level-sensitive IRQ, and its
pending state is cleared at device-level but not yet propagated
to the GIC. In between the IRQ deactivation and IRQ ack of the
new interrupt if the requested change from the timer gets propagated
then it causes a spurious IRQ.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
In the interest of stability and not breaking
things, the value of VMReadOnly remains the same.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
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 <gerwin.klein@proofcraft.systems>
* 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 <gerwin.klein@proofcraft.systems>
The `--multifile_base` option is unused in the seL4 build and has
comments indicating that it is broken.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- 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 <jorgepereira89@gmail.com>
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 <gerwin.klein@proofcraft.systems>
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 <kent@kry10.com>
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 <axel.heider@hensoldt.net>
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 <axel.heider@hensoldt.net>
- 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 <jorgepereira89@gmail.com>
- "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 <jorgepereira89@gmail.com>
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 <jorgepereira89@gmail.com>
* 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 <gerwin.klein@proofcraft.systems>
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 <gerwin.klein@proofcraft.systems>
Document in `create_untypeds_for_region` what makes region overflow for
device untypeds work.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Mention that it can be Ok for regions to overflow. State explicitly
that the end is exclusive.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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 <gerwin.klein@proofcraft.systems>
Using the same cap twice on the same slot is possible for remapping,
but using the same cap twice in different tables or VSpaces will result
in an error.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Describe the difference in 3 and 4 level configs for AArch64 and point
to the libsel4 macros that abstract from the distinction.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove previous mix of \texttt and \obj, use \obj consistently when
referring to kernel objects.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- clarify terminology (cap vs object) in ASID Control and ASID pool
- same for page sharing
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Adjusting for VSpace object clarification and making sure terminology
is used consistently.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Rework the intro to the VSpace section for slightly improved clarity
and a more explicit definition of the distinctions between VSpace and
VSpace object, and between frame object and page capability.
Addresses #564
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This header file is shared by kernel and userland. We can control the
kernel compiler setting, but userland might use an arbitrary setup.
Put a safeguard in place that things works as expected.
Signed-off-by: Axel Heider <axelheider@gmx.de>
