#
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.
|
#
48b3a8b4 |
|
04-Oct-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
update object and field widths for x64, and remove some magic numbers In X64 update the following to match the C kernel: - TCB size-bits (11). - Endpoint size-bits (4). - Guard bits (58). - Message registers. For all architectures, replace magic numbers with defined constants in specifications, and as far as possible in proofs: - tcb_bits in abstract spec. - tcbBlockSizeBits, cteSizeBits, ntfnSizeBits, epSizeBits in Haskell spec, Haskell and C refinement proofs.
|