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.

trivial: remove redundant condition

Remove redundant condition in schedcontext_resume, discovered by
verification.

Avoid adding thread without budget to scheduler

Prior to this change calling yieldTo on an sc with a thread that was not
in the scheduler and had an insufficient/unready head replenishment
would be added incorrectly to the scheduler.

If the thread isn't in the scheduler, use schedcontext_resume to ensure
that it is in the release queue if it has an insufficient/unready head
replenishment, and thus prevent that thread from being added to the
scheduler.

Fix: Move refill_unblock_check into isSchedulable

Don't modify sc parameters unless we know that sc is not in the release
queue.

mcs: Avoid removing the SC of the current thread

If the scheduling context is changed on the currently running thread
this causes issues if the operation triggers a preemption. This change
makes the proofs easier, and also makes sense for the api, as users
wishing to suspend the current thread should just use Suspend.

mcs: Use rescheduleRequired in schedcontext_bind

Schedcontext_bind is currently called in ThreadControl, which
manipulates capabilities which in turn can result in KsSchedulerAction
being deleted. This means that we cannot use possibleSwitchTo in this
function.

This is a stop-gap fix for verification, the long term fix is to split
setting scheduling parameters from ThreadControl, then we can return to
a direct switch, and also do a direct switch for other thread/scheduler
settings like priorities.

mcs: fix behaviour on seL4_SchedContext_YieldTo

When yieldingTo a same prio thread, the same prio thread should run
first, not the current thread. Due to changes to possibleSwitchTo in
master scheduler this code became outdated and the current thread would
be rescheduled immediately.

The desired behaviour is that the thread being yieldedTo should be at
the head of the scheduler queue for its priority, and the current thread
should be just after it.

mcs: Preserve the value of scConsumed on Yield

We use the chargeBudget logic in the kernel on seL4_Yield to free up
the budget available in the head refill, however this
updates scConsumed. Given this is a simulated charge (the thread is
yielding the budget, not actually using it), this is incorrect.

smp: remove excess code in schedContext_donate

- always migrate the TCB (the FPU context could be anywhere)
- don't need to call migrateTCB or rescheduleRequired, this is handled
by calling paths.

smp: remove excess remote call stall in unbindTCB

This isn't required as all code paths into this function have already
stalled the tcb

smp: remove excess code in bindTCB

- we know the tcb does not have an SC at this point
- it may need to migrate if the FPU context is still on the other core.

mcs: add seL4_SchedContext_YieldTo

Implement seL4_SchedContext_YieldTo, which allows users to manipulate
the scheduling queues up to their MCP and can be used for user level
scheduling.

mcs: timeout exceptions

- Add seL4_TCB_SetTimeoutEndpoint
- implement timeout exceptions

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: associate scheduling context + ntfn

This commit allows scheduling contexts to be bound
to notification objects. When a passive server
receives a notification it will receive the scheduling
context from the notification. When the server
blocks the scheduling context is returned.

mcs: update to build on SMP

Before this commit SMP + MCS did not build.

mcs: scheduling context donation over ipc

After this commit, threads blocked on an endpoint can recieve a
scheduling context from the thread that wakes the blocked thread.

mcs: add periodic scheduling

This commit adds periodic scheduling with sporadic servers.

mcs: Add a scheduling context object

This is the first part of the seL4 MCS. This commit:

* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.