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: Don't invoke SC on first phase of syscall

Don't allow SC cap to be invoked on first phase of syscall as if the
operation is SchedContextYieldTo then this could result in the caller
being placed in the scheduler queue and not able to perform the second
phase.

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

mcs: Don't invoke domain on first phase of syscall

Don't allow a domain capability to be invoked on the first phase of a
two phase syscall. Performing this action can lead to a thread being
enqueued in a scheduler in the first phase and accepting IPC in the
second.

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

mcs: SCs in the same region have the same size

Although it is true that any SC that refers to the same location in
memory will have the same size, it is difficult to prove. This
explicitly checks to remove the burden of proof.

This approach is already used when determining whether two CNodes refer
to the same region.

Signed-off-by: Curtis Millar <curtis.millar@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>

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.

arm,SMP: Refactor irq_t structure for smp

Explicitly create a struct definition for irq_t on SMP Arm
configurations. This makes it a lot harder to mistakenly use the wrong
irq encoding when moving an irq between a cnode index and hardware irq
number / core. A couple areas where this was being handled incorrectly
was fixed as part of the refactor. When performing an ipi for masking
PPI interrupts, the idx encoding is used as it fits into a single word.

mcs: Avoid charging invalid scheduling contexts

ChargeBudget can be called after a preemption, but the preemption may
have deleted the scheduling context. Do not charge scheduling contexts
that have been deleted (check scRefillMax).

mcs: Introduce firstPhase flag to invocations

Some invocations contain two phases, and certain operations cannot be
allowed to run in the first phase as it could effect the currently
running thread and result in an invalid system state for the second
phase. This change filters those invocations, preventing them from being
used in the first phase of a two-phase, blocking system call.

mcs: break call chain in reply_remove_tcb

Rather than preserving the chain break it completely. This changes the
semantics such that if a reply is removed in the middle of a call
chain, a donated scheduling context cannot return to the original
caller.

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: 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: configurable scheduling context size

This allows users to define custom amounts of refills without
increasing the scheduling context size system wide.

also add libsel4 functions for refill size

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: 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 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.

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

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.

Change shift target from '1' to '1ul' in finaliseCap

Literal '1' defaults to have type int, so when checking for shift
overflows in verification they are guarded with a size check of 2^31 - 1.

This change makes it so that it is now possible to shift by higher
radices than 31 on architectures which support it.

make TCB offset parametric in verification annotation

Allow Arch_finaliseCap to return cleanup information

Changes Arch_finaliseCap and Mode_finaliseCap to return the same finaliseCap_ret_t type
as finaliseCap. This allows the Arch and Mode specific functions to define cleanup
information of its capabilities if necessary, just like the generic capabilities can
in finaliseCap.

Generalise finaliseCap to more than just IRQs

Changes finaliseCap to return a generic definition of cleanup information that
needs to be done, instead of just encoding an IRQ number. The post deletion information
is encoded as a `cap_t` due to the capability type already being a union of all
the possible information. Aside from providing a properly generic mechanism the motivation
is to support a similar cleanup phase for I/O ports in the future.

Rename cnode_capdata to seL4_CNode_CapData

The purpose of renaming this type is to match the style of the other shared types in libsel4.
Previously its name was fine as this was a private kernel type.

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.

arm: Pass 'call' down to invokeVCPUReadReg

invokeVCPUReadReg should not be setting message registers for the return message unless
the user performed a call. In doing so we must refactor the call to readVCPUReg to
outside the introduced `if` condition since, as it performs machine operations, it
should always happen

SELFOUR-567: use seL4_CapRights_t from libsel4

This change

* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4

Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.

Remove recycle

Removes the recycle operation and adds an operation
to cancel any badged sends on and endpoint. Calling
Revoke + CancelBadgedSend is equivalent to Recycle
on a badged endpoint

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.

SELFOUR-444: Preemptible zeroing for retype.

Change to the order of operations and timing behaviour of
invokeUntyped_Retype. The Retype operation now zeroes the
entire range of the Untyped cap (if it is being used for
the first time) before installing any objects. This avoids
the need for long-running initialisation of large objects,
whose initial contents are always zero. The initial zeroing
phase is preemptible, and may take multiple timeslices to
complete.

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-287: 32-bit vt-x implementation

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

add basic api for setting affinity

SELFOUR-632: implement cores non-architecture dependent structres

SELFOUR-421: minor changes for c-refine

SELFOUR-421 Introduce explicit device frames and untypeds

Kernel objects cannot be created from device untypeds, with the
exception of frames, which do not get zeroed and cannot be used
as an IPC buffer. Device untypeds additionally cannot be used
in the construction of ASID pools.

This then changes the API to the rootserver (i.e. bootinfo) to
send device untypeds instead of device frames. On ARM these
device untypeds are the same as the previously exported device
frame regions. On x86 PCI scanning is removed and all physical
memory addresses (that are not important for kernel integrity)
are released to the user.

In order to have bits in the frame and untyped caps on ARM the
number of software ASIDs had to be reduced from 2^18 to 2^17,
and the maximum untyped size reduced from 2^31 to 2^30

SELFOUR-566: Decouble seL4_DebugNameThread from CONFIG_PRINTING

Explicitly check if a capability is physical or not

Previously the return value of cap_get_capPtr was compared to 0 in
sameRegionAs to emulate a check in the abstract specification that
tests if the cap is a physical cap or not. Overloading 0 results
in a scenario where a legitimate deviceUntyped's children do not
get considered to be children because they have a capPtr of 0.

This change adds and explicit function that returns whether or not
a capability is physical or not, and uses that in sameRegionAs

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-399: object sizes and globals frame addr should come from the same source

trivial: style

x86: IOAPIC/MSI syscalls

Restructure the x86 interrupt handling to allow for a more flexible
method of using IOAPIC and MSI interrupts. The essence of this change
is to allow for the user to pick, for both IOAPIC and MSIs, which
CPU vector to use. Additionally there is future support, in the API,
for seL4 to eventually protect MSI interrupts with the vt-d interrupt
routing tables.

API behaviour for legacy systems using the PIC is preserved

Part of SELFOUR-281

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

conversion: uncommit auxupd change

conversion: fixed bitfield generator, clz spec

unsigned int -> word_t

Create array types in retype AUXUPDs.

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

refactor tcb_t to remove duplication between x86 and arm header files

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

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

Trivial: Remove unnecessary #includes.

Fix style and unused variable warnings.

Ghost assertions about max object size.

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

Support IOAPIC on ia32 and modify interrupt handling to support user level setting of modes

Release snapshot