Add support for prefilling memory regions from data files at compile time by dreamliner787-9 · Pull Request #434 · seL4/microkit

dreamliner787-9 · 2026-03-10T23:52:44Z

The Memory Region (MR) prefill data file path is specified in a prefill_path attribute of a memory_region element. Then any PDs that maps the MR can learn of the prefilled data size via setvar_prefill_size.

The tool will always prefill data from the start of the MR. This is useful in cases such as packing Linux kernel and initial ramdisk images into a VMM PD.

Additional thoughts adjacent to #422 and au-ts/sddf#622 (comment): perhaps it would be better if we get rid of all the "setvar" and just have a "bootinfo" structure that we pass to init().

Closes #248

midnightveil · 2026-03-11T05:11:35Z

tool/microkit/src/sdf.rs

        max_vaddr: u64,
    ) -> Result<SysMap, String> {
-        let mut attrs = vec!["mr", "vaddr", "perms", "cached"];
+        let mut attrs = vec!["mr", "vaddr", "perms", "cached", ""];


midnightveil · 2026-03-11T05:11:56Z

tool/microkit/src/sdf.rs

        if allow_setvar {
            attrs.push("setvar_vaddr");
            attrs.push("setvar_size");
+            attrs.push("setvar_prefill_size");


what's differnce between prefill size and size?

setvar_size is the size of the entire memory region, whereas setvar_prefill_size is the size of the data blob that was prefilled.

why would you ever need the size of the memory region? (presumably by that you mean a page aligned size?) is not the size of the data good enough?

unless you're saying the size of the memory region has to be specified separately to the size of the data, in which case (I don't know why you would want this?) you should probably add more checks for handling the overflow case nicely. but again I don't know why you wouldn't ever just want the actual size.

Yes the size of the MR must be specified separately to the size of the data, since they may be different. setvar_size was an existing feature so I didn't change it. The overflow condition is checked in https://github.com/seL4/microkit/pull/434/changes#diff-e9fc0f34d513cf693bc173e1ee69c3b08a3f7be618e5a70d4d6c08faf8aa3955R1296

But why? Why would this ever matter? This is only ever going to add more work for the user who has to match the size to the prefill.

So you mean, if the user want to prefill a memory region, we automatically size it based on the prefill file size? Because right now, the only rule is that the memory region size must be >= prefill size.

yes. I don't see a case where that wouldn't be the desired behaviour.

I see, one case I thought of when doing this was that the user might use the prefill data for something, then "reclaim" the MR for other things. Which is more useful if the MR is large to begin with. Such as having a large guest RAM MR, prefilling it with the kernel and initrd at the start. Then at init(), memmove() it to the right place. Plus, if the user is responsible for sizing the MR, they have control over the page size and whatnot.

But now that I think about it, this might not be useful for PD restart and whatnot. I can change it so that prefilled MRs are automatically sized. What do you think?

It's possible that that is useful, yes.

Maybe it makes sense for it to be an optional thing?

Yes I can make it an optional thing

midnightveil · 2026-03-11T05:14:53Z

tool/microkit/src/sdf.rs

+            .map(|xml_prefill_path| Path::new(xml_prefill_path).to_path_buf());
+
+        let prefill_bytes_maybe = if let Some(prefill_path) = prefill_path_maybe {
+            let bytes = match fs::read(&prefill_path) {


this should use the get_full_path function to look at search paths

midnightveil · 2026-03-11T05:15:43Z

tool/microkit/src/sdf.rs


+        let prefill_path_maybe = node
+            .attribute("prefill_path")
+            .map(|xml_prefill_path| Path::new(xml_prefill_path).to_path_buf());


PathBuf::from

midnightveil · 2026-03-11T05:17:38Z

tool/microkit/src/sdf.rs

+        let prefill_bytes_maybe = if let Some(prefill_path) = prefill_path_maybe {
+            let bytes = match fs::read(&prefill_path) {


you should use the option chaining operations so that we're not continually doing more and more indents to handle the cases. Option and result are monadic for a reason!

Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

dreamliner787-9 force-pushed the issue_248 branch from af1ca0d to b99e2f3 Compare March 10, 2026 23:55

midnightveil suggested changes Mar 11, 2026

View reviewed changes

dreamliner787-9 added 3 commits March 12, 2026 13:32

tool: implement memory region data prefilling

04e4c9a

Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

manual: document memory region data prefilling

26986a8

Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

examples: add mr_prefill

c11e48d

Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

dreamliner787-9 force-pushed the issue_248 branch from b99e2f3 to c11e48d Compare March 12, 2026 02:56

		let prefill_bytes_maybe = if let Some(prefill_path) = prefill_path_maybe {
		let bytes = match fs::read(&prefill_path) {

Conversation

dreamliner787-9 commented Mar 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

dreamliner787-9 commented Mar 10, 2026 •

edited

Loading