Adjusted headlines and comment syntax to markdown.

* the recycle operation has been removed
* more detail on what versions are verified
* update comments on real time use of seL4

The "is" keyword compares addresses. "==" compares values.

If the toolchain file is not templated, then any template variables
won't be initialized correctly. Add a test for overwriting
CROSS_COMPILER_PREFIX only if the templated value is valid.

c_handle_fastpath should only be declared for fastpath config.
And also fix the style and docs.
This change will not affect the result of compilation.

Couldn't pass seL4test on ARMv6 due to using FORCE_INLINE.
Replace to static inline will fix it and still got inlined.
Keep FORCE_INLINE for other platforms since inline is broken
on gcc and we have to make sure those functions got inlined.

Updated contributors list from git history.

 * Point to `LICENSES/` and include the syscall note in the README.
 * BSD and GPL license files now provided in LICENSES directory.

These are the texts of all licenses mentioned anywhere in the
seL4 repository.

This file provides license and copyright information for everything
that cannot be tagged inline.

For completeness.

CC-BY-SA-4.0 is a more appropriate license for documentation than BSD
or GPL.

Two files were previously ignored in the license check.

These files are derived from the output of the device tree compiler in
the Linux kernel. The licenses of the input files do all have to be
compatible with at least GPL-2.0-only to be part of Linux.

Invocation and syscall headers are generated and provided under
BSD-2-Clause for user code and GPL-2.0-only for kernel code. To
facilitate people other than the copyright holder performing this
operation, the master files are provided under both (BSD or GPL, free
to choose).

Bib entry is from Data61 database.

references.bib is in version control for deterministic builds, but
it is a generated file.

The .gitignore file doesn't need to be removed from the license check.

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.

provide license info for Doxyfile, README, export.bst

The software license doesn't make much sense for the manual, but
it is for now the only one available.

Made third-party license tags more precise.

The value for the timer frequency was off and this commits corrects it
so that it now contains the correct value.

gcc8 might get wrong branch predications on these condition checks,
and it could break the code layout.

fastpath_call and fastpath_reply_recv got inlined into a single
function. This could cause loading unused code in cache and
additional jump instructions required in c_handle_syscall.

Re-configure a reasonable timer frequency for zynq7000,
so that it can pass the test SCHED0011.

By default, clang looks for tools prefixed with the target triple.
Explicitly setting the target triple in the toolchain file allows seL4
tools to do the same.

When generating/dumping the dtb for the qemu-arm-virt platform,
pass in a 'smp' configuration variable based on
'KernelMaxNumNodes'.

This commit updates the secondary core initialisation to reserve
the VGIC maintenance and VTimer Event IRQs. This change is
introduced in support of SMP configurations when arm hypervisor
support is enabled.

Added support for injecting remote IPI calls towards given VCPU's
on SMP configured systems. This introudcing a new type of
IpiRemoteCall and handlers for updating the vgic state on
incoming/outgoing IPI's.

Co-authored-by: Yanyan Shen <yanyan.shen@data61.csiro.au>

Added constant definitions for the VMPIDR (arm32) and VMPIDR_EL2
(arm64) registers. These being vcpu registers that can be
written, read, saved and restored. The 'Virtualization Multiprocessor
ID Register' (VMPIDR) is needed to program a vcpu's affinity during
initialisation. This is currently only exposed on SMP configurations.

Co-authored-by: Anna Lyons <anna@gh.st>

Without an invariant, during verification we no longer know that the
virtual timer irq is not inactive in restore_virt_timer, necessitating
an extra check.

Truncation to 10 bits is therefore handled by bitfield generator, making
correspondence with more abstract verified specs easier, as they use a
10-bit word to represent IRQs on 32-bit ARM platforms.

Interferes with C parser variable order, want irq_t irq to be short
name.

Provide an error if IRQ is outside of valid Arch_checkIRQ bounds.

At this time verification does not have a provable link between the
current active VCPU and the current thread which would allow concluding
the current thread is runnable when the current VCPU is active. To
handle a fault, the current thread must be runnable.
Added extra checks to VGICMaintenance and VPPIEvent.

An invalid VPPI caused out-of-bounds array access due to missing return
statement.

The message registers were not previously being set to the contents of
the fault.