IOMMU: Refactor the memory module by cazb2 · Pull Request #7 · au-ts/microkit

cazb2 · 2026-07-07T00:18:40Z

This PR makes a small change to the SDF work previously completed.

It then refactors the memory.rs module in preparation for adding support for IO Address Spaces. The refactor primarily introduces an address space abstraction that can allow simpler handling of different address space variants.

It also removes the pre-existing duplicated constants that are already defined by seL4. This commit extracts those and includes them in the Config struct that the tool passes around.

This PR preserves the existing behaviour.

midnightveil · 2026-07-09T01:03:57Z

+#endif
+
+#ifdef VTD_PT_INDEX_BITS
+MICROKIT_CONSTANT(io_page_table_index_bits, VTD_PT_INDEX_BITS)


IOSpaceTableIndexBits?

Oh, you seem to have changed this in PR 8.

midnightveil · 2026-07-09T01:04:11Z

-min_untyped_bits: seL4_MinUntypedBits
-max_untyped_bits: seL4_MaxUntypedBits
-vspace: seL4_VSpaceBits
+#define MICROKIT_CONSTANT(name, value) microkit_constant name value


What's the point of these changes? I don't understand them

Made the parsing simple when I had to dig down to get the VTD information, but with the libsel4 fix I should be able to revert

midnightveil · 2026-07-09T01:05:57Z

    // We expect the PD ELFs to be first and the monitor ELF last in the list of ELFs.
    let mon_elf_id = elfs.len() - 1;
    assert!(elfs.len() == system.protection_domains.len() + 1);
-    let monitor_tcb_obj_id = {


What's the point of this change? You just removed monitor_elf afaict.

This just uses the new return value of add_elf_to_spec, which is both the tcb obj id and the address space

midnightveil · 2026-07-09T01:07:08Z

        device_regions,
        normal_regions,
-        object_sizes,
+        object_sizes: Some(object_sizes_json.object_sizes),


I think this should be split out into object_sizes and address_space_constants, as 2 different preprocessed files or something

yep will fix, I was just following how it was before (mixed), take it back I misinterpreted the original (asid pool index bits seems like a special case), have fixed this

midnightveil · 2026-07-09T01:08:10Z


 /*
- * The Microkit tool needs to know the sizes of kernel objects.
+ * The Microkit tool needs to know the sizes of kernel objects and a small


Your third commit, 'IOMMU: Remove constants retrievable from seL4' has nothing to do with the IOMMU, and could be its own PR done standalone, which would make it easier to review.

midnightveil · 2026-07-09T01:09:01Z

    }
+
+    fn read(&self) -> bool {
+        matches!(self.perms, SysIOMapPerms::Read | SysIOMapPerms::ReadWrite)


What's the point of defininng separate SysIOMapPerms then? What do these permissions do differently than the original SysMapPerms?

SysIOMapPerms can only represent valid perms in the type system, while the other can the anything. The better improvement would be to fix SysMapPerms too... Should I do that?

midnightveil · 2026-07-09T01:09:46Z

    /// Kernel object sizes, used for kernel boot emulation and untyped allocation.
    pub object_sizes: Option<ObjectSizes>,
+    pub page_table_index_bits: u64,
+    /// Only emitted for aarch builds


emitted or omitted? If the former, I'd prefer included, and be specific that it is AArch64.

midnightveil · 2026-07-09T01:10:30Z

-            Arch::Riscv64 => 0x0000003fffffefff,
-            Arch::X86_64 => 0x7fffffffefff,
-        }
+        self.user_top


If this is just a constant now we should have pub vspace_user_top: u64 and use that. No need for this extra function.

midnightveil · 2026-07-09T01:10:38Z

    /// The two remaining fields are only valid on ARM and RISC-V
    pub device_regions: Option<Vec<PlatformConfigRegion>>,
    pub normal_regions: Option<Vec<PlatformConfigRegion>>,
+    /// Emitted on all builds corresponds to seL4_UserVSpaceTop.


Just say // seL4_UserVSpaceTop.

midnightveil · 2026-07-09T01:11:12Z

+        match (self.arch, self.iommu) {
+            (Arch::X86_64, true) => self
+                .io_page_table_index_bits
+                .expect("Error: An x86 VT-D build should have VTD_PT_INDEX_BITS defined by seL4, captured in tool/microkit/object_sizes.h"),


Please reformat over multiple lines.

Because the tool will default to priority 0 if it is not specified. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

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

This is because on x86-64, the VM shares TCB with the parent PD (VMM). Rather than being distinct entities like on ARM. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

Add tests for valid and invalid VM scenarios. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

We recently switched to using a 2 level CSpace for cap mapping support. During the switch there was a mistake in the code that caused a child TCB object to be inserted into the wrong CNode. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

A simple refactor that hide the different CNodes of a PD behind helper functions to make it less error prone during development. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

As per discussions surrounding RFC25, allowing access to a PD's CSpace can violate the static nature of a Microkit system. Let's remove this feature for now for the next release and we can always rework/add it back later. It was also broken, and it did not work properly because of the guard. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

This commit adds 'microkit_pd_resume' that resumes a PD that is stopped by 'microkit_pd_stop'. Signed-off-by: Guangtao Zhu <guangtaozhu@outlook.com>

Hex formatting. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Replace ExecutionContext trait with a Map trait. The previous trait was primarily used in the check_maps function to handle memory regions in virtual machines and normal pds. This Map trait will allow the one check_maps function to handle both SysIOMaps and SysMaps uniformly. The additional information that was provided by the polymorhpic ExecutionContext is just passed as a string to be used in the respective error message. This is because outside of the check_maps function a protection_domain and a virtual_machine are handled as distinct types. Add error checking cases to check_maps. If the map_start + mr.size overflows alot of the pre-exisiting logic breaks so check for it. Also check that we don't overflow the top of user_virtual memory accouting for the differences between protection_domains, virtual_machines and io address spaces. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Add PciDevice struct and PCIDeviceParseError enum. This types allow us to implement the Display trait which gives a consistent way to output PCI information. The FromStr trait implemented for PCIDevice avoid duplicating logic required to parse the PCI identifier from the xml. When combined with the display trait on the PCIDeviceParseError, we get consistent error messages and avoid repeating code. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

This commit adds iommu support to microkit sdfs. Define a constant to represent the a tool enforced limitation on the maximum virtual address suported for an IO address space. This is due to current x86 IOMMU behaviour in the kernel which dynamically detects the maximum virtual address for an IO address space. For more info read: BOOT_CODE bool_t vtd_init_num_iopts(uint32_t num_drhu) in seL4/src/plat/pc99/machine/intel-vtd.c. Add IOMMUDeviceIdentifier and IOMMUDeviceIdentifierParseError to support parsing the sdf based on the current architecture. This allows the sdf parsing to easily support ARM SMMU and RISCV IOMMU. The Display traits again remove repeated code when outputting IOMMUDeviceIdentifer or IOMMUDeviceIdentifierParseError, particularly useful for error messages. Add SysIOMapPerms. Representing the perms in an enum completely removes the existence of invalid IOMapPerms once we parse the sdf. Add SysIOMap. The dual to SysMap, used to represent a mapping in a devices IO virtual address space. Add check_io_maps adapter. Required because check_maps is designed to error check within one address space. Therefore we collect all the mappings that have been made on a per IO address space basis. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Update the manual to include IOMMU information. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Ensure that the sel4::Config struct has the iommu flag asserted, indicating the kernel was built with IOMMU support. If not we fail parsing any io address space elements encountered in the sdf. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Address Feedback from Bill. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Fix a test that was assuming a fixed max virtual address. Instead make the memory region large enough that it will be out of bounds on any realistic max virtual address reported by seL4 via user_top(). Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Add domain ids to microkit system descriptions. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Minor adjustments to the prior sdf work to do with how permissions are handled. Previously I implemented read and write functions as part of the SysIOMapPerms enum, however the old SysMapPerms did not do this. Given these types are meant to exhibit similar behaviour extracting this common logic into the Map trait provides a streamlined interface to check if a permission is set. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

This commit is meant to preserve original functionality. The memory.rs file previously was a collection of functions that allowed the mapping of pages into vspaces. This commit refactors this logic into an AddressSpace type. This will allow us to simply support new variants of address spaces, including IO Address Spaces for devices. The majority of changes are made to allow the old functions to be reusued in a more generic way. The changes to the builder.rs reflect the changes to memory.rs or make use of the trait Map as trait bounds to handle both normal Mappings and IOMappings. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

This commit integrates the improved config to the memory module. This commit removes some of the duplicated constants definitions that seL4 already exports. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch 2 times, most recently from 26a6f14 to c8c04e3 Compare July 7, 2026 00:40

cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from 3580597 to d543258 Compare July 7, 2026 00:51

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch 8 times, most recently from af71760 to 2a462da Compare July 7, 2026 23:38

cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from 43b0567 to dd66aeb Compare July 8, 2026 01:05

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch 3 times, most recently from 4df0221 to 4121642 Compare July 8, 2026 09:26

midnightveil requested changes Jul 9, 2026

View reviewed changes

midnightveil mentioned this pull request Jul 9, 2026

IOMMU: Add backend support for IOMMU #8

Open

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch from 4121642 to 6539123 Compare July 9, 2026 03:15

midnightveil self-assigned this Jul 9, 2026

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch from 6539123 to c4643ad Compare July 9, 2026 08:33

cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from c4b6467 to fd6dab8 Compare July 9, 2026 08:47

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch from c4643ad to d2d3d33 Compare July 9, 2026 08:48

cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch 2 times, most recently from 5e715bd to dfc3853 Compare July 9, 2026 23:50

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch from d2d3d33 to 112cc18 Compare July 9, 2026 23:55

cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from dfc3853 to 7070554 Compare July 10, 2026 00:52

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch from 112cc18 to 51f97b2 Compare July 10, 2026 00:52

cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from 7070554 to d13bf6b Compare July 10, 2026 01:12

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch from 2af2aab to 9ecdac4 Compare July 10, 2026 01:25

cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from d13bf6b to ad35214 Compare July 10, 2026 07:02

dreamliner787-9 and others added 20 commits July 13, 2026 15:56

manual: priority is optional for virtual machine

a2f1f9d

Because the tool will default to priority 0 if it is not specified. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

tool: refactor scheduling internal representation

7468e62

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

tool: a VM on x86-64 cannot have scheduling params

f04ed74

This is because on x86-64, the VM shares TCB with the parent PD (VMM). Rather than being distinct entities like on ARM. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

tool: add tests for virtual machine

200df43

Add tests for valid and invalid VM scenarios. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

tool: refactored shadow CSpace management

711eed5

A simple refactor that hide the different CNodes of a PD behind helper functions to make it less error prone during development. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

libmicrokit: introduce 'microkit_pd_resume'

2a3483a

This commit adds 'microkit_pd_resume' that resumes a PD that is stopped by 'microkit_pd_stop'. Signed-off-by: Guangtao Zhu <guangtaozhu@outlook.com>

IOMMU: Clean up sdf.rs

68ef3ff

Hex formatting. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

IOMMU: Update manual

16f4537

Update the manual to include IOMMU information. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

IOMMU: Validate IOMMU Kernel Support

b3599da

Ensure that the sel4::Config struct has the iommu flag asserted, indicating the kernel was built with IOMMU support. If not we fail parsing any io address space elements encountered in the sdf. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

IOMMU: Capitalise io in manual

45851de

Address Feedback from Bill. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

IOMMU: Fix an SDF parsing test

8fe86d7

Fix a test that was assuming a fixed max virtual address. Instead make the memory region large enough that it will be out of bounds on any realistic max virtual address reported by seL4 via user_top(). Signed-off-by: Callum <c.berry@student.unsw.edu.au>

IOMMU: Support domain ids

4dc6c98

Add domain ids to microkit system descriptions. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Memory Refactor: Integrate the improved config

73853c7

This commit integrates the improved config to the memory module. This commit removes some of the duplicated constants definitions that seL4 already exports. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch from 9ecdac4 to 73853c7 Compare July 15, 2026 04:54

midnightveil mentioned this pull request Jul 15, 2026

Refactor Memory.rs seL4/microkit#558

Merged

Uh oh!

Conversation

cazb2 commented Jul 7, 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!

cazb2 Jul 9, 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!

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!

4 participants

cazb2 commented Jul 7, 2026 •

edited

Loading

cazb2 Jul 9, 2026 •

edited

Loading