- renamed an architecture label so that it begins with ARM.
- changed setIRQTrigger so that it takes a boolean value instead of an int.
- Arch_decodeIRQControlInvocation converts the second argument (trigger)
to a boolean immediately.
Add a new invocation which allows an irq handler capability to be
obtained with a specific trigger method (edge or level). Obtaining
this capability modifies the GIC state.
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.
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.
- 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 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.
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.
