Add iommu support for capdl initializer and sel4 crate by Cheng-Li1 · Pull Request #337 · seL4/rust-sel4

Cheng-Li1 · 2026-04-10T08:24:42Z

This pull request adds functionalities to the capdl initializer and the sel4 crate.

Added functionalities include:

Functions to invoke the mapping of the page table and frame into device iospace.
Objects and structs used for iommu support.
Parsing the spec from Microkit and doing the actual mapping of frame and io page table.

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

lsf37 · 2026-04-10T08:30:44Z

Are there any updates necessary for the code, model, and spec/docs in the capDL repo? https://github.com/seL4/capdl/

(We don't want the feature set of these tools to diverge, the whole point of capDL is to provide the same interface to multiple backends).

midnightveil · 2026-04-16T06:57:22Z

+            // Reuse sel4::vspace_levels::step_bits
+            let ioaddr = ioaddr + (usize::from(i) << sel4::vspace_levels::step_bits(level));


Is this actually correct? Do the IO PT level bits always match the SW PT level bits?

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

+                    self.orig_cap::<cap_type::IOPageTable>(cap.object)
+                        .io_page_table_map(iospace, ioaddr)?;
+                    let obj = self.object_as::<object::ArchivedIOPageTable>(cap.object);
+                    self.init_iospace(iospace, level + 1, ioaddr, obj)?;


This seems inefficient, to set up a page table you're going to do a full walk from level 0 -> end for each frame. Surely a level-order walk of the tree makes more sense here?

Also, am I blind, or does the existing capDL loader C version not support IOMMU at all? It has IOPT in the specification but I can't see any kind of equivalent for IOMMU in there? I was trying to see how it did it.

I am not sure whether there is a huge difference between breadth-first search(I guess BFS is what you mean by level-order walk?) and depth-first search(what is implemented here) when recursion is used. Depth-first search is easier to implement, and we know the maximum number of recursions (since the maximum page table level is four). DFS is also used in init_vspace(). There might be a way to optimize the process further(using iterative traversal with a parent pointer so we do not need to use recursion), but it would be better to leave optimization to a different PR.

And yes, I think the C version of the capdl loader does not support IOMMU.

I believe I slightly misunderstood the code here: the object is changing (rather than just the new value being an argument), so there's some subtle control flow. Presumably the spec containing all the objects is already in the order so that you can walk the tree once in order.

(It's not a DFS vs BFS thing here at all: we aren't doing a search. A level-order walk is it's own thing, separate to DFS vs BFS. But actually, a preorder walk like you do is fine).

And yes, I think the C version of the capdl loader does not support IOMMU.

Yes, it only has some code for SMMU, but nothing for VT-d.

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

+        pub pci_bus: u8,
+        pub pci_device: u8,
+        pub dev_func: u8,
+        pub domain_id: u16,


These are x86-specific. I don't know how rust-seL4 does this but they should be as part of some kind of arch-specific data.

midnightveil · 2026-04-16T07:11:08Z

+                match &entry.cap {
+                    ArchivedCap::IOPageTable(cap) => IOPageTableEntry::IOPageTable(cap),
+                    ArchivedCap::Frame(cap) => IOPageTableEntry::Frame(cap),
+                    _ => panic!(),


panic! without a message seems silly.

maybe:

Suggested change

_ => panic!(),

_ => unreachable!("non-IO-PT cap in IO-PT"),

midnightveil · 2026-04-16T07:12:05Z

        (IO_PORT_CONTROL, IOPortControl, seL4_CapIOPortControl),
-        #[cfg(false)] // TODO
-        (IO_SPACE, Null, seL4_CapIOSpace),
+        #[sel4_cfg(all(ARCH_X86_64, IOMMU))] // TODO


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

+        pub is_root: bool,
+        pub level: Option<u8>,


Why is this Option<u8>? Why would a page table not have a level.
Also, isn't is_root <=> (level == 0)?

midnightveil · 2026-04-16T07:20:58Z

+        const DEVICE_ID_SHIFT: u16 = 3;
+        const PCI_ID_SHIFT: u16 = DEVICE_ID_SHIFT + 5;
+        const DOMAIN_ID_SHIFT: u16 = PCI_ID_SHIFT + 8;


Is this arbitrary or derived from something?

midnightveil · 2026-04-16T07:22:05Z

+                    panic!(
+                        "The hardware does not support three level VTD Page Table, but {} level is provided",
+                        level


Suggested change

panic!(

"The hardware does not support three level VTD Page Table, but {} level is provided",

level

panic!(

"The hardware page table has {level} levels which we do not support",

level

midnightveil · 2026-04-16T07:23:50Z

+            // There is no way to determine the level of io page table before actually running it on hardware
+            // So there is no way to allocate the correct number of slots
+            // Thus we default to assume the four level page table structure
+            match level {
+                // If three level page table is chosen by seL4, we skip mapping the root page table in
+                // Current approach wastes the memory root page table object
+                VTD_THREE_LEVEL_PT => {
+                    self.init_iospace(iospace_cap, root_level, 0, root_pt)?;
+                }
+                VTD_FOUR_LEVEL_PT => {
+                    self.orig_cap::<cap_type::IOPageTable>(iospace.slots[0].cap.obj())
+                        .io_page_table_map(iospace_cap, 0)?;
+                    self.init_iospace(iospace_cap, root_level, 0, root_pt)?;


I'm confused. Assuming the four-level page table structure seems like it wouldn't work.

Wouldn't it make more sense to assume the three-level page table structure, and just have an extra top-level table for the four-level page table structure?

That way, when you have 3 levels, you use the 3 levels, but when you have 4, you basically just use 3 levels, and have a top-level page table that just maps the lower 3 in the lowest entry, say.

(Also, these sentences need to be reworked, the grammar is awful and doesn't make any sense)

midnightveil · 2026-04-16T07:25:10Z

+            let badge = ((iospace.pci_bus as u64) << PCI_ID_SHIFT)
+                + ((iospace.pci_device as u64) << DEVICE_ID_SHIFT)
+                + iospace.dev_func as u64
+                + ((u16::from(iospace.domain_id) as u64) << DOMAIN_ID_SHIFT) as u64;


ditto with x86-specificness.

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

Are there any updates necessary for the code, model, and spec/docs in the capDL repo? seL4/capdl
(We don't want the feature set of these tools to diverge, the whole point of capDL is to provide the same interface to multiple backends).

The spec in the capDL tool seems to support an 'IOPT' and an 'IODevice' (not in this PR at all? it seems to contain the pci bus + domain that the IOPT does here...), but we can't see any implementation of say init_iospaces that initialises them in the loader.

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com> Fix typo. Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems> Signed-off-by: Cheng Li <53856318+Cheng-Li1@users.noreply.github.com> Remove unnecessary debug prints. Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

lsf37 reviewed Apr 10, 2026

View reviewed changes

Comment thread crates/sel4-capdl-initializer/src/initialize.rs Outdated

Cheng-Li1 force-pushed the cheng/iommu_support branch 3 times, most recently from 87f4ad3 to 70bb0a9 Compare April 15, 2026 05:46

midnightveil reviewed Apr 16, 2026

View reviewed changes

Cheng-Li1 added 9 commits May 7, 2026 13:17

Add invocations needed for iommu to sel4 crate

e052f94

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Working on IOMMU support on Capdl Initializer

47d23f0

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Change the IOSpace struct

c2fd7bd

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Iommu works for blk exampl on x86 qemu

ea317bc

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Add support for different levels of VTD PT

33d2d80

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Default to parse the three-level VTD PT

63d0ce3

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Revert to default to four level VTD PT

9f49b02

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Add cfg checks to fix compliation errors

0275a4d

Signed-off-by: Cheng Li <lichengchaoreng@gmail.com>

Cheng-Li1 force-pushed the cheng/iommu_support branch from 70bb0a9 to 3b4a5ff Compare May 7, 2026 03:19

		// Reuse sel4::vspace_levels::step_bits
		let ioaddr = ioaddr + (usize::from(i) << sel4::vspace_levels::step_bits(level));

Uh oh!

Conversation

Cheng-Li1 commented Apr 10, 2026

Uh oh!

lsf37 commented Apr 10, 2026

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!

midnightveil May 26, 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

midnightveil commented Apr 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

midnightveil May 26, 2026 •

edited

Loading