The signal fastpath aims to optimize the
seL4_Signal operation. In this commit, it is
implemented for MCS AARCH64 (SMP and non-SMP).
The fastpath does not include the case where
signaling results in a higher priority thread
being unblocked and made available for
scheduling (on any core). It does not
fastpath the case where the signaled thread
is donated a scheduling context and has its
FPU state saved in the FPU of a core.
Co-authored-by: Shane Kadish <shane.kadish@csiro.au>
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
When determining whether a SC donated from the notification should be
returned, we must ensure not to try and return a NULL SC to a
notification with not bound SC.
This could occur when a passive server performs a NBSendWait/NBSendRecv
with a notification in the receive phase, where the SC for the receiver
was returned in the send phase and the notification has no bound SC.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The current state of MCS seL4 verification makes use of an invariant
that whenever the scheduler action is set to "resume current thread"
the current thread and the current sc are bound together. Since
maybeReturnSchedContext may unbind a thread from a scheduling context,
it should perform a check on whether it is unbinding from the current
thread, and in that case call rescheduleRequired which will (among
other things) change the scheduler action.
Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
If a thread is running on the SchedContext of it's bound notification,
when it next does a blocking recv/wait operation on an ep the SC is
removed. This allows the thread to return to being a passive thread to
receive the next notification or ep message.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
