Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

make debug_print_bootinfo() a bit more verbose #51

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
+108 −48
Draft

make debug_print_bootinfo() a bit more verbose #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
2d73fd0
libsel4utils: add sel4utils_set_arg0 for RISC-V
axel-h May 9, 2020
a7d6613
style: remove empty line
axel-h Apr 6, 2023
3e78cd2
use proper printf format specifiers
axel-h Jan 2, 2022
52fb382
print slots for extra boot info pages
axel-h May 24, 2022
4c279fe
print more information and memory map
axel-h May 24, 2022
39bb115
libsel4utils: use proper types for printing
axel-h Nov 26, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
106 changes: 80 additions & 26 deletions libsel4debug/src/bootinfo.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,41 +8,95 @@
#include <sel4debug/gen_config.h>

#include <stdio.h>
#include <assert.h>

#include <sel4/sel4.h>
#include <utils/util.h>

static void print_slot_reg_info(char const *descr, seL4_SlotRegion *reg)
{
if (reg->end == reg->start) {
printf("%snone\n", descr);
} else {
printf("%s[%"SEL4_PRIu_word" --> %"SEL4_PRIu_word")\n",
descr, reg->start, reg->end);
}
}

void debug_print_bootinfo(seL4_BootInfo *info)
{
printf("Node: %"SEL4_PRIu_word" of %"SEL4_PRIu_word"\n",
info->nodeID, info->numNodes);
printf("Domain: %"SEL4_PRIu_word"\n",
info->initThreadDomain);
printf("IPC buffer: %p\n", info->ipcBuffer);
printf("IO-MMU page table levels: %"SEL4_PRIu_word"\n",
info->numIOPTLevels);
printf("Root cnode size: 2^%"SEL4_PRIu_word" (%lu)\n",
info->initThreadCNodeSizeBits,
LIBSEL4_BIT(info->initThreadCNodeSizeBits));
print_slot_reg_info("Shared pages: ", &info->sharedFrames);
print_slot_reg_info("User image MMU tables: ", &info->userImagePaging);
print_slot_reg_info("Extra boot info pages: ", &info->extraBIPages);
print_slot_reg_info("User image pages: ", &info->userImageFrames);
print_slot_reg_info("Untyped memory: ", &info->untyped);
print_slot_reg_info("Empty slots: ", &info->empty);

printf("Node %lu of %lu\n", (long)info->nodeID, (long)info->numNodes);
printf("IOPT levels: %u\n", (int)info->numIOPTLevels);
printf("IPC buffer: %p\n", info->ipcBuffer);
printf("Empty slots: [%lu --> %lu)\n", (long)info->empty.start, (long)info->empty.end);
printf("sharedFrames: [%lu --> %lu)\n", (long)info->sharedFrames.start, (long)info->sharedFrames.end);
printf("userImageFrames: [%lu --> %lu)\n", (long)info->userImageFrames.start, (long)info->userImageFrames.end);
printf("userImagePaging: [%lu --> %lu)\n", (long)info->userImagePaging.start, (long)info->userImagePaging.end);
printf("untypeds: [%lu --> %lu)\n", (long)info->untyped.start, (long)info->untyped.end);
printf("Initial thread domain: %u\n", (int)info->initThreadDomain);
printf("Initial thread cnode size: %u\n", (int)info->initThreadCNodeSizeBits);
printf("List of untypeds\n");
printf("------------------\n");
printf("Paddr | Size | Device\n");

int sizes[CONFIG_WORD_SIZE] = {0};
for (int i = 0; i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS && i < (info->untyped.end - info->untyped.start); i++) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This ordering is important because it matches the order of caps in the root CNode.

int index = info->untypedList[i].sizeBits;
assert(index < ARRAY_SIZE(sizes));
sizes[index]++;
printf("%p | %zu | %d\n", (void *)info->untypedList[i].paddr, (size_t)info->untypedList[i].sizeBits,
(int)info->untypedList[i].isDevice);
printf("Extra boot info blobs:\n");
seL4_Word offs = 0;
while (offs < info->extraLen) {
seL4_BootInfoHeader *h = (seL4_BootInfoHeader *)((seL4_Word)info + seL4_BootInfoFrameSize + offs);
printf(" type: %"SEL4_PRIu_word", offset: %"SEL4_PRIu_word", len: %"SEL4_PRIu_word"\n",
h->id, offs, h->len);
offs += h->len;
}

printf("Untyped summary\n");
for (int i = 0; i < ARRAY_SIZE(sizes); i++) {
if (sizes[i] != 0) {
printf("%d untypeds of size %d\n", sizes[i], i);
seL4_Word numUntypeds = info->untyped.end - info->untyped.start;
printf("Used bootinfo untyped descriptors: %"SEL4_PRIu_word" of %d\n",
numUntypeds, CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS);
/* Sanity check that the boot info is consistent. */
assert(info->empty.end == LIBSEL4_BIT(info->initThreadCNodeSizeBits));
assert(numUntypeds < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS);
assert(info->extraLen <= (LIBSEL4_BIT(seL4_PageBits) * (info->extraBIPages.end - info->extraBIPages.start)));

printf("Physical memory map with available untypeds:\n");
printf("---------------------+------+----------+-------\n");
printf(" Phys Addr | Size | Type | Slot\n");
printf("---------------------+------+----------+-------\n");

for (seL4_Word pos = 0; pos < (seL4_Word)(-1); pos++) {
/* Find the next descriptor according to our current position. */
seL4_UntypedDesc *d = NULL;
int idx = -1;
for (int i = 0; i < numUntypeds; i++) {
seL4_UntypedDesc *d_tmp = &info->untypedList[i];
if (d_tmp->paddr < pos) {
continue;
}
if (d && (d_tmp->paddr >= d->paddr)) {
/* Two descriptors for the same region are not allowed. */
assert(d_tmp->paddr != d->paddr);
continue;
}
d = d_tmp; /* Found a better match. */
idx = i;
}
/* No adjacent descriptor found means there is reserved space. */
if ((!d) || (pos < d->paddr)) {
printf(" %#*"SEL4_PRIx_word" | - | reserved | -\n",
2 + (CONFIG_WORD_SIZE / 4), pos);
if (!d) {
break; /* No descriptors found at all means we are done. */
}
}
printf(" %#*"SEL4_PRIx_word" | 2^%-2u | %s | %"SEL4_PRIu_word"\n",
2 + (CONFIG_WORD_SIZE / 4),
d->paddr,
d->sizeBits,
d->isDevice ? "device " : "free ",
info->untyped.start + idx);
seL4_Word pos_new = d->paddr + LIBSEL4_BIT(d->sizeBits) - 1;
assert(pos_new >= pos); /* Regions must not overflow. */
pos = pos_new;
}
}

5 changes: 5 additions & 0 deletions libsel4utils/arch_include/riscv/sel4utils/arch/util.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,3 +38,8 @@ static inline void sel4utils_set_stack_pointer(seL4_UserContext *regs,
{
regs->sp = value;
}

static inline void sel4utils_set_arg0(seL4_UserContext *regs, seL4_Word value)
{
regs->a0 = value;
}
5 changes: 3 additions & 2 deletions libsel4utils/include/sel4utils/benchmark.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,12 @@ static inline void seL4_BenchmarkTraceDumpFullLog(benchmark_tracepoint_log_entry

while ((index * sizeof(benchmark_tracepoint_log_entry_t)) < logSize) {
if (logBuffer[index].duration != 0) {
fprintf(fd, "tracepoint id = %u \tduration = %u\n", logBuffer[index].id, logBuffer[index].duration);
fprintf(fd, "tracepoint id = %"SEL4_PRIu_word" \tduration = %"SEL4_PRIu_word"\n",
logBuffer[index].id, logBuffer[index].duration);
}
index++;
}

fprintf(fd, "Dumped entire log, size %" PRIu32 "\n", index);
fprintf(fd, "Dumped entire log, size %"SEL4_PRIu_word"\n", index);
}
#endif /* CONFIG_BENCHMARK_TRACEPOINTS */
40 changes: 20 additions & 20 deletions libsel4utils/include/sel4utils/benchmark_track.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,10 @@ static inline void seL4_BenchmarkTrackDumpSummary(benchmark_track_kernel_entry_t
index++;
}

fprintf(fd, "Number of system call invocations %d\n", syscall_entries);
fprintf(fd, "Number of interrupt invocations %d\n", interrupt_entries);
fprintf(fd, "Number of user-level faults %d\n", userlevelfault_entries);
fprintf(fd, "Number of VM faults %d\n", vmfault_entries);
fprintf(fd, "Number of system call invocations: %"SEL4_PRIu_word"\n", syscall_entries);
fprintf(fd, "Number of interrupt invocations: %"SEL4_PRIu_word"\n", interrupt_entries);
fprintf(fd, "Number of user-level faults: %"SEL4_PRIu_word"\n", userlevelfault_entries);
fprintf(fd, "Number of VM faults: %"SEL4_PRIu_word"\n", vmfault_entries);
}

/* Print out logged system call invocations */
Expand All @@ -54,22 +54,22 @@ static inline void seL4_BenchmarkTrackDumpFullSyscallLog(benchmark_track_kernel_
/* Get details of each system call invocation */
fprintf(fd,
"-----------------------------------------------------------------------------------------------------------------------------\n");
fprintf(fd, "| %-15s| %-15s| %-15s| %-15s| %-15s| %-15s| %-15s|\n",
"Log ID", "System Call ID", "Start Time", "Duration", "Capability Type",
"Invocation Tag", "Fastpath?");
fprintf(fd, " %-10s | %-7s | %-20s | %-10s | %-3s | %-7s| %-8s\n",
"Log ID", "SysCall", "Start Time", "Duration", "Cap",
"Tag", "Fastpath?");
fprintf(fd,
"-----------------------------------------------------------------------------------------------------------------------------\n");

while (logBuffer[index].start_time != 0 && (index * sizeof(benchmark_track_kernel_entry_t)) < logSize) {
if (logBuffer[index].entry.path == Entry_Syscall) {
fprintf(fd, "| %-15d| %-15d| %-15llu| %-15d| %-15d| %-15d| %-15d|\n",
fprintf(fd, " %-10"SEL4_PRIu_word" | %-7u | %-20"PRIu64" | %-10u | %-3u | %-7u | %-9s\n",
index,
logBuffer[index].entry.syscall_no,
(uint64_t) logBuffer[index].start_time,
logBuffer[index].duration,
logBuffer[index].entry.cap_type,
logBuffer[index].entry.invocation_tag,
logBuffer[index].entry.is_fastpath);
(unsigned int)logBuffer[index].entry.syscall_no, /* 4 bit */
logBuffer[index].start_time, /* 64 bit */
logBuffer[index].duration, /* 32 bit */
(unsigned int)logBuffer[index].entry.cap_type, /* 5 bit */
(unsigned int)logBuffer[index].entry.invocation_tag, /* 19 bit */
logBuffer[index].entry.is_fastpath ? "yes" : "no");
}
index++;
}
Expand All @@ -84,18 +84,18 @@ static inline void seL4_BenchmarkTrackDumpFullInterruptLog(benchmark_track_kerne
/* Get details of each invocation */
fprintf(fd,
"-----------------------------------------------------------------------------------------------------------------------------\n");
fprintf(fd, "| %-15s| %-15s| %-15s| %-15s|\n", "Log ID", "IRQ", "Start Time",
"Duration");
fprintf(fd, " %-10s | %-8s | %-20s | %-10s \n",
"Log ID", "IRQ", "Start Time", "Duration");
fprintf(fd,
"-----------------------------------------------------------------------------------------------------------------------------\n");

while (logBuffer[index].start_time != 0 && (index * sizeof(benchmark_track_kernel_entry_t)) < logSize) {
if (logBuffer[index].entry.path == Entry_Interrupt) {
fprintf(fd, "| %-15d| %-15d| %-15llu| %-15d|\n", \
fprintf(fd, " %-10"SEL4_PRIu_word" | %-8u | %-20"PRIu64" | %-10u\n", \
index,
logBuffer[index].entry.word,
logBuffer[index].start_time,
logBuffer[index].duration);
(unsigned int)logBuffer[index].entry.word, /* 26 bits */
logBuffer[index].start_time, /* 64 bit */
logBuffer[index].duration); /* 32 bit */
}
index++;
}
Expand Down