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>

debug: create debug_tcb_t struct

Special debug variables that were previously stored at the end of the
tcb_t struct often cause the struct to get too large for the power-of-2
sized untyped object definition. This change moves these variables into
a new structure named debug_tcb_t that is located between the TCB CNode
and the tcb_t struct within a tcb kernel object. Because tcb_t needs to
be stored on a power-of-2 aligned boundary and the TCB CNode only
contains < 5 slots, there is easily > 512 bytes of unused data in every
tcb object. The kernel verification needs to be sure that objects don't
overlap in memory and so this space can't be easily used in a release
build at the moment, but for debug configurations using it shouldn't be
an issue.

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

trivial: Fix typo in error message

The commit is based on PR #185 created by laokz.

Co-authored-by: laokz <laokz@foxmail.com>

Signed-off-by: Yanyan Shen <yshen@cog.systems>

Remove references to kernelBase

kernelBase was used inconsistently between different architectures to
refer to the either of the first kernel address or the first address of
the mappings of the kernel ELF region specifically.

These have been replaced with more consistent use of constants
explicitly describing which region is being referenced.

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

reflect function split in thread_control_flag

The thread_control_flag enum which defines which arguments should be
used to reconfigure the TCB should also be split into two sets of flags
as they are now applied to two different functions.

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

mcs: bind SC last in ThreadControlSched

This changes the order in MCS of ThreadControlSched:

1. Bind the fault handler
2. Set priorities
3. Bind or unbind scheduling contexts

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

Split ThreadControl into two functions

This ensures that verification are not required to prove problematic
combinations of updates to a TCB that aren't even permitted by the API.

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

mcs: allow replyGrant for fault handlers

The MCS kernel so far insisted on full grant rights for fault handler
caps, but replyGrant is sufficient and consistent with the default
kernel config.

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.

Fix comps between negatives and unsigned vars

In circumstances where values are negative and
compared to unsigned variables, clang will
error saying that this is always true. Include
early break conditions that check for this

kernel: attempt direct switch on set prio

Prior to this commit the kernel would always trigger a full reschedule
on setPriority. This change allows the kernel to attempt a direct
switch, avoiding invoking the scheduler.

- Move location of setPriority call to after any cap deletion
This makes the proof easier as setPriority now changes
ksSchedulerAction, which is required to be ResumeCurrentThread or
ChooseNewThread by the cap delete functions.
- Update to attempt direct switch on set prio.

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: allow only unbound SC/TCB in SetSchedParams

This removes some special-casing from the proof.

trivial: sync comment with code

mcs: Swap TCB cap install order in ThreadControl

Installing the endpoint caps before the CSpace/VSpace roots is easier
for verification, because deleting endpoint caps is always well-behaved,
but CNode cap deletion can be complex.

mcs: timeout exceptions

- Add seL4_TCB_SetTimeoutEndpoint
- implement timeout exceptions

mcs: install fault endpoint into tcb cnode

- seL4_TCB_Configure no longer takes a fault endpoint.
- seL4_TCB_SetSpace takes a cap in the callers cspace for the
fault endpoint, not the target tcbs.
- seL4_TCB_SetSchedParams now also takes a fault endpoint as above.

This change installs the fault endpoint cap into the tcb cnode
first validating it.

This means either of the functions that set it will now return an error
if the cap is not either a null cap or an endpoint with send and
grant rights.

Significantly, the cap passed to the function should be in the callers
cspace, not the target tcbs.

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: 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: tickless scheduler implementation

This changes the budget/remaining fields in scheduling contexts
to contain timer ticks, not number of abstract sel4ticks.

seL4_SchedControl_Configure now takes microseconds, not ticks.

This commit is plat-independant - the platform and arch specific
timer code follows in later commits.

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.

Remove platform IPC buffer register.

This removes the assumption that each platform sotres the IPC buffer
address in a platform-specific register. The IPC buffer address is
instead stored in a thread-local variable in libsel4 which must be
initialised by the runtime.

Remove symlinked libsel4 files from include dir

These files can be included normally using libsel4 include paths. This
removes situations where the same file is available under different
include paths due to symlinking into different directory structures.

style: set min-conditional-indent to 0

Given we use braces all the time conditional indents do not make code
cleaner.

style: consistently attach return type

Add attach-return-type to astyle

style: consistently align pointer with name

Run astyle with align-pointer=name

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.

Remove unused variable

SELFOUR-823: Provide TCB invocation for setting TLS_BASE

This provides a common invocation for all architectures for setting their respective
TLS_BASE virtual register. As you frequently want to modify your *own* TLS_BASE, and
doing read/write registers to modify your own registers is tricky to impossible
depending on which register and how they are ordered in seL4_UserContext, this is a
separate invocation.

trivial: fix seL4_TCB_SetSchedParams error msgs

SELFOUR-331: add seL4_TCB_SetSchedParams

This allows the prio and mcp to be set in one system call.

SELFOUR-1016: Require auth cap to set prio/mcp

This fixes confused deputy problem when setting priorities/mcps.

Avoid loop in debug tcb list

Assigning to `tcbDebugNext` after assigning to `ksDebugTCBs` results in the first item
appended to the list having self->next==self, resulting in a loop. Changing the order
of the assignments fixes this.

Abstractly declare a threads registers have changed

This removes an #ifdef for x86-64 that was in generic code by declaring the generic
mechanism that is being used as an Arch_ function

Invert priority order of scheduler bitmap

Provides better cache performance for high priority threads

SMP: add top level migrateTCB

On the MCS kernel, Arch_migrateTCB is called in multiple places.
This commit moves the common code that is required when migrating a TCB
to a top level function to reduce boiler plate.

Debug: fix ksDebugTCBs for SMP

There is a separate list of tcbs per core.

- migrate between debug lists when setting affinity
- use the correct core when removing

SMP: Introduce ENABLE_SMP_SUPPORT

- Make it more readable and less confusing compared to the 'CONFIG_MAX_NUM_NODES > 1' check

SELFOUR-291 Reschedule when changing own registers

Previously if you wrote to TCB of the current thread and
changed the TLS_BASE this would not immediately take
affect, as the kernel only updates this register in
Arch_switchToThread. This change forces Arch_switchToThread
to get called, even if we would switch back to the original
thread.

SELFOUR-30 Reschedule when changing own IPC buffer

Previously if you invoked the TCB of the current thread and
changed the IPC buffer frame this would not immediately take
affect, as the kernels view of the current IPC buffer is
updated in Arch_switchToThread. This change forces Arch_switchToThread
to get called, even if we would switch back to the original
thread.

Check for CONFIG_ variables being 'defined' instead of 'true'

This is to conform with existing style of checking configuration options

SELFOUR-880: add seL4_DebugDumpScheduler

- when CONFIG_DEBUG is enabled, track all threads
- when CONFIG_PRINTING is enabled, provide seL4_DebugDumpScheduler which
allows the user to dump the state of the kernel scheduler.

Abstract setting ipc buffer register into arch fn

Change hasVCPU to generic archInfo boolean in public interfaces

The Arch_hasVCPU function instead of cheaking for whether a thread has a VCPU was
specifically checking for whether a thread on aarch32 had a VCPU, as that was the
condition needed to be passed into sanitiseRegister. This made the implementation
on x86 extremely confusing as Arch_hasVCPU was implemented to return false due to
there being no need for sanitiseRegister on x86 to know whether there was a vcpu.

This commit changes hasVCPU variables to be an abstract archInfo boolean that can
be used arbitrarily by an architecture. Arch_hasVCPU function was also changed to
become Arch_getSanitiseRegisterInfo whose result only passed to sanitiseRegister.

Refactor sanitiseRegister to take a bool rather than a (tcb_t *).

This involves adding a function to determine if a tcb has a vcpu, and
makes verification a lot easier for arm-hyp.

SELFOUR-836: Hardware debug API functions should take tcb_t and not arch_tcb_t

Touches files all throughout x86 (32 and 64) and ARM.

Pass tcb_t to sanitiseRegister instead of arch_tcb_t

SMP: Move/rename migrateTCB() arch tcb.c

ARM/SMP: Prepare for ARM SMP adding stubs

Currently building ARM/SMP is broken. This commit:
1- Makes it possible to build ARM/SMP with stubs. Run-time SMP for ARM
DOES NOT WORK.
2- Can be a reference for future SMP targets to follow in order to
layout/add the minimal required files and functions needed to support SMP.
3- Builds for Sabre only. In order to support other platforms, ipi
interrupt ID should be defined in machine.h

arm: SELFOUR-781: Only allow threads with VCPU to run outside user mode

Previously any thread could be set to run in any mode (except HYP mode).
Whilst this causes no security issues for the kernel, different execution
modes in ARM have different banked registers. These registers are not
currently saved and restored allowing for threads to manipulate registers
that will be seen (or potentially are being actively used) by other threads.

Saving and restoring these banked registers for all threads is a performance
cost (even if only done for the actual mode the thread runs in) for no real
benefit, as there is no clear reason to run a thread in other modes if you
do not have a vcpu. Therefore this commit restricts being in modes other than
user to threads that have a vcpu. When multiple VCPUs are properly supported
the switching of VCPUs will then save/restore these banked registers.

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

SELFOUR-553: Support alternate IPC buffer locations without globals frame

This commit adds support for using the ThreadID registers of the ARM MPCore
platforms for storing the address of the IPC buffer instead of the globals
frame. The choice of using the user readable/writeable ThreadID register
is chosen, even though it means the user cannot use it for its own
purposes, as it leaves room in the future for doing TLS support in the
user read only register, where compilers expect it.

Move migration logic to own function

This makes it easier to port to the RT branch, where
migration can happen in several different places.

Revert SELFOUR-242

This reverts commits
3aee0ab7b3ae5ff5294192526fb00823b49048b5
6b6b965528d16c1e4c946fb920fb95060f84424f
a1421832acd19ed5ede71640af82b982708207c2

SELFOUR-242: invert bitfield scheduler & optimise

This commit does the following:

* invert the bit field scheduler for better cache performance for high priority threads
* peeks into the bitfield scheduler to allow fastpath to be leveraged when IPC occurs from lo --> hi priority threads if correct

x64: Access core local state correctly

Store remote FPU state

trivial: change remoteTCBStall to take tcb

Instead of cap_t. This allows the function to be used from other
functions that have the tcb pointer and not the cap.

Extend IPI for two function parameters

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

[STYLE_FIX]

SELFOUR-287: 32-bit vt-x implementation

This is an implementation of vt-x for x86 kernels running in
ia32 mode.

[STYLE_FIX]

add basic api for setting affinity

x64: force return via IRQ path so that register writes have an affect

SELFOUR-632: implement cores non-architecture dependent structres

SELFOUR-499: X86, ARM: Add userspace invocations for hardware debugging

This commit implements the body of SELFOUR-499. The API exposes the x86 DR0-7
and ARM coprocessor 14 features to userspace by virtualizing them as context-
switched registers in the TCB. Implemented as TCB invocations. This feature is
only built when CONFIG_HARDWARE_DEBUG_API is selected.

* Add low-level support routines for setting, unsetting, getting, enabling
and disabling breakpoints.
* Add support for single-stepping as well.
^ Single-stepping is not supported on ARMv6 since the hardware
doesn't have support.
^ ARM implements single-stepping as instruction breakpoints
configured to fault on every instruction -- this is achieved through
the "mismatch" mode, which is only supported from ARMv7 onwards.
* Also support explicit software break requests, a la "BKPT" and "INT $3".

* New invocations:
* seL4_TCB_SetBreakpoint().
* seL4_TCB_GetBreakpoint().
* seL4_TCB_UnsetBreakpoint().
* seL4_TCB_ConfigureSingleStepping().
* New constants:
^ Event types:
^ seL4_InstructionBreakpoint.
^ seL4_DataBreakpoint.
^ seL4_SoftwareBreakRequest.
^ Access types:
^ seL4_BreakOnRead.
^ seL4_BreakOnWrite.
^ seL4_BreakOnReadWrite.
^ Exports:
^ seL4_NumHWBreakpoints.
^ seL4_NumExclusiveBreakpoints.
^ seL4_NumExclusiveWatchpoints.
^ seL4_NumDualFunctionMonitors.
^ seL4_FirstBreakpoint.
^ seL4_FirstWatchpoint.
^ seL4_FirstDualFunctionMonitor.

See documentation in the seL4 API manual.

[STYLE_FIX]

SELFOUR-276: remove some redundant checks

Existing thread priorities and MCPs are already guaranteed to be less than
seL4_MaxPrio.

SELFOUR-276: Add MCP field to threads.

Where MCP = Maximum Controlled Priority

This commit adds:

* seL4_TCB_SetMCPriority

and changes the arguments to

* seL4_TCB_Configure

As of this commit, a thread cannot create or set a threads
priority (including itself) above its mcp. Previously the kernel
did this check against a threads priority, which prevented a thread
from setting it's own priority down and then up again.

SELFOUR-566: Decouble seL4_DebugNameThread from CONFIG_PRINTING

trivial: remove duplicated setMRs_syscall_error

SELFOUR-511: remove -Wdeclaration-after-statement

And change a line of code for verification to
test if it works.

Correct separation of printing and debug builds

Fixes some build issues with 541289a32603cee8242b5360b05e8f0c52795433
as well as further allowing debugging (via the capdl interface) to
happen when printing is turned off.

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

unsigned int -> word_t

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

Using bitfields to track for which priorities there exist non-empty ready queues.

Background
seL4 organizes threads into ready queues, of which there is one for each
domain, for each priority level. The ready queue for a given
domain/priority combination can be found by indexing the array
`ksReadyQueues` with "domain*num_priorities + priority".

Current scheduler implementation
To find the non-empty ready queue with the maximum priority for the current domain,
seL4 iterates through `ksReadyQueues`, starting with the element
corresponding to the current domain and maximum possible priority, and
decrementing the priority until a non-empty queue is found. This is
problematic in cases where the only ready threads have low priorities,
as iterating through many elements of an array effectively flushes the
cache.

Changes in this patch
This patch replaces the iteration with a lookup into a table of
bitfields per domain. Using bitfields allows the kernel to determine the
highest priority level with a non-empty ready queue for the current
domain by counting the leading zeroes in bitfields. This removes the
negative cache effects of iterating through an array.

Implementation details
For each domain, a multilevel table of bitfields is maintained which
stores the priority levels within that domain for which there exist
ready threads. On a 32-bit architecture, the top level of the table is a 32-bit bitfield where if
the ith bit is set, there is at least 1 priority level in
[i*32..i*32+31] with a non-empty ready queue. The positions of bits in
this bitfield are used as indices into the second level table, which is
an array of 32-bit bitfields. The ith bit of the jth bitfield in this
array set to 1, indicates that priority level j*32+i has a non-empty
ready queue.

AEP -> Notification: deprecate old API syscalls, functions and constants that refer to AEP's and introduce new ones that refer to Notifications

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

generate warnings for incorrect format strings for kprintf, bring stdint.h
inline for x86 and arm and fix some format strings as a consequence

Ghost assertions for cteDeleteOne.

Add ability to set a human readable thread name when running kernel in debug mode

trivial: Print domain values as unsigned integers in user errors.

With the comparison preceding this being done on unsigned integers, this avoids
confusing error messages like '-2147482648 >= 1'.

Release snapshot