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.
Whilst it is always correct to invalidate the TLB even if no page was unampped this
provides a small optimization and makes the modeUnmapPage behaviour mirror the general
arch behaviour
This fixes a problem with -O0 SMP builds on ARM visible as kernel
data aborts whenever the idle thread executes.
The idle thread receives no stack pointer. At -O2, this is fine
as the wfi() call is inlined and stack operations in idle_thread
are optimized out. At -O0, the stack operations remain and wfi()
is not inlined, resulting in stack accesses in the idle thread
that cause data aborts.
Forcing -O2 behaviour was deemed the simplest solution for now.
Giving the idle thread a stack would have had larger verification
ramifications for what is now a fairly uncommon use case.
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.
Changes Arch_finaliseCap and Mode_finaliseCap to return the same finaliseCap_ret_t type
as finaliseCap. This allows the Arch and Mode specific functions to define cleanup
information of its capabilities if necessary, just like the generic capabilities can
in finaliseCap.
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.
