The thread context structure layout is explicitly designed to have the
register context first, as this simplifies saving the user context on
entry in assembly code. On the exit path there is no need to hard-code
this assumption, stick to the semantics and leave details to the
compiler.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
The signal fastpath aims to optimize the
seL4_Signal operation. In this commit, it is
implemented for MCS AARCH64 (SMP and non-SMP).
The fastpath does not include the case where
signaling results in a higher priority thread
being unblocked and made available for
scheduling (on any core). It does not
fastpath the case where the signaled thread
is donated a scheduling context and has its
FPU state saved in the FPU of a core.
Co-authored-by: Shane Kadish <shane.kadish@csiro.au>
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Remove the return value from configure_sched_context(), because it never
fails. As a consequence, create_idle_thread() also never fails and does
not need a return value.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
Because ksCurTime is compared cross-node now, time across
nodes must be the same. Check this once during boot.
Replace __atomic_signal_fence with the more correct
__atomic_thread_fence, as ksNumCPUs will be changed
cross-node.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Remove the now unused core argument from refill_new and replace all
REFILL_NEW calls with direct calls.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
The code using ksCurTime assumes that ksCurTime is up-to-date,
but this assumption is wrong for ksCurTime of other CPU cores.
Those can be quite some time in the past.
The implications of using NODE_STATE(ksCurTime) is that clocks
on all cores must be synchronous:
- Riscv is okay: The specification states: "The real-time clocks
of all hardware threads in a single user application should be
synchronized to within one tick of the real-time clock."
- x86 okay if not ancient when Invariant TSC is supported.
- aarch64 is okay.
- arm32: arm_global.h is okay. Exynos timer seems okay. am335x and
omap3430 are single-core.
See also #854.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Use the thread passed as parameter instead of making assumption that
this is in sync with the global state.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
- explicitly mention the parameter to make macro less obscure.
- add brackets to make the expression an atom.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
The pointer to a reply object, if any, can be accessed
via the replyObject in the thread state
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
At least some server-class Skylake processors use 0x55 as
their model ID.
These are Skylake X processors.
Signed-off-by: Peter Chubb <peter.chubb@unsw.edu.au>
The kernel expects object sizes to be powers of two for size and
alignment computations.
- add missing padding for MCS 64-bit configurations for notifications
(other configs were already fine)
- add missing padding for reply object struct
- strengthen compile time assertion to catch discrepancies in the
future.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The messageinfo register is set to 0 after processing a kernel object
invocation if the invocation set the thread state to restart. This is a
problem if the kernel object invocation had also set the message info
register.
The existing convention in this case is for the kernel invocation to
set the thread state to running right before it returns to avoid the
problematic code path. However, there are some invocations that do not
follow this convention and their message info register gets clobbered.
There are also some invocations that set message registers without
setting the message info register at all, or that do not guard their
message register updates with a call parameter.
This commit fixes these issues modulo setConsumed, which we defer to a
later point.
Co-authored-by: Jimmy Brush <code@jimmah.com>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
For a VM fault in a hypervisor context, 32-bit Arm translated the IP
address into an IPA, while 64-bit Arm did not. The previous commit
made these consistent by performing the translation on both.
After investigation and discussion, the 32-bit Arm behaviour was
declared a bug: reporting an IPA (instead of a VA) to the VMM is not
very useful and can cause issues when the fault message is not sent
immediately (SELFOUR-1602). This commit, therefore, removes all stage 1
translation from Arch_setMRs_fault on Arm platforms.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit introduces `addressTranslateS1` to be used on Arm platforms
with hypervisor enabled for stage 1 (vaddr to IPA) translation. On
AArch32 this is a rename from `addressTranslateS1CPR`, and on AArch64 it
wraps `ats1e1r`. This changes the ABI on AArch64 to report faulting
address as IPA.
Reasoning:
With hypervisor enabled, AArch64 defined `addressTranslateS1CPR` to do
nothing, while AArch32 defined it to do stage 1 translation. This
delivered VM faults to the user with the faulting address being either
an IPA or a vaddr depending on mode. This inconsistency is undesireable.
This commit proposes adjusting the inconsistency to match AArch32
behaviour, as it is one of the verified platforms.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For ARM currently TIMER_PRECISION exists, but that is in microseconds
and not fine-grained enough.
This is needed to make periodic tasks synchronous with the system clock.
If this value is zero every period will be extended with the overhead of
taking an interrupt and reading the system clock. To avoid this drift,
the configured value should be set to at least the average overhead.
See also issue #844.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
sysexit requires a 64-bit operand to remain in 64-bit mode when
switching to user level. gcc versions older than 12 encode this as
"REX.W SYSEXIT" while clang encodes this as "SYSEXITQ". Both compilers
don't support the alternate encoding. We instead use ".byte
0x48,0x0F,0x35" which is the actual opcode of the required instruction
which will work with both compilers.
Signed-off-by: Kent McLeod <kent@kry10.com>
seL4_UserTop must be defined to be > 0xC0000000 when the kernel is in
hyp mode due to assumptions made by the kernel init code.
Signed-off-by: Kent McLeod <kent@kry10.com>
Accessing the hyp mode SPSR register via the banked instruction syntax
is UNPREDICTABLE if hyp is the current mode. The direct syntax needs to
be used instead. This is documented in the ARMv7 Architecture reference
manual.
Signed-off-by: Kent McLeod <kent@kry10.com>
CPSR.AIF already presented in HCR_COMMON macro,
And HCR_NATIVE includes HCR_COMMON, then no need
To set CPSR.AIF bit again
Signed-off-by: Cao Jianlong <caojianlong@outlook.com>
The latest code updates introduced CONFIG_ENABLE_KERNEL_LOG_BUFFER
meanwhile other code and config.cmake keeps using
CONFIG_KERNEL_LOG_BUFFER
Signed-off-by: Nataliya Korovkina <malus.brandywine@gmail.com>
Now that there is no need to reserve page table entries in each VSpace
object, the full architecture specified address space range is usable.
Signed-off-by: Kent McLeod <kent@kry10.com>
Each vspace object has a count of how many SMMUv2 context banks are
bound to it. This attribute is moved out of a reserved page table entry
slot into the asid_map_t structure.
This also reduces the width of the MappedCB field from 12 to 8 bits
which is large enough to hold the maximum number of CBs allowed by the
SMMUv2 spec (128). This conserves otherwise wasted bits.
Signed-off-by: Kent McLeod <kent@kry10.com>
When switching to the new thread, it's VSpace must have a valid ASID
mapping. This means that the ASID in the vspace cap must resolve to the
same vspace object as the vspace cap does. In addition, when the VSpace
object is for a stage 2 translation there must be a currently assigned
hardware VMID for the vspace. Otherwise the slowpath must be taken.
Once these checks are done, the TTBR registers can be directly updated
without needing to perform another ASID translation.
Signed-off-by: Kent McLeod <kent@kry10.com>
This stores the 8-bit vmid in the ASID map rather than in a
slot of the virtual address space root for hypervisor configurations.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Kent McLeod <kent@kry10.com>
This uses the asid_map bitfield from x86 for aarch64 to map from ASID to
a given address space.
This will allow for alternate mappings from ASIDs in the future as well
as moving small amounts of metadata into the the ASID table itself.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Kent McLeod <kent@kry10.com>
This is not supposed to happen, thus printing the value gives a bit more
insight what might have happened here.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Put the parameter in brackets to ensure it is an atom. This makes the
macro work as expected in corner cases like ARRAY_SIZE(foo + 3) also.
Signed-off-by: Axel Heider <axelheider@gmx.de>
When building seL4 on a host whose default encoding is not UTF-8,
tools/bitfield_gen.py complains, as with the following log from
Python 3.6 on a Ubuntu 18.04 host says:
Traceback (most recent call last):
File "tools/bitfield_gen.py",
line 2773, in <module>
string = f.read()
File "/usr/lib/python3.6/encodings/ascii.py", line 26, in decode
return codecs.ascii_decode(input, self.errors)[0]
UnicodeDecodeError: 'ascii' codec can't decode byte 0xc2 in position
607543: ordinal not in range(128)
As the Python 3 doc for open() [1] says the default encoding is
platform dependent, such build error may happen on some hosts.
We can either updating tools/bitfield_gen.py to call open() with
an explicit encoding="utf-8" parameter, or avoiding UTF-8 characters
in the source codes.
After inspecting the two places in current source tree that use UTF-8
characters, none of them is absolutely necessary. Let's convert them
to ASCII characters.
[1] https://docs.python.org/3.6/library/functions.html#open
Signed-off-by: Bin Meng <bmeng.cn@gmail.com>
In `vcpu_enable` and `vcpu_disable`, use `setHCR` to wrap setting
REG_HCR_EL2 (similar to AArch32).
Reorder `vcpu_enable` to match AArch32 operation order for easier proof.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Since hardware.h is shared with assembler code, it's better to avoid
having C ode in there. This also aligns the RISC-V port with the ARM
port, where machine.h contains the special register wrapper functions.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Factoring out the benchmark syscall handling in dedicated functions
improves code readability and maintainability.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Explicitly include the config header file as the first thing, don't rely
on other headers doing this eventually.
Signed-off-by: Axel Heider <axelheider@gmx.de>
When calling chargeBudget or commitTime, only consume time within the SC
refills if the SC does not belong to the idle thread. This is to make it
easier to prove that the idle thread is always runable, even if it has
just consumed its SC's current timeslice.
Signed-off-by: Kent McLeod <kent@kry10.com>
Defined to be equal to CONFIG_NUM_DOMAINS. seL4 makes control-flow
decisions based on whether the number of domains is greater than 1. To
perform refinement proofs independent of the number of domains, we need
to follow both branches of these if statements, pretending we don't know
which branch will be taken. This is made significantly harder when
preprocessed C code ends up with comparisons like `if (16 > 1)`.
By adding a numDomains that appears in the C code, we obtain a name we
can point to and link up to higher level specifications.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
It seems all Cortex-A7, Cortex-A15, Cortex-A53 boards require to
flush to coherency in order to get it work.
It is a temporary fix, and we will keep track on this issue.
Signed-off-by: Luca (Wei) Chen <wei@cvluca.com>
The getMaxUsToTicks function is supposed to return maximum
amount of time you can pass to usToTicks without overflow,
but in RISC-V implementation it returns ticks instead. This
patch corrects it so it's implementation is akin to those in
other platforms.
Signed-off-by: Marcin Witkowski <mwitkowski@antmicro.com>
Hide the actual SBI call parameter details of the legacy API and remove
the pointer parameters in the higher code layers. This is a preparation
step for switching to the newer SBI API.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Since uint32_t and uint64_t are used, stdint.h needs to be included.
- Improve comments about GCC/LLVM internals.
Co-authored-by: Matthew Brecknell <matthew@brecknell.net>
Signed-off-by: Axel Heider <axelheider@gmx.de>
The memory mapping for the timer only uses 1K on AllwinnerA20, but
the minimum device mapping is 4K in seL4. Other devices within this
4K page (CCU and PIO) cannot be accessed in the userland.
Replace the kernel timer with the ARM generic timer on AllwinnerA20,
and remove the implementation for AllwinnerA20 specific timer in the
kernel. So we should have user access to those devices now.
Signed-off-by: Luca (Wei) Chen <wei@cvluca.com>
32-bit architectures have to share a small 4GiB address space between
privileged and non-privileged modes. Picking the address to split the
address space at affects how much virtual memory userlevel can use, and
how much physical memory the kernel can turn into untypeds. This is
something that should be configurable policy as different divisions make
sense for different applications. For now we only add the config
option to qemu-arm-virt to try it out before potentially adding it to
all 32-bit platforms.
Signed-off-by: Kent McLeod <kent@kry10.com>
The function Arch_finaliseInterrupt() is empty now and can be removed as
it serves no purpose any longer. There has never been a guarantee that
it gets only called due to kernel entry caused by an interrupt. Instead,
getActiveIRQ() is called in various places of the kernel to check if
there is a pending interrupt. There is a guarantee that the generic
kernel code calls ackInterrupt() within the same kernel entry call
path eventually, when it has finished processing this interrupt. Any
architecture or platform specific cleanup can be done there is this is
necessary.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
PC99 is the only platform that uses Arch_finaliseInterrupt() instead of
ackInterrupt(). There seem no reason for this, thus the code is moved
from Arch_finaliseInterrupt() to ackInterrupt() now.
Arch_finaliseInterrupt() is empty now, but still kept, because it is
part of the proofs and provides a hook that might be useful one day.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
On aarch64 in EL2, there aren't any addresses after 2^48 and so the
any kernel device untypeds that have very large physical addresses could
potentially move into an invalid address range when translated to a
Kernel window PPTR address when being stored in a cap slot. The kernel
in EL2 doesn't need to share its address space with user level and so we
can make the kernel window start low enough that we can't get overflows.
We start from the second entry in the top level page table so that we
don't conflict with any setup code running in the lowest 512GiB of
virtual addresses.
Signed-off-by: Kent McLeod <kent@kry10.com>
CONFIG_DEBUG_BUILD and CONFIG_PRINTING are different config options that
can be used independently from each other. CONFIG_PRINTING controls the
backend of kernel print functions while CONFIG_DEBUG_BUILD controls
other kernel debug features.
Note that CONFIG_VERIFICATION_BUILD is the config option that controls
whether any of these options can be used.
Signed-off-by: Kent McLeod <kent@kry10.com>
- KernelGlobalsFrame caused the definition of seL4_GlobalsFrame which
was a reservation at the top of the user address space on ARMv6
platforms.
- KernelDangerousCodeInjectionOnUndefInstr was used to implement calling
user code in kernel mode won ARMv6.
Signed-off-by: Kent McLeod <kent@kry10.com>
Remove all support for ARMv6 architectures now that all platforms and
CPUs that use this architecture have been removed.
Signed-off-by: Kent McLeod <kent@kry10.com>
The platform was the original verification target of seL4 over 10 years
ago and by now there doesn't appear to be any ways to obtain new
hardware.
Currently, the KZM platform is the only ARMv6 platform and supporting it
requires a few work-arounds for emulating mechanisms that newer hardware
supports. Removing this platform also implies removing armv6 support
soon.
Signed-off-by: Kent McLeod <kent@kry10.com>
Moving the type checks avoid the need for conditional compilation. This
also allows simplifying some include file dependencies.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Use SMP_TERNARY() macro.
- Rename get_hart_id() to plic_get_current_hart_id(), as this is just a
helper function for the other PLIC code in this file.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
RISC-V defines the concept of a PLIC, but leaves the details open. The
driver is for the PLIC of the SiFive U54/U74 SOC, which is used on
the HiFive Unleashed/Unmatched and Polarfire board.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- describe PLIC behavior and corner cases.
- provide a common header file for the API.
- add a dummy PLIC driver for spike.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- Move CSR SIE access wrappers to generic code.
- Move CSR SIE/SIP bit constants to header file.
- Rename CSR SIE/SIP bit constants to use the names from the RISC-V
specification.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
MODE_RESERVED is unused on RISC-V, so remove it from the code base. It
can be brought back when needed based on the state of the ARM
implementation, which has been clean up to remove global dependencies.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- define NUM_RESERVED_REGIONS to align ARM and RSIC-V code
- add runtime checks to catch errors. These checks can't be static or
use assert(), as the parameters are passed by a kernel loader. They
must be considered dynamic and can potentially change any time out
of the kernel's control.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Update GIC_VCPU_MAX_NUM_LR constant to reflect that only 16 list
registers are supported on GICv3. The kernel still reads the actual
number of supported list registers out of the GICH_VTR register so the
kernel would still do the right thing before this change.
Signed-off-by: Kent McLeod <kent@kry10.com>
This adds sufficient kernel support for the GICv3 interrupt controller
to be used in a virtualization context on aarch64.
This set of changes has some limitations, however it is still an
improvement on the status quo.
Limitations:
1: This only provides support for aarch64. Anyone wanting support
for aarch32 + GICv3 + virtualization would need to add additional
code.
2: This code only supports 32 priority levels. Support for more
than 32 priority requires changing the get/set_gic_vcpu_ctrl_apr
interface. This is feasible, but requires a more invasive set of
changes. 32 priority levels has been shown to be sufficient in
practise.
Impacts on verification:
This set of changes should only impact Aarch64 Hypervisor
configurations. This is not yet verified so should not have
an impact on verification.
Level of testing:
This has been tested on an iMX8QXP based board. Testing
has at this point in time been limited to a single virtual
machine.
Note: support for this board is not yet upstrea, but is
currently being prepared.
Explanation of changes:
Ideally a new config item would not be required and this
could be driven purely by DTS and hardware.yml configuration.
However, the structures.bf requires changes. This can only
deal with config.h header files, not other more complex
header files. As such it was necessary to introduce a config
item which can be used for this purpose.
The appropriate platforms (as determined by examination of
DTS files) have been updated with the appropriate config
setting. This config setting only has any relevance if
hypervisor mode is already enabled, so should not cause
any difficulty for existing code or configuration.
Note: No testing has been performed on the updated
platforms.
There may be alternative factorings of this, which could
be considered in future work.
Signed-off-by: Ben Leslie <benno@brkawy.com>
- The field 'slot_pos_max' from 'ndks_boot' is not needed, the value
stored there is the constant BIT(CONFIG_ROOT_CNODE_SIZE_BITS).
- Improve the error message if the limit has been reached
Signed-off-by: Axel Heider <axelheider@gmx.de>
The structure actually describes kernel frames and not kernel devices.
In most of the cases a peripherals will fit into one page, but some can
need more pages. On some platform there are no kernel devices at all.
Provides the macro NUM_KERNEL_DEVICE_FRAMES as simple way to find out if
there are mapping that hides the corner cases. This eventually allows
implementing a generic handling even on RISC-V without much overhead, so
the hack for HiFive/Spike can be removed.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This removes the operations that trigger a reschedule or reprogram the
timer from `preemptionPoint` to ensure the relevant state updates in
the proof occur where they are easier to verify.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The L2 cache handling functions were copied from the ARM code in the
initial port, but they are not used on RISC-V. Remove them from the
code base, they can be brought back if a platform has an L2 cache that
needs to be maintained.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
Turns out the invariant 17109eb8c9 refers to is hard to prove
because it is not true, and the runtime check is necessary. This
assertion fails in sel4test SCHED_CONTEXT_0003 (Basic
api_sc_bind/UnbindObject testing).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a comment to clearly state the functions are empty on purpose, but
they still need to be provided to support the generic code flow.
Signed-off-by: Axel Heider <axelheider@gmx.de>
The functions insert_region() and create_rootserver_objects() are not
used outside of boot.c, so there is no reason to make it publicly
available.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Replace the macro SMP_TERNARY(getCurrentCPUIndex(), 0) by the much
simpler macro CURRENT_CPU_INDEX() that does the same.
Signed-off-by: Axel Heider <axelheider@gmx.de>
CURRENT_CPU_INDEX() is supported to return a word_t. The C parser from
the verification toolchain requires declaring word_t constants without
casting integer values to word_t.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This fixes a correctness and security issue where uncached user
mappings might see old data from before the clearMemory operation.
See also the discussion on GitHub issue #481
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Also merge create_device_untypeds() and create_kernel_untypeds() into
create_untypeds() to simplify the code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Make the definition for NULL generic, so it can be used in constants
that are shared by C and assembly code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Provide the macro ULL_CONST() for 'unsigned long long' constants, and
use it where applicable.
- Add a verbose explanation why the 'unsigned long long' type is used
for time constants.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Reorder the macro definitions to ensure things are define before they
are used.
- provide a verbose explanation why the UL_CONST() macro is needed.
- make BIT() macro is defined generic by using UL_CONST().
Signed-off-by: Axel Heider <axelheider@gmx.de>
Also make the output more verbose in case of errors, which is
helpful when porting the kernel to new platforms.
Signed-off-by: Axel Heider <axelheider@gmx.de>
With this change, even architectures which do not use a distinct region
to map the kernel ELF will use the `kpptr_to_addr` to translate any
address from the kernel region.
This ensures that these accesses are correctly checked for bounds when
used and will make it easier to move the ELF mapping into a distinct
region of virtual address space.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Move all of the virtual to physical translation functions into a single
common file and use the updated constants.
Signed-off-by: Curtis Millar <curtis.millar@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>
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 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>
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>
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>
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>
When ksDomainTime reaches 0 the current domain expires and the next
domain is switched to. This change performs the domain time accounting
in one place, in updateTimestamp, and avoids situations where ksConsumed
is reset without also updating ksDomainTime such as in chargeBudget.
Calling rescheduleRequired in the domain expires ensures that a new
thread will be chosen in the scheduler after the domain has been
advanced. Any remaining ksConsumed will be charged to the outgoing
scheduling context when it is switched away from.
Signed-off-by: Kent McLeod <kent@kry10.com>
Rather than charge consumed time to the current thread at the point
where it is exhausted in a long-running syscall, we only check whether
checkBudget would fail and raise an exception if it would. We then
always charge after handleInvocation rather than avoid-double charging.
This is done as it is easier to add the exhaustion case in the abstract
spec in this manner (without also adding changes to the current SC).
Signed-off-by: Curtis Millar <curtis@curtism.me>
When determining whether a SC donated from the notification should be
returned, we must ensure not to try and return a NULL SC to a
notification with not bound SC.
This could occur when a passive server performs a NBSendWait/NBSendRecv
with a notification in the receive phase, where the SC for the receiver
was returned in the send phase and the notification has no bound SC.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
As this variable bounds both the period and the budget and the period
itself bounds the budget, the name for this variable would be more
appropriately named 'MAX_PERIOD'
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
See: https://sel4.atlassian.net/browse/SELFOUR-2830 for details.
On SMP configuration the `ic ialluis` instruction must be used
to ensure the I-cache on all cores is invalidated.
Signed-off-by: Ben Leslie <benno@brkawy.com>
This adds a flags parameter to SchedControl_Configure to enable
configuration of a sporadic SC.
This also allows flags to be added in the future as needed without
breaking the API.
This allows the user to configure an SC either to be constrained as a
sporadic task where accumulated time is only delayed to when a task has
become runnable (implementing the sporadic server algorithm) or
whenever the task becomes the current executing task (implementing the
sliding-window constraint as in constant-bandwidth servers).
This can be used to prevent non-realtime tasks from exceeding bandwidth
under any circumstances, even in an over-committed configuration, whilst
also allowing work-conserving tasks to be configured in the same system.
To implement sporadic servers, we need to ensure that the suspension of
a task cannot be used as a mechanism to amplify budget of a task by
granting that task access to effectively multiple periods worth of
replenishments within a single period.
To align the implementation of SCs with the model of sporadic servers we
must delay available time until the release of a task. Within seL4, a
release would be any time where an SC changes from not being associated
with a Running, RunningVM, or Restart thread to one that is.
This can occur when an SC is bound to a new thread in such a state or
when a thread changes to such a state from any non-running states.
Critically, replenishments should not be delayed at the point when an SC
becomes the current SC (as was the case prior to this commit). This has
the effect of enforcing a continuous, constant bandwidth which is a
restriction that is incompatible with standard scheduling logic.
Accounting for this requires inserting a new refill_unblock_check
call whenever a sporadic SC is unblocked and removing the
refill_unblock_check call from when said SC is scheduled.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Actually divide by KHz frequency when on a platform that uses a clock
that does not have an integer MHz frequency for aarch64.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
A previous commit (9ec5df5f) to provide more efficient CLZ (count
leading zeros) and CTZ (count trailing zeros) removed the `__clzsi2` and
`__ctzsi2` symbols, due to a misunderstanding of the types of these and
other library functions expected by GCC's intrinsics. 9ec5df5f broke the
riscv32 build.
This commit corrects the misunderstanding:
- `__clzsi2` and `__ctzsi2` are reinstated with correct types.
- The types of `__clzdi2` and `__ctzdi2` are corrected.
- `__clzti2` and `__ctzti2` are removed, since seL4 contains no compiler
intrinsics that would require them.
- `clzl` and `ctzl` dispatch to the appropriate library functions based
on the size of `unsigned long`.
- Configuration options are updated to ensure that the library functions
are included in the kernel binary only when needed.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
`register_t` only needs to be able to index into the TCB user context
array, which has 35 entries. Therefore `uint8_t` is sufficient.
Using the smallest possible type for `register_t` helps with binary
verification. This shrinks static read-only data, which in turn reduces
the complexity of binary verification proof search.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The `register_t` type was intended to be used for *indices* into the
user context, but various sbi operations in the RISC-V kernel have used
it for register *contents*. This commit changes those to use `word_t`
for register contents.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
For RISC-V platforms that do not provide machine instructions to count
leading and trailing zeros, this commit includes more efficient library
functions. For verification, we expose the bodies of the functions to
the proofs.
Kernel config options `CLZ_BUILTIN` and `CTZ_BUILTIN` allow selection of
whether compiler builtin functions should be used. These are only
supported on platforms where the builtin compiles to inline assembly. By
default, the options are on for all platforms except RISC-V.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The binary verification tools perform inlining of C specifications, to
simulate inlining that has been performed in the binary. This means that
`DONT_TRANSLATE` and `inline` are incompatible, since the binary
verification tools require C specifications for any functions that have
been inlined in the binary.
This `DONT_TRANSLATE` annotation was added with a `MODIFIES` annotation
for proofs that the C refines the abstract specification. Those proofs
have been updated such that the annotations are no longer needed.
Reverts 1fba3d9e68 and b903cb7372.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The RISC-V calling convention specifies that when a C function takes an
argument by value, the binary function should take the argument by
reference, if the value is larger than 2 pointer words.
For binary verification, we avoid implementing this aspect of the RISC-V
calling convention, by eliminating all such function arguments for
functions which are not inlined.
In this commit, we remove the `slot_range_t` structure altogether. For
the small number of functions which previously used this type, we unpack
the structure into three separate arguments.
Even though we are primarily concerned with RISC-V, we remove
`slot_range_t` arguments across all architectures.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The RISC-V calling convention specifies that when a C function takes an
argument by value, the binary function should take the argument by
reference, if the value is larger than 2 pointer words.
For binary verification, we avoid implementing this aspect of the RISC-V
calling convention, by eliminating all such function arguments for
functions which are not inlined.
In this commit, we remove `extra_caps_t` function arguments. This
primarily concerns invocation decode functions. Since `loookupExtraCaps`
already stores extra caps in a global `current_extra_caps`, this
essentially amounts to eliminating many redundant structure copy
operations.
On some execution paths involving IPC, the extra caps lookup may happen
twice: first in the invocation decode, and then for cap transfer in the
performance phase of the IPC operation. Because the two phases are
entirely distinct, there is no interference in the use of a common
global variable.
Even though we are primarily concerned with RISC-V, we remove
`extra_caps_t` arguments across all architectures.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
A 'released' SC is one that has been configured with its head refill in
the past.
An 'active' checking function checks for whether an SC has been
configured.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Different microarchitectures & configurations save different sets of
VCPU registers when the current VCPU is not active. This generalises the
handling of these cases such that each microarchitecture defines which
regisers are managed in this fashion.
Fixes regression introduced in 454dfd897f
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Most of the uses of these are in functions where the cap type is
statically known and the correct branch could be used directly, but the
compiler does not know this so having these as inlines causes a large
number of accesses to bitfields of unrelated cap types in functions that
manipulate caps.
Moving this out of line makes the results of changing cap bitfields less
noisy.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
For 64-bit, this adds a 2nd-level page table for mapping devices using
2MiB frames instead of 1GiB frames.
The boot mapping and hardware header generator have also been fixed to
correctly report the number of large frames needed for devices rather
than only reporting the first. The frame size is also specified
correctly (rather than assuming mapping with 4KiB frames).
This likely fixes an issue whereby only the first 4KiB frame of a device
was reserved but the remaining region of that kernel device could be
mapped at user level.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This is a shortcut for dealing with the inline assembly inside to
prevent the modifies analysis from picking up every part of the state.
For any future binary correctness analysis, this will need to be
removed, and instead an appeal made to inline assembly being unable to
modify the heap.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
merge the PLIC drivers for ariane and hifive
Signed-off-by: Nils Wistoff <nwistoff@iis.ee.ethz.ch>
Reviewed-by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
This makes the kernel configuration defaults public and known to the
user level. Generally shouldn't depend on these definitions outside of
code testing and benchmarking the kernel.
Signed-off-by: Curtis Millar <curtis@curtism.me>
This implements the syscall that maps the kernel log buffer for debug
and bencharking and defines the constant used to reference the buffer.
The x86_64 kernel log buffer is stored in the page directory used for
the kernel devices in the entry after the one used for the kernel device
page table.
Signed-off-by: Curtis Millar <curtis@curtism.me>
This removes the explicit CMake configuration for the kernel log buffer
and replaces it with a #define that is enabled for the required
configurations.
Signed-off-by: Curtis Millar <curtis@curtism.me>
The kernel connects ASID used in MMU and context banks used in
SMMU, and conducts TLB invalidation on context banks if a page
entry is invalidated from MMU is also used in SMMU.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing support to delete stream ID caps and remove any assigned
context banks to deleted stream ID caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls on stream ID caps that unbinds its
context banks. Any future transaction using this stream ID
will result on faluts.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing a system call that removes an assigned vspace root from its
context bank. This operation causes the context bank being disabled
as it does not have a valid vspace root after the unassignment.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
The mapped attributes in both context bank and stream ID caps
are reundant for maintaining the semantics on those caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls for conducting TLB invalidation operations
on all TLB entries or entries in a context bank.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls that binds context banks to stream IDs.
Once the stream ID is bound, the transaction using that SID is
enabled.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Supporting user-level applications to assign vsapce root to context
banks through system calls. This commit also configures the context
bank according to stage 1 or stage 2 requirement.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Providing system calls on stream ID control cap and context bank
control cap for creating stream ID and context bank caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Adding the master control caps that are used to create transaction
and context banks caps. This commit includes the internal kernel
structure that required to manage any created transaction and
context bank caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
This renames the RISCV PLIC driver file hifive.h to riscv_plic0.h to
better reflect the fact that the driver could be used for a number of
platforms that use the PLIC used by SiFive and SiFive derived platforms.
Signed-off-by: Jesse Millwood <jesse.millwood@dornerworks.com>
reply_unlink takes a reply and remove the link between that reply
and its tcb. This link always exists at the call site and the tcb
information is always avaialble, or can be made available.
This commit adds this tcb as an extra argument to aid varification.
Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
- This commit largely copies the ARM way of handling
device tree blobs on to RISC-V, as they work pretty
similarly.
Signed-off-by: Michael Yoo <Michael.Yoo@data61.csiro.au>
A previous commit produced some build errors, since it converted the
`REFILL_HEAD` and `REFILL_TAIL` macros to functions returning
`refill_t`, and the results were used as lvalues. This commit returns
pointers instead, and also converts `REFILL_INDEX` to a function.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
SimplExportAndRefine can't handle the level of pointer arithmetic being
performed by `REFILL_INDEX` if it's literally inlined into a function,
however it *can* handle that arithmetic if it's in a separate function.
Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
The base pointer is wrong, and it creates some nasty corruption down the
line (only affects debug builds).
Signed-off-by: Sylvain Gauthier <sylvain.gauthier@data61.csiro.au>
The current state of MCS seL4 verification makes use of an invariant
that whenever the scheduler action is set to "resume current thread"
the current thread and the current sc are bound together. Since
maybeReturnSchedContext may unbind a thread from a scheduling context,
it should perform a check on whether it is unbinding from the current
thread, and in that case call rescheduleRequired which will (among
other things) change the scheduler action.
Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
If a thread is running on the SchedContext of it's bound notification,
when it next does a blocking recv/wait operation on an ep the SC is
removed. This allows the thread to return to being a passive thread to
receive the next notification or ep message.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
The capacity does not need to be passed as an argument to
refill_check_budget as all information that it was being used for can be
dertermined from the usage directly.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
We need to bound the time the user provides to configure scheduling
contexts to avoid malicious or erraneous overflows of the scheduling
math. Make the max period/budget 1 hour.
1 hour is sufficiently small that it will fit in a 32-bit error message.
1 week is sufficiently small for 64-bit platforms.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Special debug variables that were previously stored at the end of the
tcb_t struct often cause the struct to get too large for the power-of-2
sized untyped object definition. This change moves these variables into
a new structure named debug_tcb_t that is located between the TCB CNode
and the tcb_t struct within a tcb kernel object. Because tcb_t needs to
be stored on a power-of-2 aligned boundary and the TCB CNode only
contains < 5 slots, there is easily > 512 bytes of unused data in every
tcb object. The kernel verification needs to be sure that objects don't
overlap in memory and so this space can't be easily used in a release
build at the moment, but for debug configurations using it shouldn't be
an issue.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
For each thread also track number of times scheduled, number of kernel
entries and amount of cycles spent inside the kernel. Also add
core-wide totals for each.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Change benchmark_track_reset_utilisation to take a tcb object parameter
so that the function is more widely applicable.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Create per-node global definitions for utilization variables.
This enables the tracking to more cleanly work on SMP configurations.
As resetting and starting the counters via SysBenchmarkResetLog only
updates the counters of the current thread and idle thread on the
current node it was not possible to accurately record utilization
statistics across multiple nodes. Now each node can have its tracking
independently started, stopped and queried. It is possible to add
additional syscalls in the future for doing this for all nodes in a
single syscall.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
This definition is intended to select functionality for processing a PMU
cycle counter overflow interrupt while using the thread utilization
benchmarking feature. Instead of forcing for all Arm platforms, only set
it if KERNEL_PMU_IRQ is defined and the IRQ has been configured
properly.
The consequence of this change is that aarch64 platforms that
have a 64bit counter that is unlikely to overflow do not need an
overflow interrupt to be defined.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
VTD context table entry is 16 bytes, and there are 256 entries
in a context table.
The commit is based on PR #185 by laokz
Co-authored-by: laokz <laokz@foxmail.com>
Signed-off-by: Yanyan Shen <yshen@cog.systems>
Strengthen the clh_lock_acquire to use release on the atomic_exchange
that makes the node public. Otherwise (on ARM & RISCV), the store to
the node value which sets its state to CLHState_Pending can become
visible some time after the node is visible.
In that window of time, the next thread which attempts to acquire the
lock will still see the old state (CLHState_Granted) and enters the
critical section, leading to a mutual exclusion violation.
Signed-off-by: jonas <s9joober@gmail.com>
The implementation of try_arch_atomic_exchange does not correctly pass
RELEASE memory ordering (or stronger) to the exchange operation.
To acknowledge this, try_arch_atomic_exchange is replaced by a relaxed
try_arch_atomic_exchange_rlx which does not apply any memory ordering.
Instead, the memory ordering is now added manually by
sel4_atomic_exchange. This provides better latency for interrupts as no
barriers are evoked inside the loop which performs the relaxed exchange
and checks for interrupts.
Furthermore, the new manual application of barriers ensures the memory
ordering passed to sel4_atomic_exchange.
Signed-off-by: jonas <s9joober@gmail.com>
This makes all daigrams have their first address at the end of the
diagram and their last address at the start of the diagram.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
kernelBase was used inconsistently between different architectures to
refer to the either of the first kernel address or the first address of
the mappings of the kernel ELF region specifically.
These have been replaced with more consistent use of constants
explicitly describing which region is being referenced.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Each architecture now only needs to describe the bounds of the three
memory regions: the 1:1 mapped physical memory region, the kernel ELF
region (which may or may not overlap the physical memory region) and the
device / kernel page table region.
The physical base address of the 1:1 mapped physcial memory region and
the kernel ELF region must also be specified.
The top of user addressable memory (where in the same virtual address
space as the kernel) is defined by USER_TOP.
The physic memory virtual mapping is described by PPTR_BASE and
PPTR_TOP. The base physical memory address is PADDR_BASE and is the
physical address used to map PPTR_BASE.
Don't use kernelBase when referring to the base of the 1:1 mapped
physical memory window.
The kernel ELF virtual address region is described by KERNEL_ELF_BASE
and extends until the virtual address of the symbol `ki_end` which is
created by the linker. KERNEL_ELF_PADDR_BASE is the base address of
the physical memory region used to map the kernel and is the address to
which KERNEL_ELF_BASE maps.
KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE do not need to be aligned to a
page size boundary as they are approriately truncated during boot by the
`map_kernel_window` function.
KDEV_BASE describes the base virtual address of the kernel device region
and the region is assumed to extend to the end of virtual memory.
Note: The offset between PPTR_BASE and PADDR_BASE is used to translate
the virtual address of all untyped objects to physical addresses. This
includes device untyped objects or frame objects where the virtual
address does not fall within the 1:1 mapped physical memory region.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Adapted musl printf implementation using our output abstraction.
Floating point specifiers are not supported in this adaptation.
Modified the code to also match our style and make it
less unnecessarily complex.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
Verification requires packed C structures for reasoning. The C parser
assumes uint64_t (unsigned long long) has 8-byte alignment, thus size of
struct vcpu should be a multiple of 8. As this was not the case, we add
an extra word_t (4 bytes) for padding.
This type of manual padding is naturally fragile and will break as soon
as any field of struct vcpu changes in size by < 8 bytes.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This register is visible to software executing at PL0 but not writeable.
Storing it in the VCPU context required custom save/restore handling as
it had to be explicitly handled when switching from a VCPU thread to a
non-VCPU thread so that it didn't become a channel. It is possible to
now update this register via seL4_TCB_WriteRegisters for software
executing at PL0.
This also fixes a bug where if a vcpu-thread is switched for a
non-vcpu-thread and then switched to a different vcpu-thread the
original vcpu-thread's copy of this register will get set to 0.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
The FPU enable/disable state is cached for all architectures, so
the RV64 FPU code is updated accordingly.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
lazyFPURestore is call during kernel exits. Then, the FPU is
enabled or disabled accordingly by chaning the SSTATUS
of the current thread. The SSTATUS will be written to the
physical SSTATUS CSR, and thus the FPU accesses will be
enabled or disabled.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
These functions are called by the arch-independent functions
to save and restore FPU state lazily.
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
This changes the semantics if `isBlocked` to not include the 'inactive'
state when it returns true. The old semantics for isBlocked are provided
by `isStopped`.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
