IOMMU: Add backend support for IOMMU by cazb2 · Pull Request #8 · au-ts/microkit

cazb2 · 2026-07-07T23:45:33Z

Adds logic for the creation of the IOMMU Capdl spec objects.
Adds an example demonstrating the use of the IOMMU.
Enables the IOMMU in the build_sdk.

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


 env:
-  SEL4_VERSION: b7ef16a42d6d87b776462e66b8803365aea9f41d
+  SEL4_VERSION: b57b3de19526375eb63343f750b9720a3e20babf


Note that this also requires updates to seL4/microkit-manifest.

where's that?

https://github.com/seL4/microkit-manifest/

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

+#include <stdint.h>
+
+#include <microkit.h>
+#include <sys/wait.h>


Erm, we don't have Linux, how does this work?

unused, will delete

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

-#ifdef VTD_PT_INDEX_BITS
-MICROKIT_CONSTANT(io_page_table_index_bits, VTD_PT_INDEX_BITS)
+#ifdef seL4_IOPageTableIndexBits
+MICROKIT_CONSTANT(io_page_table_index_bits, seL4_IOPageTableIndexBits)


Oh, I see this changed from here: #7 (comment)

midnightveil · 2026-07-09T02:15:26Z

+            // The useable set of domain_ids can only be discovered through run-time errors in seL4.
+            // Crazy right! Mircokit tool does not support multiple devices sharing the same address
+            // space thus domain_id is not used by the Microkit tool.
+            domain_id: Word(0),


This will need to be changed as discussed.

midnightveil · 2026-07-09T02:16:12Z

        Object::PageTable(_) => "PageTable",
        Object::AsidPool(_) => "AsidPool",
+        Object::IODevice(_) => "x86 IODevice",
+        Object::IOPT(_) => "x86 IOPageTable",


midnightveil · 2026-07-09T02:16:27Z

 // SPDX-License-Identifier: BSD-2-Clause
 //

+use sel4_capdl_initializer_types::x86_io_address_space;


Please make this consistent with other imports.

midnightveil · 2026-07-09T02:16:52Z

            (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"),
+                .expect("Error: An x86 VT-D build should have seL4_IOPageTableIndexBits defined by seL4, captured in tool/microkit/object_sizes.h"),


Move to other PR?

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>

Update microkit to use rust-sel4 with the new x86 IOMMU capdl support. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

This commit adds a helper to extract the io page table index bits from the config. This currently only supports a IOMMU build on x86. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

This commit implements support for the x86 IOMMU Capdl spec. The memory module is extended to allow for the construction of IOMMU address spaces. The Capdl spec refers to the IOSpace object as the IODevice object and the IO Page tables as IOPTs. Within microkit we use IOSpace to refer to the whole IO address space. It also provides an example using the qemu dma capable test device, demonstrating the use of the IOMMU. Note we did not need to provide physical memory addresses for any dma buffers, proving the IOMMU correctly translated our requests. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

While seL4 does not support large pages to be used by the IOMMU, we will raise an error at the SDF parsing stage. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

Integrate the new IOMMU support from the rust-sel4 capdl initialiser. Integrate the rust-sel4 PCI structure to avoid repeating definitions to improve code maintainability. The traits that we implement on the wrapper struct, make it easy to use the wrapper without having to worry about accessing the underyling type. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

cazb2 requested review from dreamliner787-9 and midnightveil July 7, 2026 23:45

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch 2 times, most recently from ad6a939 to 4fdc587 Compare July 8, 2026 00:58

cazb2 force-pushed the callumb_and_cheng/iommu_memory_refactor branch 2 times, most recently from 6a5c062 to 4df0221 Compare July 8, 2026 01:49

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch 7 times, most recently from 6110e20 to 0f014d7 Compare July 8, 2026 09:22

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

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch 2 times, most recently from 54437dc to f363700 Compare July 8, 2026 10:22

midnightveil reviewed Jul 9, 2026

View reviewed changes

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

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from f363700 to 4d27483 Compare July 9, 2026 03:23

cazb2 changed the base branch from callumb_and_cheng/iommu_memory_refactor to callumb_and_cheng/config_constants July 9, 2026 03:25

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 4d27483 to 711827e Compare July 9, 2026 03:31

cazb2 force-pushed the callumb_and_cheng/config_constants branch 2 times, most recently from caf67fe to 31069d2 Compare July 9, 2026 03:43

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 711827e to 0f1363d Compare July 9, 2026 03:44

cazb2 force-pushed the callumb_and_cheng/config_constants branch from 31069d2 to 284c6d6 Compare July 9, 2026 03:49

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 0f1363d to 91e685e Compare July 9, 2026 03:50

cazb2 force-pushed the callumb_and_cheng/config_constants branch from 284c6d6 to 08f27ce Compare July 9, 2026 03:56

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 91e685e to 86928dc Compare July 9, 2026 03:56

midnightveil self-assigned this Jul 9, 2026

cazb2 force-pushed the callumb_and_cheng/config_constants branch from 08f27ce to b8f5869 Compare July 9, 2026 05:18

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 5073a85 to 2d8be3a Compare July 9, 2026 08:41

cazb2 force-pushed the callumb_and_cheng/config_constants branch from 658c8e4 to 5919e3f Compare July 9, 2026 08:49

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch 2 times, most recently from b5c3336 to 54f9a05 Compare July 9, 2026 08:51

cazb2 marked this pull request as ready for review July 9, 2026 08:51

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 5366060 to 2e1b57e Compare July 9, 2026 09:22

cazb2 force-pushed the callumb_and_cheng/config_constants branch from 5919e3f to 84cec53 Compare July 9, 2026 23:56

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 2e1b57e to 5a4cd2f Compare July 9, 2026 23:59

cazb2 force-pushed the callumb_and_cheng/config_constants branch from 84cec53 to 95dd28f Compare July 10, 2026 00:54

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch 2 times, most recently from 3c79207 to 342676a Compare July 10, 2026 01:04

cazb2 changed the base branch from callumb_and_cheng/config_constants to callumb_and_cheng/iommu_memory_refactor July 10, 2026 01:07

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 342676a to 829568e Compare July 10, 2026 01:23

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/iommu_microkit_backend branch from 829568e to df27a19 Compare July 10, 2026 01:26

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

cazb2 added 3 commits July 15, 2026 15:05

Memory Refactor: Integrate the improved config

770bf45

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_microkit_backend branch 3 times, most recently from b852552 to 1b6af52 Compare July 15, 2026 06:02

cazb2 added 4 commits July 15, 2026 16:08

IOMMU: Update Cargo rust-sel4

5f4f199

Update microkit to use rust-sel4 with the new x86 IOMMU capdl support. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

IOMMU: Add IOMMU helper to config

559c139

This commit adds a helper to extract the io page table index bits from the config. This currently only supports a IOMMU build on x86. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

IOMMU: Add large page guard

e63bdef

While seL4 does not support large pages to be used by the IOMMU, we will raise an error at the SDF parsing stage. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 1b6af52 to 0f708aa Compare July 15, 2026 06:09

midnightveil mentioned this pull request Jul 15, 2026

IOMMU: IOMMU backend support seL4/microkit#559

Merged

cazb2 force-pushed the callumb_and_cheng/iommu_microkit_backend branch from 0f708aa to ba6cf23 Compare July 15, 2026 06:25

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

IOMMU: Add backend support for IOMMU#8

IOMMU: Add backend support for IOMMU#8
cazb2 wants to merge 8 commits into
callumb_and_cheng/iommu_memory_refactorfrom
callumb_and_cheng/iommu_microkit_backend

cazb2 commented Jul 7, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

cazb2 Jul 9, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

cazb2 Jul 9, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

midnightveil Jul 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

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

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