Add iommu support to microkit by Cheng-Li1 · Pull Request #467 · seL4/microkit

Cheng-Li1 · 2026-04-10T08:04:33Z

This pull request adds iommu support for Microkit and needs Rust-Sel4 with the iommu support to work.

Supported features:
Map the memory region to a device-visible memory address.

Tests done:
Blk example with iommu feature enabled on x86 qemu and hardware(vb-105).

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

…ure for generating spec in microkit tool. Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

…e check unused mr and mr page size optimization logic for iomaps support. Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

dreamliner787-9 · 2026-04-16T01:06:46Z

 [workspace.dependencies.sel4-capdl-initializer-types]
-git = "https://github.com/seL4/rust-sel4"
-rev = "7a2321f2d84310ba7a09fe7f5988e6dcecde3566"
+path = "/home/cheng/system/rust-sel4/crates/sel4-capdl-initializer/types"


Can you update it to the commit hash that added IOMMU support to the capDL initialiser in rust-sel4 so that the CI works? On that note, you will need to rebase your branch as well, the CI doesn't run when there are conflicts.

dreamliner787-9 · 2026-04-16T01:09:38Z

@@ -0,0 +1,282 @@
+use std::ops::Range;


Missing copyright here

dreamliner787-9 · 2026-04-16T01:12:29Z

+        }),
+    });
+
+    const PD_TO_DOMAIN_ID_OFFSET: u16 = 1;


You should explain why this is needed (with kernel source) for future reference.

dreamliner787-9 · 2026-04-16T01:15:34Z

+                            "Error: iomap for '{}' has address 0x{:x} which exceeds the upper limits of {} in {} '{}' @ {}",
+                            io_map.name,
+                            map_end,
+                            crate::capdl::iomem::VTD_MAX_ADDR,


I feel like VTD_MAX_ADDR should be printed as hex.

dreamliner787-9 · 2026-04-16T01:19:29Z

    }
+
+    #[test]
+    fn test_iommu_valid_on_x86() {


This should be called test_iommu_out_of_bound or similar.

On this note, I would like to see more tests, e.g. overlapping mappings, invalid page size, trying to use IOMMU on non-x86 targets etc.

dreamliner787-9 · 2026-04-16T01:31:21Z

            phys_base: None,
            spec_metadata: None,
-            log_level: LogLevel::Info,
+            log_level: LogLevel::Debug,


This shouldn't be changed.

dreamliner787-9 · 2026-04-16T01:36:59Z

+    sel4::Config,
+};
+
+// VTD Page table level is defaulted to the three-level structure even if the hardware supports four level.


I forgot the content of the conversation we had offline about this. But what happens when the target machine only support 3 levels VT-d page table, but we made a 4 levels one (according to VTD_PAGE_TABLE_LEVEL)?

dreamliner787-9 · 2026-04-16T01:41:24Z

Your commit history needs to be cleaned up and squashed. Some of the commits checked in code that should not be in Microkit, then other commits removed them.

dreamliner787-9 · 2026-04-16T01:49:43Z

A nice to have would be a minimal example showing this in action on QEMU x86, like the arm_smc or x86_64_ioport examples, as a proof that it works.

For example, you can use QEMU's DMA-capable "educational device": https://www.qemu.org/docs/master/specs/edu.html. You copy some data from normal RAM into the device's SRAM with a DMA transaction, then read back the device's SRAM via normal MMIO to verify that the transfer succeeded.

midnightveil

Misc things.

I'm not quite sure how this is supposed to be used in the SDF file.

I can only vaguely infer from the error tests you added, but you should add documentation on how to use this and what that means for the layout of the page tables for both.

midnightveil · 2026-04-16T07:26:18Z

 use sel4_capdl_initializer_types::{
-    object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec,
-    Word,
+    object::{self},


Why object::{self}. What was wrong with just object?

midnightveil · 2026-04-16T07:26:59Z

+    for frame_obj_id in frames.iter() {
+        // Make a cap for this frame.
+        let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, false, false);


Suggested change

for frame_obj_id in frames.iter() {

// Make a cap for this frame.

let frame_cap = capdl_util_make_frame_cap(*frame_obj_id, read, write, false, false);

for &frame_obj_id in frames.iter() {

// Make a cap for this frame.

let frame_cap = capdl_util_make_frame_cap(frame_obj_id, read, write, /* what does this mean */ false, /* what does this mean */ false);

midnightveil · 2026-04-16T07:27:42Z

-        // Step 3-4 Create Scheduling Context
+        // Step 3-4 Create and Map IO Page Table Structure
+        if kernel_config.iommu {
+            let mut pci_to_iospace: HashMap<(u8, u8, u8), ObjectId> = HashMap::new();


This is assuming x86-specificness.

Do we not have a PciDev type anyway, that would make this nicer

also what happened to the domain id from the rust-seL4 pr?

midnightveil · 2026-04-16T07:29:45Z

+};
+
+// VTD Page table level is defaulted to the three-level structure even if the hardware supports four level.
+// Sel4 will only attempt to use the four-level structure if the hardware does not supports three level.


seL4.
Check the grammar.

midnightveil · 2026-04-16T07:30:06Z

+
+// VTD Page table level is defaulted to the three-level structure even if the hardware supports four level.
+// Sel4 will only attempt to use the four-level structure if the hardware does not supports three level.
+// https://github.com/seL4/seL4/blob/c406015c389decc4559fd44cb69604ddd24a0ddb/src/plat/pc99/machine/intel-vtd.c#L498


Use a link to a commit tag preferably over a random commit hash, e.g. seL4/seL4/blob/15.0.0.

midnightveil · 2026-04-16T07:45:39Z

+    pub name: String,
+    pub pci_bus: u8,
+    pub pci_dev: u8,
+    pub dev_func: u8,
+    pub ioaddr: u64,
+    pub perms: u8,
+    pub text_pos: Option<roxmltree::TextPos>,


Same comments as the rust-seL4 PR: the PCI stuff should be part of x86 as itis arch-speicific.

midnightveil · 2026-04-16T07:46:13Z

+                if map_end > crate::capdl::iomem::VTD_MAX_ADDR {
+                    return Err(
+                        format!(
+                            "Error: iomap for '{}' has address 0x{:x} which exceeds the upper limits of {} in {} '{}' @ {}",


midnightveil · 2026-04-16T07:47:07Z

            },
            ObjectType::AsidPool => Some(object_sizes.asid_pool),
+            ObjectType::IOPageTable => Some(12),
+            // It would be best to avoid such catch all case so people might forget to add the size of new object type here.


Fix it or make an issue I think

midnightveil · 2026-04-16T07:47:17Z

@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW.


midnightveil · 2026-04-16T07:47:45Z

@@ -68,7 +68,7 @@
    "KernelPlatform": "pc99",
    "KernelX86MicroArch": "generic",
    # See https://github.com/seL4/microkit/issues/418 for details.


remove this comment if its solved

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Cheng-Li1 added 12 commits April 9, 2026 13:25

Incomplete support for VTD in microkit tool.

0e3dc58

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Finish the first iteration of the implementation.

48b37e0

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Tool can output correct specs in tried (limited) tests.

726cb26

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

iommu works for blk exampl on x86 qemu.

704a361

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Check whether IOMMU is enabled in Kernel Config.

2dc4f59

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Add config and memory region sanity checks.

cac9f93

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Use the three-level VTD PD structure instead of the four-level struct…

bdf848f

…ure for generating spec in microkit tool. Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Change the code back to default for four level VTD page table.

e63fbac

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Add check to make sure the io addresses are in valid range. Refine th…

72abe79

…e check unused mr and mr page size optimization logic for iomaps support. Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Add perms and setvar for iomap.

17d4374

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Remove unused code.

62eb4cc

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Enable x86 iommu in build_sdk.py.

6d880c9

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

dreamliner787-9 reviewed Apr 16, 2026

View reviewed changes

midnightveil reviewed Apr 16, 2026

View reviewed changes

Improve code.

bd75a2f

Signed-off-by: Cheng Li <cheng.li10@unsw.edu.au>

Conversation

Cheng-Li1 commented Apr 10, 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!

dreamliner787-9 Apr 16, 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!

dreamliner787-9 commented Apr 16, 2026

Uh oh!

dreamliner787-9 commented Apr 16, 2026

Uh oh!

midnightveil left a comment

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

dreamliner787-9 Apr 16, 2026 •

edited

Loading