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?

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>

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 2 times, most recently from 82e995b to 5073a85 Compare July 9, 2026 05:21

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

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 added 3 commits July 10, 2026 11:25

IOMMU: Add IOMMU helper to config

b319171

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

df27a19

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

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