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.

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

IOMMU: Support domain ids

d13bf6b

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

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

cazb2 added 2 commits July 10, 2026 11:25

Memory Refactor: Integrate the improved config

9ecdac4

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 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

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!

2 participants

cazb2 commented Jul 7, 2026 •

edited

Loading

cazb2 Jul 9, 2026 •

edited

Loading