Skip to content

Commit

Permalink
Merge patch-axel-6
Browse files Browse the repository at this point in the history
  • Loading branch information
@axel-h
axel-h committed Apr 12, 2024
2 parents 8c940b9 + 238a5be commit c819a0a
Show file tree
Hide file tree
Showing 4 changed files with 108 additions and 48 deletions.
106 changes: 80 additions & 26 deletions libsel4debug/src/bootinfo.c
View file
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++) {
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
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
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
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

0 comments on commit c819a0a

Please sign in to comment.