The prior behavior would emit ANSI escape codes which set the terminal
foreground color to black bold (`[30;1m`), leaving the default
background color. On many terminals configured with a dark color scheme,
this creates black on black characters, i.e. the output is invisible.
This change moves to a better adapted output, where the output is only
marked as bold (`[1m]`), which works well on all color schemes.
Fixes#1243
Signed-off-by: wucke13 <wucke13@gmail.com>
This is not supposed to happen, thus printing the value gives a bit more
insight what might have happened here.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Defined to be equal to CONFIG_NUM_DOMAINS. seL4 makes control-flow
decisions based on whether the number of domains is greater than 1. To
perform refinement proofs independent of the number of domains, we need
to follow both branches of these if statements, pretending we don't know
which branch will be taken. This is made significantly harder when
preprocessed C code ends up with comparisons like `if (16 > 1)`.
By adding a numDomains that appears in the C code, we obtain a name we
can point to and link up to higher level specifications.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Replace the macro SMP_TERNARY(getCurrentCPUIndex(), 0) by the much
simpler macro CURRENT_CPU_INDEX() that does the same.
Signed-off-by: Axel Heider <axelheider@gmx.de>
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>
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>
The format string in userError is now written to
the IPC buffer for debugging purposes.
This requires an snprintf which reuses vprintf with
a new structure for handling how output is done.
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 changes the budget/remaining fields in scheduling contexts
to contain timer ticks, not number of abstract sel4ticks.
seL4_SchedControl_Configure now takes microseconds, not ticks.
This commit is plat-independant - the platform and arch specific
timer code follows in later commits.
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.
These files can be included normally using libsel4 include paths. This
removes situations where the same file is available under different
include paths due to symlinking into different directory structures.
Now these bitfield definitions are generated from the same source file
in the kernel and libsel4, and also result in the same include path: <sel4/shared_types_gen.h>
GrantReply is a new access right added to endpoint capabilities, which
allows seL4_Call to be used on those capabilities (specifically, it
allows reply caps *only* to be granted across endpoints).
Prior to the addition of GrantReply, endpoint capabilities required the
Grant access right, which allowed any arbitrary capabilitiy to be
transferred over an endpoint. Using GrantReply, systems can now be
constructed where threads using seL4_Call over an endpoint do not need to be in the same
security subsystem.
- don't print header every time
- drop address, it's not very useful and clutters the output
- add pretty header
- use new leading spaces feature in kprintf
In file included from ./kernel/src/api/faults.c:16:
In file included from ./kernel/include/api/syscall.h:19:
./kernel/include/api/debug.h:51:38: error: comparison of constant 'SysSend' (-3) with expression of type
'seL4_Word' (aka 'unsigned long') is always false [-Werror,-Wtautological-constant-out-of-range-compare]
if (ksKernelEntry.syscall_no == SysSend ||
~~~~~~~~~~~~~~~~~~~~~~~~ ^ ~~~~~~~
./kernel/include/api/debug.h:52:42: error: comparison of constant 'SysNBSend' (-4) with expression of type
'seL4_Word' (aka 'unsigned long') is always false [-Werror,-Wtautological-constant-out-of-range-compare]
ksKernelEntry.syscall_no == SysNBSend ||
~~~~~~~~~~~~~~~~~~~~~~~~ ^ ~~~~~~~~~
./kernel/include/api/debug.h:53:42: error: comparison of constant 'SysCall' (-1) with expression of type
'seL4_Word' (aka 'unsigned long') is always false [-Werror,-Wtautological-constant-out-of-range-compare]
ksKernelEntry.syscall_no == SysCall) {
~~~~~~~~~~~~~~~~~~~~~~~~ ^ ~~~~~~~
- 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.
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.
This is a *breaking API change*
This commit:
* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
the user calling seL4_SetTag() first (seL4_MessageInfo is passed
in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes
Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.
benchmark_track.h does not depend upon anything in debug.h and
so it does not need to include it. Once this include is removed
debug.h can pull its definition of ksKernelEntry from benchmark_track.h
This commit implements the body of SELFOUR-499. The API exposes the x86 DR0-7
and ARM coprocessor 14 features to userspace by virtualizing them as context-
switched registers in the TCB. Implemented as TCB invocations. This feature is
only built when CONFIG_HARDWARE_DEBUG_API is selected.
* Add low-level support routines for setting, unsetting, getting, enabling
and disabling breakpoints.
* Add support for single-stepping as well.
^ Single-stepping is not supported on ARMv6 since the hardware
doesn't have support.
^ ARM implements single-stepping as instruction breakpoints
configured to fault on every instruction -- this is achieved through
the "mismatch" mode, which is only supported from ARMv7 onwards.
* Also support explicit software break requests, a la "BKPT" and "INT $3".
* New invocations:
* seL4_TCB_SetBreakpoint().
* seL4_TCB_GetBreakpoint().
* seL4_TCB_UnsetBreakpoint().
* seL4_TCB_ConfigureSingleStepping().
* New constants:
^ Event types:
^ seL4_InstructionBreakpoint.
^ seL4_DataBreakpoint.
^ seL4_SoftwareBreakRequest.
^ Access types:
^ seL4_BreakOnRead.
^ seL4_BreakOnWrite.
^ seL4_BreakOnReadWrite.
^ Exports:
^ seL4_NumHWBreakpoints.
^ seL4_NumExclusiveBreakpoints.
^ seL4_NumExclusiveWatchpoints.
^ seL4_NumDualFunctionMonitors.
^ seL4_FirstBreakpoint.
^ seL4_FirstWatchpoint.
^ seL4_FirstDualFunctionMonitor.
See documentation in the seL4 API manual.
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.
