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>
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>
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.
- 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.
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.
This commit moves a declaration of `ksKernelEntry` such that it is now only
guarded by `DEBUG`, not additionally `CONFIG_PRINTING`. This allows the kernel
to be built standalone with debugging enabled using the following invocation:
DEBUG=1 TOOLPREFIX=arm-none-eabi- CPU=arm1136jf-s PLAT=imx31 ARCH=arm \
ARMV=armv6 make
Benchmark feature that currently:
- Keeps track of system calls info
- Start time
- Duration
- Capability type
- Invocation tag
- Log the number of invocations of each system call*
- Log the number of invocations for each capability type per syscall.
- Has 3 new syscalls (dump, reset, get size).
- This new feature uses the existing log buffer (which is 1MiB for x86
and ARM). Since the number of syscall invocations is not
deterministic, the logged number of invocations is limited by the size
of the buffer. I suggested to enable the users to pass their own
user-level buffer, to enable more flexibility, later.
- ENABLE_BENCHMARKS is now a parent config option of trace points and
system call track features, they can't be used at the same time.
