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>
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 register is visible to software executing at EL0 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 EL0.
This also fixes a potential 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.
This is the first part of the seL4 MCS. This commit:
* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.
Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).
Depending on the physical address range the top level translation table
may be a page upper directory or a page global directory. Rename in
libsel4 the invocations on top level structures to be on an
seL4_ARM_VSpace rather than an seL4_ARM_PageGlobalDirectory.
Switched appropriate naming conventions.
Was using the aarch64, have switched to aarch64 names.
TIPDRURW -> tpidr_el0
TPIDRURO -> tpidrro_el0
TPIDRPRW -> tpidr_el1
Switch TLS register on aarch32 from TPIDURO (tpidrro_el0) to tpidr_ro so
that it can be written to from user-land.
Thread ID registers tpidr_el0 have been added to the user context for
aarch32 and aarch64.
Only the thread ID that is writeable from EL0 is saved in the TCB and
saved/restored on context switch.
Thread IDs that are only changed within a VM (the read-only thread ID
for exception level 0 and the thread ID for exception level 1) are
stored in the VCPU and saved and stored as part of VM enable/disable.
Thread IDs that are only changed with VMs have been separated out into
hypervisor code.
TLS_BASE virtual register is replaced with FS_BASE and GS_BASE virtual
registers.
The FS_BASE and GS_BASE virtual registers are moved to the end of the
context so they need not be considered in the kernel exit and entry
implementation.
Removed tracking of ES, DS, FS, and GS segment selectors on kernel entry
and exit.
ES and DS are clobbered on kernel entry with the RPL 3 selector for a
DPL 3 linear data segment.
FS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with FS_BASE as the base. This is done on exit to reload the value from
the GDT.
GS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with GS_BASE as the base. This is done on exit to reload the value from
the GDT.
Kernel entry and exit code is refactored, simplified, and improved in
light of the above changes.
x64: update verified config to use fsgsbase instr
The verification platform for x64 relies on the fsgsbase instruction.
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.
This change generates doxygen groups for each object type, which allows us to create sections in
output documents for each object. This has the advantage that we can later label those sections and
link to them from the main document. Additionally, it improves nagivation of the API docs.
Changes the way IO ports work such that instead of 'minting' IO port caps down into new
IO port caps with smaller ranges new IO port ranges must be allocated centrally from
an IO port control cap. This mechanism acts in a very similar fashion as IRQ handler/control
capabilities and ensures that allocated IO ports do not overlap. Disallowing overlapping
IO ports is necessary to ensure the CDT remains valid as capabilities are deleted.
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.
Manual labels for methods are inferred unless specified in the api
description. This change extends this inference to prevent slashes
appearing in method labels. It also refactors the logic for label
inference to be more readable.
If no documentation is provided for the return value of a function, the
documentation generator will attempt to infer the documentation based on
the return type.
This change
* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4
Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.
* commit 'be68b0c0bde5bfa439376fac4c8be255dacaa958':
libsel4: Allow invocations to not use IPC buffer
Retain in-register error descriptions when not using IPC buffer
- Fixes "lost" error descriptions when using *WithMRs system call
variants [1].
- Only stores real registers to IPC buffer if there's an error.
- If there's an error in a struct-returning function, return
early without setting any struct members.
- Passes the sabre/qemu test suite... with and without --buffer!
[1] https://sel4.systems/pipermail/devel/2016-October/001079.html
Where MCP = Maximum Controlled Priority
This commit adds:
* seL4_TCB_SetMCPriority
and changes the arguments to
* seL4_TCB_Configure
As of this commit, a thread cannot create or set a threads
priority (including itself) above its mcp. Previously the kernel
did this check against a threads priority, which prevented a thread
from setting it's own priority down and then up again.
Condition invocation labels where added in commit 73837c8ace
This commit guards usage of conditionally generated labels during generation
of the syscall stubs.
They would get shifted by the size of the type rather than the
size of the word. This wasn't detected initially as the master
branch of the kernel does not have any double word types in the API.
