This is useful for sel4test et al for testing that a certain
PD has been succesfully migrated between cores, or that it
is running on a particular core.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
a7 is not changed by seL4_Yield, so the original declaration is correct.
However, in some loops GCC 14.2 may drop the load to a7 if a7 or
memory are not declared as clobbered in the assembly block. This is a
problem if *other* code does write to a7. For some reason GCC 14.2 does
not recognise those other loads. GCC 14.3 and GCC 15 both work as
expected.
The problem manifests in SCHED0011 in sel4test.
This change works around the GCC 14.2 problem because GCC 14.2 is the
standard Debian trixie compiler and it is likely that people will hit
the problem even if we say that GCC 14.2 should not be used.
The workaround uses the same implementation of seL4_Yield as the Arm and
x86/x64 versions do: inline call to sys_null with an empty asm volatile
declaring memory as clobbered. The memory clobber declaration eliminates
the miscompilation, and overall the implementations are now consistent.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Nowhere else in the documentation uses the phrase
"Must be a depth of 32"
which seems incorrect for 64-bit riscv.
Also, the index parameter had the same description as root, which
is incorrect.
Signed-off-by: julia <git.ts@trainwit.ch>
This commit's parent renames the interface XML files.
The symlinks added in this commit serve to ease the transition to the
new names for downstream projects.
These links are added:
- include/interfaces/{sel4.xml -> object-api.xml}
- arch_include/*/interfaces/{sel4arch.xml -> object-api-arch.xml}
- sel4_arch_include/*/interfaces/{
sel4arch.xml -> object-api-sel4-arch.xml
}
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Add a comment that they are empty on purpose. They are not removed to
keep the infrastructure in case there will be deprecated items in the
future.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Today the file autoconf.h is created by the CMake build system and thus
HAVE_AUTOCONF is always defined. Time to get rid of some legacy by
removing the check if HAVE_AUTOCONF is set.
Signed-off-by: Axel Heider <axelheider@gmx.de>
These files should have been released under BSD-2-Clause in the first
place (as per parent LICENSE.md file).
Closes#245
Signed-off-by: Gerwin Klein <gerwin.klein@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.
- 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>
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.
We add support for seL4_IRQControlGet and seL4_IRQControlGetTrigger. If
a platform doesn't support setting the trigger, then
seL4_IRQControlGetTrigger will return an error. If the platform doesn't
have a PLIC driver, then it won't have any IRQs that can be requested.
Also authored by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
The registers a7, s2-11, and t3-6 were missing from seL4_UserContext.
We also add these to frameRegisters and gpRegisters, which are used
to implement the TCB invocations for reading and writing these
registers.
Zero-length arrays aren't valid expressions or types in ISO C, so
to keep the c parser happy we need to either remove gpRegisters or
provide some contents for it.
In the past, frameRegisters and gpRegisters distinguished between
those registers preserved across a syscall and those that weren't.
TCB_CopyRegisters allows the caller to choose which set to copy.
Since we preserve all non-return registers, this distinction isn't
relevant anymore and there's no easy way to justify the members of
frameRegisters and gpRegisters.
We arbitrarily choose to put the 'last' register t6 in gpRegisters,
for consistency with the register list in registerset.h and with the
order that registers are restored.
Correct exported functions that were still defined as 'static inline' to
use LIBSEL4_INLINE_FUNC so that they can be controlled by
LibSel4FunctionAttributes.
This is important to other languages that want to bind to the libsel4
static library instead of using the inline C functions.
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.
