Skip to content

use the initial task untypes for no kernel patch#308

Closed
midnightveil wants to merge 2 commits intoseL4:mainfrom
au-ts:julia/microkit-no-kernel-patch
Closed

use the initial task untypes for no kernel patch#308
midnightveil wants to merge 2 commits intoseL4:mainfrom
au-ts:julia/microkit-no-kernel-patch

Conversation

@midnightveil
Copy link
Contributor

@midnightveil midnightveil commented May 28, 2025

Previously, microkit used a kernel patch which added two extra parameters to
the seL4 kernel entry code: extra_device_addr_p and extra_device_size. This
allowed for microkit to pass the protection domains ELFs and system invocation
data to the initial task without the data being zeroed by seL4 upon an Untyped
Retype invocation. This was done by making it appear as extra device untypes.

That had several downsides. For one, having a kernel patch is not a great
situation to live in. Furthermore, on certain platforms, e.g. RISC-V SMP, it
would be impossible to add these two extra parameters as it would require extra
C-ABI registers which don't exist.

Instead, what this patch does, is pass the extra data as part of the initial
task region. This is fine, as it was already contiguous with the initial task
(monitor) ELF file; being present in memory just before it.

What this looks like from the initial task's perspective is that it gets
capabilities to Frames in the seL4_BootInfo data. These frames are for the
initial task's memory. As they are already frame objects, we don't have to do
untype retypes for these objects. As they are already mapped into the initial
task memory, we also don't have to create page tables mappings via the monitor
bootstrap invocations.

Fixes #52


  • Can we verify that the initial task frames are for the correct physical addresses (i.e. that they match what we expected?). I had an off-by-1 bug when developing which took a while to figure out; I used an seL4 patch that made DebugCapIdentify print out the cap_getAddr value but that's not viable in general.
  • Does the code structure make sense? I don't know if the way that I wrote the allocation of the frames makes sense.
  • Test all the sDDF examples as a regression test

@midnightveil midnightveil marked this pull request as draft May 28, 2025 05:21
@midnightveil midnightveil force-pushed the julia/microkit-no-kernel-patch branch 2 times, most recently from 5e68849 to c2e6b51 Compare May 28, 2025 06:17
@midnightveil midnightveil marked this pull request as ready for review May 28, 2025 06:33
Comment on lines +98 to +115
#if 0
for (i = bi->userImageFrames.start; i < bi->userImageFrames.end; i++) {
// seL4_DebugCapIdentify(i);
// puts("userImageFramesList[");
// puthex32(i);
// puts("] = slot: ");
// puthex32(bi->userImageFrames.start + i);
// puts(", paddr: ");
// puthex64(bi->untypedList[i].paddr);
// puts(" - ");
// puthex64(bi->untypedList[i].paddr + (1UL << bi->untypedList[i].sizeBits));
// puts(" (");
// puts(bi->untypedList[i].isDevice ? "device" : "normal");
// puts(") bits: ");
// puthex32(bi->untypedList[i].sizeBits);
// puts("\n");
}
#endif
Copy link
Collaborator

Choose a reason for hiding this comment

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

Do you want to make this uncommented?

Copy link
Contributor Author

@midnightveil midnightveil May 28, 2025

Choose a reason for hiding this comment

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

No, it doesn't work because there is no userImageFrames list. I don't think we get told about what physical addresses the user image frames are for. This is the TODO list item № 1.

Comment on lines +204 to +206
// TODO: Why are we even rederiving it here, tbh?
assert_eq!(monitor_virt_subregion.base, monitor_first_vaddr);
assert_eq!(monitor_virt_subregion.end, monitor_last_vaddr);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Retrieving monitor_first_vaddr do you mean?

Copy link
Contributor Author

@midnightveil midnightveil May 28, 2025

Choose a reason for hiding this comment

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

Yeah, since monitor_virt_subregion.base was derived from the monitor ELF first vaddr anyway, I don't know why we load it again here.

(also, not a typo: re-deriving)

Previously, microkit used a kernel patch which added two extra
parameters to the seL4 kernel entry code: `extra_device_addr_p` and
`extra_device_size`. This allowed for microkit to pass the protection
domains ELFs and system invocation data to the initial task without the
data being zeroed by seL4 upon an Untyped Retype invocation. This was
done by making it appear as extra device untypes.

That had several downsides. For one, having a kernel patch is not a
great situation to live in. Furthermore, on certain platforms,
e.g. RISC-V SMP, it would be impossible to add these two extra
parameters as it would require extra C-ABI registers which don't exist.

Instead, what this change does, is pass the extra data as part of the
initial task region. This is fine, as it was *already* contiguous with
the initial task (monitor) ELF file; being present in memory just before
it.

What this looks like from the initial task's perspective is that it gets
capabilities to Frames in the seL4_BootInfo data. These frames are for
the initial task's memory. As they are already frame objects, we don't
have to do untype retypes for these objects. As they are already mapped
into the initial task memory, we also don't have to create page tables
mappings via the monitor bootstrap invocations.

Signed-off-by: julia <git.ts@trainwit.ch>
Signed-off-by: julia <git.ts@trainwit.ch>
@midnightveil midnightveil force-pushed the julia/microkit-no-kernel-patch branch from c2e6b51 to c0e15d5 Compare May 29, 2025 04:31
@Ivan-Velickovic
Copy link
Collaborator

Ivan-Velickovic commented Oct 30, 2025

@midnightveil this has a subtle issue because it is dependent on the kernel build time option of root CNode bits which means that unless you explicitly increase it at build time, it won't work well for larger images.

This is a general problem that also exists with #337, and am currently thinking about the best way to solve it for the next release.

I'm going to close this for now due to it not being applicable with #337.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Allowing Microkit to not require a kernel patch

2 participants