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>
Don't allow a domain capability to be invoked on the first phase of a
two phase syscall. Performing this action can lead to a thread being
enqueued in a scheduler in the first phase and accepting IPC in the
second.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The SC of a thread that has timed-out cannot be donated to the time-out
fault handler, preventing recursion on timeout faults.
This prevents that donation from occuring but will leave
the fault handler 'running' but without any SC.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Although it is true that any SC that refers to the same location in
memory will have the same size, it is difficult to prove. This
explicitly checks to remove the burden of proof.
This approach is already used when determining whether two CNodes refer
to the same region.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
If the current SC is bound to a notification and the current thread is
deleted it is possible for the current SC to be signalled by the
pre-emption. In this case the current SC may be donated to another
thread without being changed the value in ksConsumed.
refill_unblock_check can only be called on the current SC if
ksConsumed is 0. Further, it makes no sense to call refill_unblock_check
on the current SC as it was not blocked.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The call to `checkBudget` should always return true as this function
can't be called unless the current thread has sufficient time.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Fixes interrupt flag reset upon nested interrupt resume.
There were intermittent test failures on x86/32 characterised by
assertion failures at `c_nested_interrupt()`. The kernel only allows
one pending interrupt at a time, yet the kernel was entering
`c_nested_interrupt()` multiple times during a single entry-exit.
This should have been disallowed by `getActiveIRQ()` checking against
any pending interrupts.
`c_nested_interrupt()` is "entered" by the pc99-specific
`receivePendingIRQ()` helper (i.e. `sti; nop; cli`). If the nested
interrupt handler fails to clear the interrupt flag before running
`iret`, there's a small window between `nop; cli` that could trigger
a second nested interrupt.
This fixes the nested interrupt trap to correctly clear the interrupt
flag in the EFLAGS register that is restored upon `iret`.
Signed-off-by: Michael Yoo <Michael.Yoo@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>
- seL4_BenchmarkDumpAllThreadsUtilisation: Prints a JSON formatted
record of total and per-thread utilisation statistics about the system.
This currently includes a thread's total cycles scheduled, total number
of times scheduled, total cycles spent in the kernel and total number of
times entering the kernel and then totals of each for all threads on the
current core.
- seL4_BenchmarkResetAllThreadsUtilisation: Resets the current counts of
every user thread on the current core.
These syscalls are only available in a Debug build configuration as they
use a kernel debug list of all of the threads that exist for a given
node.
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>
The total bits should include the page bit and index bits.
The commit is based on PR #185 by laokz.
Co-authored-by: laokz <laokz@foxmail.com>
Signed-off-by: Yanyan Shen <yshen@cog.systems>
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>
doRemoteClearCurrentVCPU should be called when the vcpu->last_cpu
is not the current CPU that is executing vcpu_finalise.
The commit is based on PR #185 by laokz.
Co-authored-by: laokz <laokz@foxmail.com>
Signed-off-by: Yanyan Shen <yshen@cog.systems>
The PCID feature is the 17th bit in ECX when CPUID is called with
EAX=1. The constant for testing the feature should be 0x20000.
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 commit refactors the github workflows into two
file (push/pull request), makes use of the new central
seL4 github actions, and adds the preprocess test for
pull requests.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
On e.g. FreeBSD, Bash lives at /usr/local/bin/bash. This change
makes the script find Bash wherever it may be hiding.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Fixes#110 on Github. As the issue describes, `**` is not
the right syntax.
We could write `**/*.pyc` instead, but according to
https://git-scm.com/docs/gitignore a pattern already
matches at any directory level if it doesn't contain `/`.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
The first two data arguments used for the printf don't match what's
expected in the format string and are reversed.
Signed-off-by: Damon Lee <Damon.Lee@data61.csiro.au>
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>
This should not change behaviour, but makes sure we replicate the test
setup more precisely.
Signed-off-by: Gerwin Klein <gerwin.klein@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>
