- for arm generic timer platforms, we remove resetTimer ->
resetGenericTimer indirection and simply include generic_timer.h
- this reduces boiler plate for platforms that share timer drivers, as
they simply include the one header
- there is far more timer code in the RT kernel, which motivates this
change
This prepares for inlinining the generic timer in header files, which will reduce the
redundancy for all platforms that use it.
Since mct.c shared code with the generic timer, both could not define a
resetTimer function. This commit splits the logic and definitions used
by exynos4 and exynos4* into common definitions in mct.h, with the
unique code for both in hardware.c
Instead of switching to the thread contained in `ksSchedulerAction` on a `schedule` we
instead decide between the 'candidate' contained in `ksSchedulerAction`, the current thread
or potentially neither if the candidate is deemed invalid and the current thread is blocked.
A consequence of this change is that it is no longer meaningful to have a distinction between
`switchIfRequiredTo` and `attemptSwitchTo`. Now both these cases simply identify a candidate,
which may or may not be picked in `schedule`. Part of the distinction of `switchIfRequiredTo`
was to not avoid switching if possible when performing notifications. This is now handled by
prefering the current thread over the candidate if the current thread has not blocked.
This change is largely semantic preserving overall, with the exception of non-blocking
synchronous sends now acting like notifications and also preferring to resume running the
current thread.
The motivation for this change was to make it much easier for verification to show
correspondence between the fastpath changes introduced in the previous commit and the
slowpath scheduler.
This corrects the calculation of the L2 bitmap size to correctly handle cases where the
requested num priorities is not a clean multiple of the wordBits
This commit generalises 32 and 64 bit configuration for arm: 32bit uses
coprocessor access through mrc/mcr, 64bit system configuration through
msr,mrs
- SYSTEM_READ|WRITE_WORD: read or write configuration word
- SYSTEM_READ|WRITE_64 : read or write 64bits of configuration
`Arch_checkIRQ` already prints an error message in the case of x86. Printing the additional
error message is both unnecessary, confusing as the message makes no sense on x86. As the
error does make sense on ARM this commit moves the message to the arm `Arch_checkIRQ`
The CParser can't deduce modifies rules for functions without
definitions (like in8, out8 et al and interrupt handler functions).
This adds explicit modifies rules for these functions.
This provides a more robust and efficient implementation that only forces memory reloads
at explicit known points, instead of the over approximation of every time they are
accessed that is forced by volatile.
Adds a named constant of the IPC buffer size bits that can be used when checking the
size/alignment of an IPC buffer. This constant has a compile time assertion to ensure
it corresponds to the actual IPC buffer
This unifies the badge size of endpoints and notifications on 64-bit platforms to a
consistent 64-bits, and also changes the libsel4 definitions to match for both.
The maximum guard size was unnecessarily restricted to 18 bits as it is on 32-bit
platforms. This change increases it to the current maximum possible of 58 bits.
The 58-bit limitation exists due to the need to encode a guard+guardsize into a
single word for cnode invocations.
This data structure is meant to be the user visible format of the data for a cnode_cap,
yet it is defined in a kernel only bitfield file. Moving it to libsel4 opens up the
possibility of consolidating the definitions in libsel4
Zombie caps perform bit packing that relied on the log2(wordBits), which was being
hard coded to 5. Whilst 5 is the correct value on 32-bit platforms, it is incorrect
on 64-bit ones. This changes the previously hardcoded 5 to be the, already existing,
wordRadix definition.
This clock value isn't set consistently on some platforms due to software
rounding, so halting here tends to happen a lot. Instead print a warning
and continue on.
For example using a default Xilinx platform with a 33.333... MHz oscialltor
and a default bootloader the clock value will be somewhere in the range
99999000-100000000, which for most practical purposes is the same thing.
Since this register is written by software and doesn't have the precision to
fully represent common hardware oscillator frequencies, this check seems overly
strict anyway.
makeUserPDEPageTableInvalid and makeUserPDELargePageInvalid were both just creating the same
kind of thing, an invalid mapping, which really should be thought of as the third type of
PDE entry type.
Zero sized arrays are not a C standard extension supported by the C parser. This changes
to the older C90 style for variable length arrays of declaring an array of length 1, as
the C parser also does not suppor the C99 flexible array members.
Declares to a bootloader that we hare multiboot2 compliant and provides an additional
try_boot_sys_mbi2 function for processing a multiboot2 information header.
This abstracts the existing try_boot_sys into two portions, one which pulls data out
of a multiboot1 style information header, and one which performs generic booting
without being multiboot1 specific.
This creates a similar structure as ARM, where an `enum` is created with the `#define` values
from libsel4. Having these values as enum types provides a 'real' C symbol for verification.
RSDP validation was previously done directly in acpi_init. This splits the validation
into a seperate, publicly useable, function. The intention is for this to be used in
boot scenarios where an RSDP is given and does not need to be searched for.
The full RSDP is useful beyond just extracting the RSDT address out of it. In particular
this prepares us for being able to pass a copy of the RSDP to the rootserver.
The previous function signature might lead a user to believe that they were getting a
pointer to a useable acpi_rsdt_t structure. This was in fact not the case and was
actually returning the physical address, that may or may not be mapped in, of the rsdt
table. All of the other acpi *_scan functions would therefore immediately map in the physical
rsdt pointer they were given.
This commit changes acpi_init to return a boolean indicating whether it found a valid
rsdp, and then fills in a copy of the rsdp data. The copy is necessary as the rsdp
data may be at a temporary mapping.
As a result of changing acpi_init the boot code and state is changed to have a acpi_rsdt_t
instance that can be filled out.
This was previously a word_t type, presumably because when the function was originally
written irq_t was a word_t on the platform, this is a mistake and it is more correctly
an irq_t
Verification will guarantee that all usages of the parent cap_get* functions will
be correct and that this case does not happen. However, it is difficult to prove
that the `fail` cannot happen in isolation, and is ultimately not neccessary.
