Add bootinfo tag by terryzbai · Pull Request #536 · seL4/microkit

terryzbai · 2026-06-25T00:36:37Z

This PR is rebased on branch rust_sel4_update_to_main, which should be merged soon. The proposed feature is included in the only last commit.

This PR adds the bootinfo tag to map specified type of bootinfo into PD's vspace, and patch the address to pre-declared variable bootinfo_{bi_type}. This is useful for the cases where the userspace applications needs to consume bootinfo, e.g., RSDP in ACPI driver, TSC used as clock source, etc.

The usage of bootinfo tag is added in the example x86_64_ioport. It works with this rust-sel4 PR on x86 to show how TSC frequency is mapped and read by a PD.

Previously, the ELF code treats program headers = segments. While this worked originally, it broke for cases that requires >= 2 program headers to refer to the same segment. Now, when the ELF is parsed, the code will create a 1-1 mapping of segments to program headers like before. But the allow for additional program headers to be inserted. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

Added `pub fn phdrs_table(&self) -> Vec<(ElfProgramHeader64, usize)>` to ELF code. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

Modified `pub fn add_segment()` to allow for an additional program header in the ELF to describe the segment with a user defined type identifier. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

Which also required changes to how the spec is packed into the intialiser. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

This adds the 'bootinfo' tag to map specified type of bootinfo into PD's vspace, and patch the location to the pre-declared variable. This is useful for the cases where the userland needs to access some of boot information, e.g., RSDP in ACPI driver. The example shows how TSC Frequency is mapped and read by a PD. Signed-off-by: Terry Bai <tianyi.bai@unsw.edu.au>

midnightveil · 2026-06-25T01:08:02Z

+        let bi_type = match xml_bi_type {
+            "vbe" => FillEntryContentBootInfoId::X86Vbe,
+            "mbmmap" => FillEntryContentBootInfoId::X86Mbmmap,
+            "rsdp" => FillEntryContentBootInfoId::X86AcpiRsdp,
+            "framebuffer" => FillEntryContentBootInfoId::X86FrameBuffer,
+            "tsc_freq" => FillEntryContentBootInfoId::X86TscFreq,
+            _ => return Err(format!("BootInfoMap type: '{xml_bi_type}' is not supported.")),
+        };


This should be consistent with the naming scheme of the enum/seL4 Bootinfo items - as in keep the prefix.

you mean the whole sel4_bootinfo_header_x86_vbe or x86_vbe?

midnightveil · 2026-06-25T01:10:20Z

+                        if existing_bi_map.bi_type == bi_map.bi_type {
+                            let pos = xml_sdf.doc.text_pos_at(child.range().start);
+                            return Err(format!(
+                                "Error: duplicate {:?} in protection domain '{}' @ {}",


Unless rust-seL4 actively prevents this I don't really see a reason to prevent duplicates. It adds extra code that isn't useful.

"No duplicates" assumption is used for patching the address of bootinfo into a PD via setvar? and there is no use cases that need duplicate bootinfo I think.

Oh, is the name of the setvar implicit? I really don't like that.

no use cases that need duplicate bootinfo I think.

That doesn't mean there couldn't be one, and it's more effort to prevent it.

yes, it is implicit. It will be solved if we use prefilled MRs.

That doesn't mean there couldn't be one, and it's more effort to prevent it.

right, so prefilled MR is indeed a better solution in this case.

Well, we can't use "prefilled" MRs directly, but if we had a mechanism closer to it.

Are you saying we still need a bootinfo tag outside of PDS? Can I know what's your concern of adding an optional parameter in prefilled MRs?

Prefilled MRs means an MR prefilled from a file.

This isn't "prefilled" in the same way as other prefilled, but it's a similar mechanism.

midnightveil · 2026-06-25T01:13:02Z

        let mut setvars: Vec<SysSetVar> = Vec::new();
        let mut child_pds = Vec::new();
+        let mut bootinfo_maps: Vec<BootInfoMap> = Vec::new();
+        let mut mem_top = config.pd_map_max_vaddr(stack_size);


I don't link this very much. The implicit allocation adds a whole bunch of extra cases to our logic about overmapping, which makes things difficult.

Could the bootinfo not just be another <mr> that one specifies and then we can place bootinfo "inside" of it?

(You could then in theory map it in RO to multiple PDs without needing to copy it many times - for instance, if we wanted to map in the FDT it would probably be bad to copy it into every PD)

We could make the SysMemoryRegion have the kind be User/Elf/Stack/Prefill(with a buffer)/Bootinfo (type)` and then these would all be consistently handled

Yes, that's true. I didn't realise that we already had prefilled MR.

midnightveil · 2026-06-25T01:13:51Z

+
+#[repr(u64)]
+#[derive(Debug, Copy, Clone, Eq, PartialEq)]
+pub enum BootInfoId {


Isn't there already the rust-sel4 FillEntryContentBootInfoId which you use?

uh my bad. I forgot to remove them after replacing with FillEntryContentBootInfoId.

dreamliner787-9 · 2026-06-25T03:03:12Z

+    microkit_dbg_puts("TSC Frequency: ");
+    microkit_dbg_put32(bootinfo_tsc_freq->value);
+    microkit_dbg_puts("MHz\n");
+


Can we please split this into a new example called bootinfo or something like that? That comes with the benefit of being able to target other archs as well. As this example is just meant to show x86 PIO operations.

yes, I have added a separate example for this. Do you have any ideas of how to demonstrate the ability to read DTB on ARM?

we can probably quite easily parae the fdt header and at the very least verify the magic bytes and print the version, without having to write an entire fdt library.

edit: although saying that, microkit loader does not pass through the dtb and always passes 0,0 for the dtb, so.

dreamliner787-9 and others added 5 commits June 19, 2026 10:10

tool/elf: refactored program headers table mgmt

0c8df63

Added `pub fn phdrs_table(&self) -> Vec<(ElfProgramHeader64, usize)>` to ELF code. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

tool/elf: + segment with multiple program headers

c7abd5a

Modified `pub fn add_segment()` to allow for an additional program header in the ELF to describe the segment with a user defined type identifier. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

Switch rust-sel4 to mainline commit

d9b1e0a

Which also required changes to how the spec is packed into the intialiser. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

midnightveil reviewed Jun 25, 2026

View reviewed changes

dreamliner787-9 suggested changes Jun 25, 2026

View reviewed changes

Uh oh!

Conversation

terryzbai commented Jun 25, 2026

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!

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!

midnightveil Jun 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

midnightveil Jun 25, 2026 •

edited

Loading