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>
