boot: Allocate init bookkeeping structs in bss

ndks_boot, rootserver and rootserver_mem don't contain any non-zero init
values and can be moved to bss so they don't take up space in the ELF.
ndks_boot contains a sparse struct that is > 4MiB on x86_64 and so this
change allows the x86_64 ELF to return to < 200KiB.

Signed-off-by: Kent McLeod <kent@kry10.com>

boot: initialise root server domain

The domain of the root server was previously implicitly initialised to
zero. In the case that the first slot in the domain schedule has a
domain ID other than zero, this might be incorrect. Here, we explicitly
initialise the domain of the root server to the domain ID in the first
slot of the domain schedule.

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

trivial: fix header files

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

mcs: Configure idle SC based on target core

Every SC in the system must be configured based on the actual core on
which it will run and all time comparisons for that SC must be made
relative to that core.

When creating SCs for the system idle threads those SCs must be
configured for their target cores.

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

mcs: SC time relative to assigned core

The starting and ready times for any SC should be relative to the core
on which the SC is running rather than the current core.

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

Make padding word-size independent

An unfortunate hack that lets us specify padding within one
`sizeof(seL4_Word)`-sized chunk of a struct, indpendently of the size of
a word.

Fix calculate_extra_bi_size_bits implementation

This function returns the size_bits for an allocation covering the size
of the extra boot info region.

Previously it was incorrectly handling rounding up the result of CLZL.

Create device untypeds at boot for all arches

Currently on x86 device untypeds are generated by passing the entire
address space minus any parts that are reserved by the kernel or that
are "real" memory (e.g. kernel image, physical RAM).

On ARM and RISC-V, device untypeds were generated at compile-time from
a device tree. This patch moves ARM and RISC-V to use the same approach
as x86, and moves the code from x86 into a common location that's
shared between the three architectures.

Co-Authored-By: Anna Lyons <anna@gh.st>

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

boot: allocate rootserver objects last

This change allows us to know, from just the kernel and dtb, where user
level untyped objects start being allocated from.

- allocate rootserver objects from last available freemem region.
- move create_rootserver_objects call into init_freemem.

ARM boot: abort if out of freemem slots

This fails early if the build process failed to calculate a suitable
MAX_NUM_FREEMEM_REG.

ARM boot: MAX_NUM_FREEMEM_REG++ for new allocator

Previously, the boot allocator would do dynamic calculations to
minimise fragmentation, then throw away the smallest regions.
With the new boot allocator, we can reasonably predict that
fragmentation will create at most one extra region, so this commit
adds one freemem slot for ARM.

boot: refactor allocation of rootserver objects

Prior to this change, the boot process would dynamically allocate
memory for root server objects based on the order of initialisation.
Allocation was a best-fit algorithm.

This change preallocates all memory for root server objects to an
aligned untyped just after the user image. By allocating the objects in
order of size, allocation is greatly simplified and the ability to
reproduce the allocation offline based on the kernel and user image
sizes is increased.

config: make root cnode size 4k minimum

The previous minimum (4) was actually too small to fit more than 1
capability, which would not allow the kernel to boot. A 4K minimum means
on 32-bit, an 8 size is the minimum (256 slots) and on 64-bit, 7 (128
slots).

In addition to being a more practical minimum, this also allows for
simplification of the boot code for future commits.

boot: revert binary verification workaround in init_freemem

The toolchain has been tweaked to accept the original code, so the
workaround is no longer required.

This reverts commit d0d97779cbf0bbf54bab26b2274ae435908d5ab6.

boot: avoid array access in init_freemem

This works around an issue in the binary correctness proofs. The `if`
conditions become assumptions when proving refinement of the branches.
Currently, a simplification step is slow when these assumptions contain
certain modes of array access. The slowdown apparently becomes
dramatically worse when multiple such assumptions are present, such as
in the final `else` branch. Hopefully, this limitation can be addressed
in future work.

boot: use static array rather than stack array

Binary verification cannot parse the instructions produced by the stack
array, likely because none of the existing kernel code declares arrays
on the stack. Given all boot code and data is unmapped, wiped and made
available to the user after boot, moving the array to static data isn't
a problem.

boot: pass the c-parser

- use constant array size on stack
- cast arrays to pointers to match function return types

boot: consolidate init_freemem

init_freemem sets up available regions of memory for the hardware that
seL4 is booting on. Previously this function was duplicated across
architectures, with minor duplication.

This change provides a top-level init_freemem suitable for all
architectures.

- arm/riscv: change get_avail_p_reg to return whole p_reg array
- update all architectures to use new init_freemem.
- wrap init_freemem calls with arch_init_freemem for each arch, where
arch_init_freemem sets up the available and reserved regions of memory
which are passed to init_freemem.

Boot code: Statically allocate idle thread

The idle thread is not managed at user-level and so it can instead be
statically allocated. This simplifies the boot code and increments
towards being easier to formally verify.

boot: allocate irq cnode statically

The memory used for the irq cnode is never available to the user. As a
result this memory can be allocated statically, simplifying the
bootcode.

- remove allocation of irq cnode
- add static init
- generate irq cnode size from cmake for arm
- add static constants for riscv, x86 as there is no variability at the
moment.

Add support for extra bootinfo larger than a page

The current code may not always allocate enough -
change the logic to over-allocate memory rather than under-allocate.

style: set code width to 120

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

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.

Calculate IRQ_CNODE_BITS from maxIRQ

IRQ_CNODE_BITS is determined by the maxIRQ on the platform. Calculate
this value from maxIRQ instead of hardcoding for each platform.

Retire boot_ctzl.

This was a workaround for a problem that was properly fixed in
f8606c86 however the boot_ctzl version somehow persisted.

Remove irrelavant changes from riscv commit to non riscv arch code

[SELFOUR-1156] RISC-V Port

Experimental release that supports both RV32 and RV64

Assign correct affinity to idle thread

Avoid repeatedly appending idle threads to debug list

Each node calls `init_core_state` and so can be relied upon to append their own idle
thread. Having every core enqueue all the cores idle threads is not correct as it will
result in attempting to enqueue a thread more than once.

Share linker.h between architectures

SMP: Introduce ENABLE_SMP_SUPPORT

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

Call Arch_setTCBIPCBuffer from kernel/boot.c

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.

SELFOUR-880: name the idle thread

SELFOUR-864: Fix alignment calculation

refactor: initialise common core state in one place

Remove assumption on 32-bit memory offsets

On 64-bit platforms physical address could be >2^32 offset from a virtual address. This
changes offsets to match the word size of the target architecture

Provide spec for CTZL

Provides a spec for the __builtin_ctzl function and changes existing
code to use this wrapper

[STYLE_FIX]

Helper for allocating the extra boot info region

Extend bootinfo to support potentially arbitrary additional structures

This provides a future proof interface for extending the bootinfo region with additional
kinds of optional architecture and platform specific information. The basic idea is to
report the size of a region directly following the bootinfo frame, which is made up of
a series of 'chunks'. Each chunk has an identifier (describing what it is) and a length,
allowing unknown chunks to be skipped in favor of examining the remaining of the chunks.

Use same constant for clearing and allocating bootinfo frame

Closes #56

Remove many DONT_TRANSLATE markers.

The vast majority of the DONT_TRANSLATE markers in the kernel are used
to hide __asm__ statements and builtin functions
(e.g. __builtin_unreachable ()) from the C-to-Isabelle parser.

The parser now supports underscore identifiers and many __asm__ statements,
and the builtin functions are prototyped, meaning the vast majority of the
DONT_TRANSLATE markers can be dropped. The remaining markers cover functions
that must be treated specially.

[STYLE_FIX]

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.

SELFOUR-222: Configure IRQ cnode size per platform

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.

add basic api for setting affinity

Update SMP idle thread handling

Defined untyped size ranges in libsel4

SELFOUR-632: implement cores non-architecture dependent structres

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-421: Add padding for untyped in bootinfo

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

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 bootinfo.h duplication

SELFOUR-399: object sizes and globals frame addr should come from the same source

Do not switch to the the root thread until after cpu initialization is done

Remove `boot_clzl`.

This function seemed to exist for the sole reason of being able to mark the CLZ
operation as DONT_TRANSLATE. This is no longer necessary as the underlying
`clzl` function is now marked DONT_TRANSLATE.

Fix missing include.

This file uses macros like `CLZL` that are defined in util.h.

x86: Define a KERNEL_BASE_OFFSET for translating the kernel image region

This definition is different to BASE_OFFSET in that it is only meant to
apply to the kernel image portion of the kernel window, and doesn't
assume that the entire window can be translated by a single offset

unsigned int -> word_t

Rename uint32_t -> word_t in any relevant places

Rename CTZ and CLZ functions to long variants, change parameters from uint32_t to word_t to make compatible between 32 and 64-bit

Use wordBits instead of constant 32

refactor tcb_t to remove duplication between x86 and arm header files

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

ARM: Map the initial thread's IPC buffer and boot info as non-executable.

Note that this also required some irrelevant x86 changes to match function
arguments.

ia32: Large commit that implements PAE paging for x86

This commit involves the PAE paging itself, refactoring the
vspace code to extra what is common between PAE and 32bit paging,
as well as some renaming to not call the root paging structure
a PD

trivial: Standardise on 32-bit unsigned variables for domain values.

Domains are unnecessarily treated explicitly as 8-bit values within boot info.
Though there are existing proof constraints that limit the maximum domain value
to 8 bits, most of the code would permit domain values up to 32 bits. The
maximum value is unnecessarily constrained in boot info, a restriction which
this commit removes.

Closes VER-341

Derive a new IPC buffer cap when inserting into the initial threads TCB to remove mapping information

For any other thread setting the IPC buffer via TCB_Configure will result
in a derived capability being installed that does not have mapping information.
This leads to a expected behaviour that setting a new IPC buffer (even if it is
the same as the current one), will not perform an unmapping.

Release snapshot