mcs: add tcb argument to reply_unlink

reply_unlink takes a reply and remove the link between that reply
and its tcb. This link always exists at the call site and the tcb
information is always avaialble, or can be made available.

This commit adds this tcb as an extra argument to aid varification.

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>

mcs: Return bound notification SC before ep recv

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>

mcs: prevent recursion on timeout faults

The SC of a thread that has timed-out cannot be donated to the time-out
fault handler, preventing recursion on timeout faults.
This prevents that donation from occuring but will leave
the fault handler 'running' but without any SC.

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

Enabled IPC debug features under new config

Introduced a new config flag to enable
userError format strings to be written to the IPC buffer.
Another config bool has been introduced to toggle
printing the error out and this can also be set at runtime.

Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>

userError string written to IPC buffer

The format string in userError is now written to
the IPC buffer for debugging purposes.
This requires an snprintf which reuses vprintf with
a new structure for handling how output is done.

Signed-off-by: Saer Debel <saer.debel@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: in cancelIPC, clear the tcbFault

A fault message is an IPC. Threads which have faulted can be inactive,
blocked on send, or blocked on reply. Always clear tcbFault when
cancelling IPC to make sure restarted threads are not in a fault state.

mcs: Set threads to inactive in cancelBadgedSends

This is the same reasoning as for cancelAllIPC

mcs: Set thread to inactive if no reply is present

If we're in a scenario where do_call or fault is set, but there is no
reply, the calling/faulting thread needs to be set to inactive to
prevent it reentering the scheduler in a bad state. If the reply is set,
then the calling/faulting thread is set to blocked on reply correctly.

mcs: Set threads to inactive in cancelAllIPC

If a thread's fault endpoint has been deleted, such that cancelAllIPC is
called on that endpoint, set the thread state to inactive. This prevents
threads with faults from entering the run queue and makes the
behaviour consistent with threads faulting without a fault handler set.

This came up as verification now need the invariant that threads in the
runqueue have no faulted, an invariant not required before MCS.
Previously the behaviour was not broken, as threads would just refault
and be made inactive at that point.

mcs: Use cancelIPC instead of reply_clear

- reply_clear only does half the job
- remove reply_clear no longer used

mcs: Refactor replies to solve revoke problems

Before this change, we set the replyObject in the thread state on recv
with no back pointer such that stray pointers would be left in the
thread state when a reply object was completed.

The new semantics are clearer and fix this problem by doing the
following:

- tcb->tcbReply is removed and the thread state field is always used,
this was unneccessary duplication previously
- the thread state value is set to the reply object only when the thread
is in BlockedOnReply or BlockedOnRecv
- the reply contains a back pointer, replyTCB, which points to that
thread
- if a thread has its reply removed, it must be set to
ThreadState_Inactive.
- deletion is easy in the blockedOnRecv case, we just unlink the reply
and the tcb.
- deletion is complicated for blockedOnReply. If we are deleing a tcb,
we remove the actual reply object and the call chain is broken. If we
are deleting a reply, we maintain the call chain by moving the tcb to
the next reply.
- we refactor the reply object interface to solve the above.
* reply_clear: removes the reply from any connections (tcb, sc)
* reply_unlink: just unlinks the tcb and reply, and sets the thread
state to inactive
* reply_remove: removes the reply from the call chain
* reply_remove_tcb: removes the exact reply that a tcb is bound to,
as we are removing that tcb. Breaks the call chain.

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: order EP and NTFN queues

Previously IPC signal queues were FIFO, as of this change they are
ordered by priority (FIFO for same prio threads).

mcs: add periodic scheduling

This commit adds periodic scheduling with sporadic servers.

style: consistently attach return type

Add attach-return-type to astyle

style: consistently align pointer with name

Run astyle with align-pointer=name

style: correct parenthesis padding

Use astyle's unpad-paren to unpad all parentheses that are not included
by pad-header, pad-oper, and pad-comma.

SELFOUR-6: Add GrantReply to the rights system.

GrantReply is a new access right added to endpoint capabilities, which
allows seL4_Call to be used on those capabilities (specifically, it
allows reply caps *only* to be granted across endpoints).

Prior to the addition of GrantReply, endpoint capabilities required the
Grant access right, which allowed any arbitrary capabilitiy to be
transferred over an endpoint. Using GrantReply, systems can now be
constructed where threads using seL4_Call over an endpoint do not need to be in the same
security subsystem.

ksSchedulerAction contains candidate thread instead of target thread

Instead of switching to the thread contained in `ksSchedulerAction` on a `schedule` we
instead decide between the 'candidate' contained in `ksSchedulerAction`, the current thread
or potentially neither if the candidate is deemed invalid and the current thread is blocked.

A consequence of this change is that it is no longer meaningful to have a distinction between
`switchIfRequiredTo` and `attemptSwitchTo`. Now both these cases simply identify a candidate,
which may or may not be picked in `schedule`. Part of the distinction of `switchIfRequiredTo`
was to not avoid switching if possible when performing notifications. This is now handled by
prefering the current thread over the candidate if the current thread has not blocked.

This change is largely semantic preserving overall, with the exception of non-blocking
synchronous sends now acting like notifications and also preferring to resume running the
current thread.

The motivation for this change was to make it much easier for verification to show
correspondence between the fastpath changes introduced in the previous commit and the
slowpath scheduler.

SELFOUR-413: refactor libsel4 fault API

This is a *breaking API change*

This commit:

* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
the user calling seL4_SetTag() first (seL4_MessageInfo is passed
in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes

Generated bitfield proofs: use hrs_mem_update.

This is a technical change to the proof mode of the bitfield
generator included in the seL4 source.

The postconditions of the generated specifications of the
*_ptr_set and *_ptr_new functions now describe the entire new
heap via (new_heap = hrs_mem_update (...) old_heap).
Previously they described the contents of various projections
of the heap, which is less precise.

SELFOUR-635: support for TCB operations
This will update TCB invocations to consider multicore environment, this may include:
- adds the affinity invocation to transfer TCB between different cores and update TCB structure for core ID
- checking the thread/core state before performing TCB operation, e.g. deleting the runnable TCB, etc

SELFOUR-56: Remove diminish rights from IPC

Diminish rights were to prevent a user from sending a writeable
cap over a read only endpoint. It turns out this 'security' can
be worked around without difficulty (by putting caps in a cnode
and sending the cnode) making the current diminish rights
implementation functionally useless.

Removing diminish rights has the benefit of simplifying all the
IPC paths.

SELFOUR-114: remove duplication of seL4_MessageInfo_t, adjust naming to avoid cparser mangling

unsigned int -> word_t

SELFOUR-279: rename Wait -> Recv, add wrappers for seL4_Poll and seL4_Wait for notification objects.

This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely,
and changes the return type of seL4_Wait to void (seL4_Wait should be
used for notification objects, and seL4_Recv should be used where
seL4_Wait was used previously for endpoints).

Replaced "async endpoint" with "notification" in comments and error messages

SELFOUR-317: rename async endpoint to notification object, and other
fallout.

Add seL4_NBWait: non blocking wait for notifications and endpoints.

Introduce 'Notification Binding': a new feature which allows a tcb to be bound to a single asynchronous endpoint.

Ghost assertions for cteDeleteOne.

Release snapshot