These files can be included normally using libsel4 include paths. This
removes situations where the same file is available under different
include paths due to symlinking into different directory structures.
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.
Revocability of a cap, with respect to its parent, is a general property on caps and
makes sense to be abstracted. This allows for the addition of an arch case without
further complicating the cteInsert function itself.
A TCB object has two objects inside it, the cnode object and the 'actual tcb object'.
For simplicity of verification we would like the tcb_t portion of the object to also
be size aligned instead of just just being offset by the size of the cnode.
This definition is used as the size of the cnode portion of the TCB object (and not the tcb_t)
portion and so this provides a much less confusing name.
Allows architectures to define their own operations for post deletion of capabilities.
The Arch_ variants could be extended to Mode_ if desired in the future, but there is
no need to do this until it is necessary.
Moves the explicit call of `deletedIRQHandler` in `emptySlot` into a new
`postCapDeleted` function that is a generic function to call after a capability
has been deleted.
Currently `deletedCap` only implementes the IRQ case.
Changes finaliseCap to return a generic definition of cleanup information that
needs to be done, instead of just encoding an IRQ number. The post deletion information
is encoded as a `cap_t` due to the capability type already being a union of all
the possible information. Aside from providing a properly generic mechanism the motivation
is to support a similar cleanup phase for I/O ports in the future.
In f6d367e8df virtual addresses were changed from 48
bits to 49 bits, but this does not seem necessary and the commit does not have enough
detail to justify the change. As such it is being changed back to 48 bits in this
commit, which is far less confusing and results on the bitfield generated functions
switching on bit 47 to determine sign extension (instead of bit 48), which matches
what the hardware description says should be done.
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.
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
Zombie caps perform bit packing that relied on the log2(wordBits), which was being
hard coded to 5. Whilst 5 is the correct value on 32-bit platforms, it is incorrect
on 64-bit ones. This changes the previously hardcoded 5 to be the, already existing,
wordRadix definition.
- 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.
Prior to this commit virtual addresses in the bitfield were considered
to be 48-bits, with sign extension to 64-bits. This meant that we were
actually sign extended bit number 47. Whilst this gives correct cannonical
addresses it prevents a portion of the address space from being used.
This commit changes the bitfield to use 49-bit virtual addresses, so that
after the bit 48 is used for sign extension there is still 48-bits of
usable address.
This looks like we're just swapping the positions of capEPBadge and capEPPtr,
but it turns out that the bitwise op being performed on capEPPtr to set the
high bits were part of the data dependency critical path, so this actually
does improve the speed by moving the bitwise op to capEPBadge (albeit it's
now an AND instead of an OR)
I initially set the field size to 32 bits, but it turns out that causes gcc
to emit an instruction (mov r32, r32) that causes the instruction decoder
to switch to the legacy decode path for the rest of the fast path for some
reason.
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.
benchmark.h requires a definition of KS_LOG_PPTR, but its previous
placement in machine.h resulted in a circular include. This commit
factors out KS_LOG_PPTR and related definitions to a separate header,
creates the corresponding header for x86, and prevents circular
includes in the x86 builds
Removes the recycle operation and adds an operation
to cancel any badged sends on and endpoint. Calling
Revoke + CancelBadgedSend is equivalent to Recycle
on a badged endpoint
Change to the order of operations and timing behaviour of
invokeUntyped_Retype. The Retype operation now zeroes the
entire range of the Untyped cap (if it is being used for
the first time) before installing any objects. This avoids
the need for long-running initialisation of large objects,
whose initial contents are always zero. The initial zeroing
phase is preemptible, and may take multiple timeslices to
complete.
This will update TCB invocations to consider multicore environment, this may include:
- adds the affinity invocation to transfer TCB between different cores and update TCB structure for core ID
- checking the thread/core state before performing TCB operation, e.g. deleting the runnable TCB, etc
