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