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.
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.
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.
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.
Regardless of the number of PT levels SEL4_MAPPING_LOOKUP_NO_PT always represents the
bits at which we don't have a PT as with more PT levels the number of bits a PT translates
does not change.
Although the C kernel examines (and may modify) some bits of the message
info register, all remaining bits are treated as user data, which the
kernel passes through IPC unmodified.
The seL4_MessageInfo register describes the message info register. The
kernel examines fields `length`, `extraCaps` and `capsUnwrapped`, while
the `label` field represents bits available to the user. However, in
reality, the user may also use any padding bits for user data, since the
kernel also passes these through IPC unmodified.
For verification, we would like to phrase specifications in terms of the
bitfield definition, and so we would like the `label` field to
incorporate all of the bits which the kernel treats as user data.
This commit therefore extends the `label` field across the bits which
were previously marked as padding.
The alignment of the tcb_t portion of a TCB object is going to be increased, this will
cause the total TCB size to overflow in some cases. This updates the definition of
seL4_TCBBits such that TCBs will be large enough after the alignment change.
CPPFile is a much more robust version of GenCPP command. We drop the `extra_cflags`
as the CPPFile command uses regular cmake compilation and will use the include
directories added by `include_directories`, which includes all the directories from
`extra_cflags`
include_directories makes these directories directly available to all compilation that
happens, without needing to provide additional target link directories. This is the
first step to removing the `extra_cflags` variable
Provides a syscall interface for reading and writing arbitrary MSR values. This is
being introduced as an alternative to the DebugRun, as the main purpose of debug run
is for modifying the performance monitoring events via read/write MSR.
The GetStatusBits invocation is only implemented on ia32. Adding the condition to the
XML list prevents the invocation from being in the list of invocations on x86_64, when
it has no implementation.
Placing lists directly in the generater expression means that this string, despite having
semicolons in it, is not actually a list, as it has an expression (the generator expression)
spanning multiple lists. This leads to confusion during argument processing and expansion
Adds a named constant of the IPC buffer size bits that can be used when checking the
size/alignment of an IPC buffer. This constant has a compile time assertion to ensure
it corresponds to the actual IPC buffer
This unifies the badge size of endpoints and notifications on 64-bit platforms to a
consistent 64-bits, and also changes the libsel4 definitions to match for both.
The maximum guard size was unnecessarily restricted to 18 bits as it is on 32-bit
platforms. This change increases it to the current maximum possible of 58 bits.
The 58-bit limitation exists due to the need to encode a guard+guardsize into a
single word for cnode invocations.
The definitions of guard and badge sizes is going to be changed for 64-bit platforms,
this change provides an easy way of providing different definitions
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.
The purpose of renaming this type is to match the style of the other shared types in libsel4.
Previously its name was fine as this was a private kernel type.
This data structure is meant to be the user visible format of the data for a cnode_cap,
yet it is defined in a kernel only bitfield file. Moving it to libsel4 opens up the
possibility of consolidating the definitions in libsel4
The Zynq UltraScale+ MPSoC (PLAT zynqmp) is a Multi-Processor SOC
made by Xilinx that has a quad-core Cortex-A53, a dual-core Cortex-R5
and an FPGA.
This adds 32-bit, single-core support on the the Cortex-A53 cluster.
This provides documentation for kernel design of the x86 virtualisation, the additional
syscall and object invocations. The ARM design is not fully expanded.
Fixes an inconsistency between manual_label for the x86 AsidPool_Assign invocation
and its reference in the manual. This makes the x86 align with the ARM name.
Nested structs with attributes are not understandable by the C parser. This change simply
moves the nested definitions into the global namespace (with suitable names).
The IOMMU implementation is not going to be verified at the moment, and so the code for
it needs to be hidden from verification, which we do by #ifdef'ing it out if the IOMMU
is not enabled. As a result the IOMMU configuration depends on a non verification target
Changing the register used for the IPC buffer is useful as the standard TLS model for
aarch64 is to use tpidr_el0 for the thread pointer, which we are presently using
for the IPC buffer. This therefore paves the way for implementing proper TLS support
on aarch64.
Since we are not using tpidr_el0 for the IPC buffer we need to save/restore (or at
least clear) this register on thread switch to prevent it being a user channel. Saving
and restoring of it is achieved by ensuring CONFIG_IPC_BUF_TPIDRURW is not set, which
as we are no longer using this strategy this will be the case. To that end as aarch64
only has one IPC buffer strategy this commit makes the choice of IPC buffer strategy
dependeont on aarch32.
This commit implements lazy FP save/restore mechanism, required for user threads
when they use the FPU. The following caveats take place:
* Only support synchronous exceptions. No support for asynchronous ones.
* VFP opcodes are used instead of normal instructions to discard compiler warnings/errors.
* Support is limited to specific ARM subarchitectures we support and tested this commit on.
* Disable the FPU by default if users are not using it to avoid channels.
* FPU support is not verified yet.
* Will not work properly if using a VM that's running besides other VMs/threads that are using the FPU.
Previously anything in an autoref block was assumed to reference
a section, which isn't true. Change 'sec' to 'label' and move the
'sec' prefix into the label itself.
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.
Methods with no output params return an error. Previously each such
method had a line of documentation in its interface definition
explaining this. This commit removes this. The documentation is
for such cases is generated implicitly.
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.
- 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.
Provides a configuration option for enabling HDCR.TD* traps, or saving and loading debug
state on VCPU switches. Currently verification only plans to support the trap setting.
As this option complicates all of the #ifdef's related to debug registers even further,
abstractions for enabling/disabling each individual piece of the debug code for different
configuration options are also implemented.
Part of these refactored #ifdef guards was to remove the guards completely from libsel4
around the definitions of the number of breakpoints and watchpoints.
This patch disables the debug register state save and restore on ARM-hyp,
such that Guest VMs can now interfere with one another and trigger
one another for certain limited scenarios. This will be undone later on.
As things are now, the Guest VMs can modify the debug registers at will
from non-secure PL1, and the kernel does nothing to ensure that guest VM
debug coprocessor registers are preserved.
This is a preliminary patch that simply hooks into vcpu_save and saves the
CPU's debug coprocessor registers when saving VCPU state.
For restoring the debug registers on switching to a VCPU, we just re-use
restore_user_debug_context, which is already called in restore_user_context.
(Restore_user_context is called by c_handle_vcpu_fault()). Specifically,
we modify the used_breakpoints_bf so that restore_user_debug_context()
will always pop all the debug context.
This patch only covers the breakpoint and watchpoint registers,
and it doesn't cover the entire debug coprocessor, which is another
conversation.
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.
This provides a future proof interface for extending the bootinfo region with additional
kinds of optional architecture and platform specific information. The basic idea is to
report the size of a region directly following the bootinfo frame, which is made up of
a series of 'chunks'. Each chunk has an identifier (describing what it is) and a length,
allowing unknown chunks to be skipped in favor of examining the remaining of the chunks.
