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>
This introduces library functions for updating the linked lists which
use the tcbSchedNext and tcbSchedPrev pointers of a TCB, and uses these
to perform the updates to the ready queues and the release queue.
In order to accommodate this, ksReleaseQueue is now of type tcb_queue_t.
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Python2 is no longer supported and hence the dependency
on six is no longer necessary.
According to https://six.readthedocs.io/#six.string_types,
six.string_types is just str in Python3.
According to https://six.readthedocs.io/#six.next in Python2.6
and above, six.next is just next.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Depedencies on Python2/3 cross support (such as six, past and future)
are removed as only Python3 is supported at this point. Fewer
external deps is a good thing.
Signed-off-by: Ben Leslie <benno@brkawy.com>
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
The prior behavior would emit ANSI escape codes which set the terminal
foreground color to black bold (`[30;1m`), leaving the default
background color. On many terminals configured with a dark color scheme,
this creates black on black characters, i.e. the output is invisible.
This change moves to a better adapted output, where the output is only
marked as bold (`[1m]`), which works well on all color schemes.
Fixes#1243
Signed-off-by: wucke13 <wucke13@gmail.com>
Check for CONFIG_ENABLE_SMP_SUPPORT instead of checking for the
number in CONFIG_MAX_NUM_NODES. This allows enabling SMP support
with just one node also.
Signed-off-by: Axel Heider <axel.heider@codasip.com>
- fix: brackets in check
- fix: use CONFIG_ENABLE_SMP_SUPPORT
- conditions for CONFIG_MAX_NUM_NODES have been removed
Signed-off-by: Axel Heider <axel.heider@codasip.com>
This should not have been added in commit ad4ea6cd. And since
commit c642a398 this is handled by a python script anyway.
Signed-off-by: Axel Heider <axel.heider@codasip.com>
Replaced deprecated macros in statedata.c to get the page table index,
and replaced function in vspace.c to create a new page
table entry for
aarch64/
Signed-off-by: Krishnan Winter <krishnanwinter1@gmail.com>
The check was not enforcing the minimum radix intended by 5fac9e8 and
still allowed a radix of 4 to be specified.
Signed-off-by: Craig McLaughlin <thecraigmclaughlin@gmail.com>
Previously accessing the ccnt_num_overflows
value using the NODE_STATE macro. In SMP
configurations, this looks for this value
in the system node state, however, it
resides in the cpu arch node state. This should
therefore be accessed using the ARCH_NODE_STATE.
Signed-off-by: Krishnan Winter <krishnanwinter1@gmail.com>
Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
