- tweak SMP/multikernel text to make clear that SMP is not deprecated
- rephrase old VSpace reuse section hopefully be clearer
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- MCS WCET settings are just defaults without much basis
- stale page cap data also allows cache ops to proceed
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Frame caps should be checked for stale mapping info before authorising
any operation on them. In this particular case, the mapping may have
become invalid.
See also #1281
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When performing data cache invalidate by virtual address, the mapping
must have write permissions, otherwise a fault will be generated by the
hardware. Therefore, when the kernel performs this operation during
cache maintenance invocations it must first check that the mapping has
write rights in the decode phase of the operation.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit's parent renames the interface XML files.
The symlinks added in this commit serve to ease the transition to the
new names for downstream projects.
These links are added:
- include/interfaces/{sel4.xml -> object-api.xml}
- arch_include/*/interfaces/{sel4arch.xml -> object-api-arch.xml}
- sel4_arch_include/*/interfaces/{
sel4arch.xml -> object-api-sel4-arch.xml
}
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The ELF loader may well be satisfied with a smaller alignment, but the
compile time assert in the kernel requires super section alignment for
physBase.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The page no longer exists on the doc site, and the site does not
actually have more info, because the change log is generated from here.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Improve markdown compliance to make sure the change log gets rendered
correctly on website and GitHub.
- use markdown headings for old releases
- make headings markdown-spec consistent so that editors can fold
sections/releases
- use:
- level-2 heading for release version
- level-3 heading for main changes/upgrade notes etc
(= one level down from before)
- increase levels of rest accordingly
- consistent list indent (unbreaks rendering)
- use markdown <URLs> over bare URLs
- no content changes apart from one typo
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This reorders the guard in one of the if statements in preemptionPoint
to first check isIRQPending, since it is the most likely cause of this
guard being true. This also eases verification.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
When KernelArmDisableWFIWFETraps is disabled (trapping of WFI/WFE is
enabled), the kernel traps WFx instructions from both native and vCPU
threads. This change makes the code in line with the config description.
In any case, there don't exist many use cases for trapping WFx from
native threads vs vCPU threads. Example: kvm uses this to yield physical
CPU time to other vCPUs instead of busy waiting.
Signed-off-by: Andy Bui <andy.bui2001@gmail.com>
This eases verification by having only one call to refill_head
within refill_head_overlapping, and by giving a name to the body
of the loop within refill_unblock_check.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
lockTLBEntry uses the global tlbLockCount as input without checking
bounds. This is fine, because the function is called at most 2 times per
core, but this is only apparent when checking the entire possible
calling context.
Make this bound obvious locally by doing nothing if the function is
called with values of tlbLockCount of 2 or greater. This is safe,
because TLB lockdown is a performance change only. Also add an assert
for debug mode, becase we want to know if calling context ever changes.
This potential issue was reported by The UK's National Cyber Security
Centre (NCSC).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The code previously used the same instructions for Cortex A8 and A9,
but the Cortex A8 instructions are undocumented for A9, and A9 provides
a slightly different TLB interface.
As far as we can tell, the instructions were simply ignored by the
supported A8 platforms, so there was no current correctness issue.
Since the instructions had no effect, this commit removes A9 TLB
lockdown support.
This potential issue was discovered and reported by the UK's National
Cyber Security Centre (NCSC).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This configuration option requires access to the CLINT in S-mode
which is not available on newer versions of OpenSBI. Because of
this, it makes more sense to not turn on this option by default
and instead let it be 'opt-in' for those who want the performance
benefit and also have firmware that does not restrict S-mode access
to the CLINT.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
There is a warning when creating a write-only mapping on
AArch32/AArch64.
This patch simply makes the message consistent across all
architectures since the behaviour when creating a write-only
mapping is also consistent across all architectures.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Correctly mask the IOAPICVER register to the Maximum Redirection Entry
field to potential avoid spurious higher bits on e.g. AMD processors.
Set IOAPIC_IRQ_LINES to the maximum value this field is allowed to
return (239+1). While our haswell machines report 24 IRQ lines as
expected, the skylake machines report 120.
The only impact should be the size of the ioredtbl_state array.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Use the Isabelle version set in the verification manifest instead of
overriding to a specific version here. This will automatically update
as the verification repository updates to new Isabelle versions.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This new platform is NXP Semiconductor's Evaluation Kit for the i.MX 8M
Plus Applications Processor. It's from the i.MX 8M family of processors
and is largely similar to the existing i.MX 8M Quad and i.MX 8M Mini
platforms.
Signed-off-by: Damon Lee <damon@kry10.com>
IOAPICS can have varying numbers of lines attached. The actual number
can be accessed in the top 16 bits of the version register.
Rather than assuming fixed 24 lines per IRQ, read the actual number and
use that. We still bound that value by 24 and abort initialization if
the bound is not met. As all current IOAPICS have at most 24 IRQ lines,
this will not trigger on current hardware.
Signed-off-by: Peter Chubb <peter.chubb@unsw.edu.au>
Replace "\<"" in strings with "\\<". Until recently python did not
complain about this illegal escape sequence, but now it warns.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
