KernelAArch64SErrorIgnore needs to be saved into the cache in
seL4Config.cmake if it is set by any platform's config.cmake.
Signed-off-by: Kent McLeod <kent@kry10.com>
By default any SError interrupt will halt the kernel. SErrors
may be caused by e.g. writes to read-only device registers or
uncorrectable ECC errors.
When this option is enabled SErrors will be ignored.
Enable this option for the TX2 platform.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Don't create CONFIG_ARCH_AARCH32 on every platform and architecture.
Remove KernelSel4ArmHypAarch32.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
Add support the i.MX low-power UART. This is available on
chipsets such as i.MX8QXP.
Note: This is a preliminary patch in advance of providing
full support for the i.MX8QXP platform.
Note: getchar is not implemented (current) for this platform.
Signed-off-by: Ben Leslie <benno@brkawy.com>
On ARM platforms the code assumes the top phys addr is
exclusive, not inclusive (as is the case on other platforms).
While it would be good to make this consistent across platforms
that is a more invasive change. This simple fix makes the
confir correct for ARM. A more comprehensive consistency fix
can be applied at a later time.
Signed-off-by: Ben Leslie <benno@brkawy.com>
This is to work around an issue in a variant of syslinux that treats a
PHDR segment as distinct from a PT_LOAD segment and rejects an ELF if
the two segments are overlapping.
Signed-off-by: Kent McLeod <kent@kry10.com>
A previous update added a disjunct to an `if` condition outside the
existing `unlikely` branch hint. This commit extends the hint to the
full `if` condition.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Like SCTLR, CNTV_CTL is switched to/from hardware when we enable/disable
the VCPU, so it must be read from a saved VCPU context when that VCPU
isn't active.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Although the functions aren't implemented properly, this is a stop gap
issue to prevent the linker from raising problems about missing
references to various platform-specific capDL printing functions.
Signed-off-by: Damon Lee <Damon.Lee@data61.csiro.au>
An aditional parameter for the dtb was added to the init_kernel
function call in the elfloader. The corresponding _start entry
in the kernel was never updated.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
The scheduler cannot correctly schedule once the timestamp exceeds
MAX_RELEASE_TIME as releases beyond this point may be subject to
overflow. For most systems this should still allow a great many years if
the timestamp starts from 0 at system boot.
Some systems currently start with a random initial timestamp and my
begin with a timestamp that prvents correct budgeting. This assert helps
to catch cases where scheduling becomes invalid due to the timestamp
exceeding the give bound.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The implementation currently never produces a case where the head might
overlap any subsequent refill as it now always effectively prepends when
merging refills at the head rather than appending.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The proofs currently only guarantee that the system scheduler is correct
while the current time is less than INT64_MAX - 3 * MAX_PERIOD ticks.
With the MAX_PERIOD configured to almost INT64_MAX, this would imply
that the system scheduler is never correct.
To ensure that we get a large duration where the system is correct, we
take 1/8th of the TOTAL representable time as the MAX_PERIOD, ensuring
that 3 * MAX_PERIOD is still less than half of all representable time.
For a system with a 1MHz scheduling clock, this produces a valid
execution time on the order of 2^19 years.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This re-introduces the overrun handling but bounds charging of budget
such that we never calculate a refill with a start using an integer
overflow.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
A refill can still be charged if the refill list is full. This means
that we only require sufficient capacity to continue a timeslice.
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
When a task is preempted the head refill is partially charged. When it
is later resumed and again charged, the new charge will be added to the
refill created before the preemption resulting in only a single new
refill being created for each activation.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
We guarantee that all refills in an SC are disjoint.
We don't care about ordering or disjointness for round-robin SCs.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This replaces the refill_split_check and refill_budget_check with a
single function that chanrges the provided usage to an SC and updates
the refills.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
We only need to guarantee that the head refill is MIN_BUDGET so we allow
refills of any size.
We still merge overlapping refills and delay tail refills if there are
no more refills available.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Remove the UART handling details from the top level I/O handling that
implements printf(). The architecture's I/O handling must define how
the debug channel is implemented and what special handling is
required. This allows separating UART and SBI debug output handling.
Signed-off-by: Axel Heider <axelheider@gmx.de>
It seems no kernel code uses the padding feature in the printf() format
string, so this NULL pointer dereferencing case has never been observed
anywhere practically. Furthermore, this code is not part of the formal
verification, so this step also could not catch this.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Replace capDL() by a generic debug_capDL() where all architectures are
supposed to provide an implementation or print an error.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Go through the ELF file to look for large sections that are filled with
zeros and fixup any definitions to minimize them.
Also write more of the pc99 linker script to maintain alignments between
file offsets and address mappings.
Signed-off-by: Kent McLeod <kent@kry10.com>
Fix issues where scheduling context is dereferenced after it is removed
from the associated TCB.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
While the new check is technically redundant, it is consistent with how
schedContext_completeYieldTo is called elsewhere and eases verification.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
