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.
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.
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
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 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