The UL_CONST macro provides a way to declare a constant that may or may not have a UL
suffix. In the case of assembly the UL suffix will be an error to many assemblers and
is not needed.
This defines a CURRENT_CPU_INDEX() macro that resolves to a constant 0 in the absence of
SMP, or a call to getCurrentCPUIndex in the presence of SMP. This provides a way to use
per-core data structures, without additional guards, in a way that is nearly invisible
to verification
Restricting virtual addresses to essentially be only addresses without bit 47 set
allows us to not need to check that an address passed in by the user is canonical
or not. Any address that is in danger of not being canonical (has bit 47 set but
not bits 48 to 63) will all by higher than USER_TOP and will not be permitted.
In f6d367e8df virtual addresses were changed from 48
bits to 49 bits, but this does not seem necessary and the commit does not have enough
detail to justify the change. As such it is being changed back to 48 bits in this
commit, which is far less confusing and results on the bitfield generated functions
switching on bit 47 to determine sign extension (instead of bit 48), which matches
what the hardware description says should be done.
- 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.
