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>
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>
- 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>
Introduced a new config flag to enable
userError format strings to be written to the IPC buffer.
Another config bool has been introduced to toggle
printing the error out and this can also be set at runtime.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
This commit introduces a new fault type, seL4_Fault_VPPIEvent.
This change means the kernel can reserve PPI interrupts and virtualise
them via delivering the irq to the active vcpu through a
specific fault. This enables multiplexing PPI IRQs across multiple VCPUS
which requires correctly masking and unmasking the IRQ depending on
which VCPU is running.
A new VCPU invocation, seL4_ARM_VCPU_AckVPPI is also added for
acknowledging the handling of the IRQ. This takes an IRQ as a parameter
but will only accept IRQ numbers that are sent as VPPIEvent faults.
Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
- Remove Remap function from seL4 API for arm, x86, riscv and the
respective invocation implementation.
- Update Map as replacement for Remap
- Update manual
This allows a change of rights if the frame being mapped is already
mapped in at the given vaddr. To map a page to a different address,
unmap it first.
Co-authored-by: Hesham Almatary <hesham.almatary@data61.csiro.au>
Co-authored-by: Anna Lyons <Anna.Lyons@data61.csiro.au>
Co-authored-by: Victor Phan <Victor.Phan@data61.csiro.au>
Co-authored-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Created a new syscall, seL4_DebugSendIPI for ARM to send arbitrary SGIs
(software generated interrupts) to arbitrary cores. As SGIs are
specifically PPIs (private interrupts), this syscall effectively allows
to trigger PPIs on arbitrary cores, for debug/testing purposes.
Some platforms and configurations do not allow user code to change the
value of the register used for TLS. On these architectures a syscall can
be used to allow the kernel to update the register on their behalf.
This does not immediately update the value in the user context on many
configurations as the values are only stored in the user context on a
context switch.
This removes the assumption that each platform sotres the IPC buffer
address in a platform-specific register. The IPC buffer address is
instead stored in a thread-local variable in libsel4 which must be
initialised by the runtime.
- renamed an architecture label so that it begins with ARM.
- changed setIRQTrigger so that it takes a boolean value instead of an int.
- Arch_decodeIRQControlInvocation converts the second argument (trigger)
to a boolean immediately.
Add a new invocation which allows an irq handler capability to be
obtained with a specific trigger method (edge or level). Obtaining
this capability modifies the GIC state.
This change updates the vspace chapter to separate the high-level concept of a VSpace from the
architectually defined objects. It also updates the various names for the vspace parameter to all be
vspace.
- increases the maintainability of the docs
- move descriptions of methods to the API reference
- remove hardcoded invocations in manual
This commit removes the content completely from vspace.tex, as it is out of date and needs
restructuring. The next commit does the restructuring.
Introduced a new Doxygen XML tag '<docref>'. The intention of
this tag is to indicate a section of text in the Doxygen XML that
will contain a reference to another section in the Manual e.g.
"See \autoref<sec:x>". As other generation formats aren't aware of
other chapters/sections in the manual, the <docref> encapsulation
allows it to omit the text from the output. The Latex generator
has been modified to continue parsing the 'docref' contents.
Using the bitfield generator to treat guards and badges as a union type can be convenient,
but it requires reserving a bit in the data for the bitfield run time type information.
This type information is not needed by the kernel as it knows implicitly whether the passed
data is a badge or a guard based on the kind of cap being operated on. However, with the
type information present we cannot pass a word sized piece of data to the kernel.
The solution here is to go back to using a plain seL4_Word as the type for invocations
that want a capdata and let the user either construct a badge as a plain word, or use
the seL4_CNode_CapData bitfield for constructing a guard, although they have to manually extract
the word representation out of it.
- when CONFIG_DEBUG is enabled, track all threads
- when CONFIG_PRINTING is enabled, provide seL4_DebugDumpScheduler which
allows the user to dump the state of the kernel scheduler.
There is no way to know how many entries the syscall log contains
otherwise. One option was iterating through until finding a 0
terminator, however this requires the log to be zeroed before each
trial. This changes the FinalizeLog syscall to return the number of
entries.
Previously the #ifdefs for some debug syscalls relied on definitions
from Makefile.flags in sel4_tools. This changes them to use configs
defined in autoconf.h which makes them easier to import when building
projects that don't use sel4_tools.
