RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

boot: Check that predicted page tables were used

Browse Source 
During boot, all dynamic memory allocated by the kernel is precalculated
and then allocated in one chunk. The precalculation is supposed to match
the allocation logic precisely which means any left over objects
indicated an inconsistency between the precalculation and reality. The
kernel should print an error and potentially abort if it encounters this
situation.

Signed-off-by: Kent McLeod <kent@kry10.com>
This commit is contained in:
Kent McLeod
2022-09-26 09:00:18 +10:00
committed by Kent McLeod
parent 411ff14556
commit f2925faee8
1 changed files with 6 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
src/kernel/boot.c
View File

@@ -832,6 +832,12 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap)
BOOT_CODE void bi_finalise(void)
{
if (rootserver.paging.start != rootserver.paging.end) {
printf("WARNING: internal book keeping errror. Less pagetables allocated than predicted: "
"%ld page tables allocated but not used.\n", (rootserver.paging.end - rootserver.paging.start) >> seL4_PageTableBits);
}
ndks_boot.bi_frame->empty = (seL4_SlotRegion) {
.start = ndks_boot.slot_pos_cur,
.end = BIT(CONFIG_ROOT_CNODE_SIZE_BITS)