- 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.
CONFIG_LIB_SEL4_PUBLIC_SYMBOLS=y will disable inlining for external
interfaces (except deprecated functions), thereby providing public
symbols for easy linkage with other languages.
This also moves the description of TCBSetEPTRoot from the general object
invocation xml file to the x86-specific one to prevent the need for
documentation-generating scripts to distinguish between VTX (ie. x86)
invocations, and truly architecture independent invocations.
JIRA: SELFOUR-606
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.
This commit adds support for using the ThreadID registers of the ARM MPCore
platforms for storing the address of the IPC buffer instead of the globals
frame. The choice of using the user readable/writeable ThreadID register
is chosen, even though it means the user cannot use it for its own
purposes, as it leaves room in the future for doing TLS support in the
user read only register, where compilers expect it.
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.
Rename all functions, constants and types in libsel4 that are in the
general x86 architecture to have an X86 name instead of an IA32 name.
As libsel4 and the kernel share names this requires changing those
in the kernel as well.
All the original IA32 names can still be used for the moment, but are
marked as deprecated.
Restructure the x86 interrupt handling to allow for a more flexible
method of using IOAPIC and MSI interrupts. The essence of this change
is to allow for the user to pick, for both IOAPIC and MSIs, which
CPU vector to use. Additionally there is future support, in the API,
for seL4 to eventually protect MSI interrupts with the vt-d interrupt
routing tables.
API behaviour for legacy systems using the PIC is preserved
Part of SELFOUR-281
Moving the section and super section objects to the aarch32 mode headers caused the
object orders to be reordered, which breaks verification. This commit undoes this
until it can either be verified or refactored a different way.
* commit '1a1110a0949c76a2d372e2bba6b2526898c51a68':
Modify Kconfig and Makefile for aach32 as sel4_arch libsel4: updates to include aarch32 as sel4_arch
Guarding code with #ifdef's makes even cursor testing of 'does this code compile'
difficult due to code being hidden by the pre-processor. Using config_set in
regular C if statements is performant as the compiler can trivially detect
dead code at compile time, and at -O1 and above will not even link in symbols
referenced by dead code in these blocks, so this will not bloat image size
Guarding code with #ifdef's makes even cursor testing of 'does this code compile'
difficult due to code being hidden by the pre-processor. Using config_set in
regular C if statements is performant as the compiler can trivially detect
dead code at compile time, and at -O1 and above will not even link in symbols
referenced by dead code in these blocks, so this will not bloat image size
This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely,
and changes the return type of seL4_Wait to void (seL4_Wait should be
used for notification objects, and seL4_Recv should be used where
seL4_Wait was used previously for endpoints).
The 'WithMRs' variants of the syscall stubs are known to be broken
on ARM with GCC at -O0. This commit prevents the generation and
usage of these stubs when -O0 is set in the common tool configuration
options.
Due to limitations in specifying Kconfig constraints, and to preserve
the existing meaning of the Kconfig variables, the 'LIB_SEl4_STUBS_USE_IPC_BUFFER_ONLY'
config variable has to be duplicated with two variants, one for use
when the user is free to pick either and one hidden for when selection
has to be forced. Also to prevent the sub options from not appearing
in the libsel4 submenu I had to change libsel4 to be a 'true' menu
instead of a 'menuconfig'
This commit closes SELFOUR-187
There are now separate libs for benchmark, assert, printf, putchar
start/stop:
libs/libsel4benchmark
libs/libsel4assert
libs/libsel4printf
libs/libsel4putchar
libs/libsel4startstop
The primary changes are introducing sel4/sel4.h and removing std* types
plus porting assert and IO code from the kernel to libsel4assert,
libsel4printf, libsel4putchar.
This means the code within libsel4 and the newlibs do not overload any
typical libc entities. Instead the libraries use types like
seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and
assert is seL4_Assert ....
Finally, the only file modified that effects kernel code is
kernel/tools/bitfield_gen.py. It needed to be modified as it generates
files for both kernel and user space. And for user space the generated code
(types_gen.h) needed to use the new types and asserts. The changes should
not change what is generated for the kernel and I did a comparison of
kernel_final.{c|s} before and after my change and the only differences
were time stamps.
Bug: #15 Streamline kernel/libsel4 and remove its libc dependencies
IA32 is 32bit version of the x86 architecture. Whilst only IA32
is supported, much of the code is generic x86. Using a generic
x86 architecture will aid in future 64bit support
Without a name, this struct (and its typedef) comes out as an anonymous type
when imported into Isabelle. This makes it difficult to automate proofs of
functions that use this type.
See also JIRA VER-434
This commit involves the PAE paging itself, refactoring the
vspace code to extra what is common between PAE and 32bit paging,
as well as some renaming to not call the root paging structure
a PD
A C++ compiler will attempt to interpret 'return info' as an invocation of a copy
constructor. Even though the copy constructor is auto-generated (and eventually
completely eliminated due to inlining) and just does obvious member copying it
still results in an intermediate invocation that must take a reference to 'info'.
Because 'info' is a register variable it is not permissable to take a reference
to it. Manually reconstructing a new info from the .words keeps everything as
Plain Old Data
