mcs: return pointer from `refill_head` and others

A previous commit produced some build errors, since it converted the
`REFILL_HEAD` and `REFILL_TAIL` macros to functions returning
`refill_t`, and the results were used as lvalues. This commit returns
pointers instead, and also converts `REFILL_INDEX` to a function.

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

mcs: change REFILL_HEAD, REFILL_TAIL to functions

SimplExportAndRefine can't handle the level of pointer arithmetic being
performed by `REFILL_INDEX` if it's literally inlined into a function,
however it *can* handle that arithmetic if it's in a separate function.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>

mcs: Don't pass capacity through calls

The capacity does not need to be passed as an argument to
refill_check_budget as all information that it was being used for can be
dertermined from the usage directly.

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

mcs: ensure head refill is sufficient

this is an invariant on the refill queue

Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>

mcs: avoid 'break' in refill_unblock_check

"Interesting" control flow makes translating C to the Haskell kernel
much harder.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

mcs: Compare with time in assigned core

All time for an SC should be relative to its assigned core. Any
operations which may occur on an SC on a remote core must explicitly
refer to that core.

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

mcs: SC time relative to assigned core

The starting and ready times for any SC should be relative to the core
on which the SC is running rather than the current core.

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

Convert license tags to SPDX identifiers

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.

mcs: explicitly use ksCurSC

- in refill_[budget|split]_check.
- This simplifies the code and the proofs.

mcs: make sure blocked threads have spare refills

otherwise they wake up and go back to sleep immediately

mcs: only charge extra budget if it exists

Don't attempt to charge 0 budget.

mcs: avoid rolling back time if acted upon

Otherwise strange things can happen where threads are in the future.

mcs: update refills based on spec

This is a list of fixes that came up while working on the verification
spec for the mcs changes.

- trigger a timer tick if we are unable to split a refill
due to the refill list being full.
- make refill_ordered more useful
- pull the thread out of the scheduler before updating it
- simplify refill logic at verifications request
- Add unused to refill_sum
- Don't refill_split_check if consumed is empty
- sched_control: fix double increment bug
- sched-control: charge before reconfiguring ksCurSC
- Charge round robin threads differently

Sporadic server refill rules do not behave correctly for round robin
threads, instead, change the logic. Round robin threads have 2 refills:
current and next.

mcs: add periodic scheduling

This commit adds periodic scheduling with sporadic servers.