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.
It has become clear that the 'packed' GCC attribute affects the
memory semantics of C in a way that the verification tools do not
understand. The bootinfo types are used by kernel boot code (not
currently verified, but covered by binary verification) and should
not use this attribute.
This is a source-compatible but not binary-compatible change.
This provides a common invocation for all architectures for setting their respective
TLS_BASE virtual register. As you frequently want to modify your *own* TLS_BASE, and
doing read/write registers to modify your own registers is tricky to impossible
depending on which register and how they are ordered in seL4_UserContext, this is a
separate invocation.
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.
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.
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 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
This provides documentation for kernel design of the x86 virtualisation, the additional
syscall and object invocations. The ARM design is not fully expanded.
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.
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.
