#
3a22487c |
|
24-Nov-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242) Colloquially known as "invert-fastpath". Update verification efforts on ARM for the following seL4 changes: - scheduling decisions done in possibleSwitchTo are moved to the scheduler - possibleSwitchTo only checks whether the candidate is valid for a fast switch, not its priority, accepting possible candidates immmediately as a switch-to scheduler action - the scheduler checks the candidate against the current thread and against the bitmaps before making a decision - attemptSwitchTo and switchIfRequiredTo are gone - scheduler is now more complicated, and numerous proofs related to it are rewritten from scratch - fast path now checks ready queues via the scheduler bitmaps - L2 scheduler bitmap order reversed for better cache locality Many iterations between the kernel and verification teams were needed to get this right.
|