IOMMU: Add IOMMU Support by cazb2 · Pull Request #358 · seL4/rust-sel4

cazb2 · 2026-07-08T02:59:10Z

This commit adds support for the creation of IOMMU address spaces on x86.

The capdl spec for defining an IO Address Space on x86 is a root IODevice object, which contains in slot 0 the root IOPageTable object and in slots 1.. spare IOPageTable objects. These IOPageTable objects are similar to the normal x86 page table structures.

At runtime, the initialiser will calculate how many of the spare page tables must be mapped. It does this by taking the difference of what seL4 reports to be the number of page table levels and the configured number of levels we define in the x86_io_address_space module.

This means that capdl enforces a fixed upper limit on the maximum IO virtual address and will fail if seL4 reports that the IOMMU supports less than this maximum. If seL4 reports support for a larger maximum IO virtual address, this design works by mapping in the spare page tables into the highest levels of the hierarchy in slot 0, until we reach the page table responsible for translating the first valid bits of the maximum IO virtual address.

midnightveil · 2026-07-08T07:33:59Z

+        for entry in obj.slots.iter() {
+            let entry_ioaddr = ioaddr + (usize::from(entry.slot) << shift);


Please follow init_vspace if you can; I suspect this should be for (i, entry) in obj.entries().

Equivalent, but will update.

midnightveil · 2026-07-08T07:37:30Z

+            );
+        }
+
+        let runtime_level = iopt_level + prefix_depth;


I need to think about this prefix a bit more, FWIW.

It's not immediately obvious from the code how this works, so it would be a good idea to include your motivation from the PR description as a comment here.

I do have a question though: how are the levels encoded in the spec, as who defines "Level = 0 => top of the page table"?

Obviously there's a mismatch here somewhere, but I'm not clear on precisely where it is.

// Level is zero indexed in the spec.

This comment to me seems to imply that the spec always starts the levels from 0.

And how is this not an issue for the VSpace? seL4 has similar behaviour; for AARch64-hyp with PASize=40 it's 3-level, but for AArch64-hyp with PASize>=44 it's 4-level, so I don't see why IOMMU would be special in this case (where special = extra behaviour not needed for vspace).

@nspin How does your VSpace code handle PASize=40 (num_levels=3) on AArch64? (AARCH64_VSPACE_S2_START_L1 in seL4 and this relevant discussion here).

Yep, the difference is the IODevice (which is the IOSpace) object. For a normal address space it would be the vspace that consumes 4KiB and acts as the root of the translation table. But for IOMMU the IOSpace is meagrely a capability i.e. it's a fake kernel object. The root of translation is the actually the first IOPT that gets mapped in.

I don't know if this is the same as the hypervisor, I would be surprised...

I think I simplified it:)

midnightveil

I'm happy with this now, until the kernel changes (seL4/seL4#1703) go through.

Waiting on @nspin review.

dreamliner787-9 · 2026-07-10T00:52:59Z

+    }
+
+    #[sel4::sel4_cfg(all(ARCH_X86_64, IOMMU))]
+    fn init_iopt_tree(


I think the *_tree postfix is a bit out of place compared to similar functions like init_vspace_x86_ept() and init_vspace(). I feel like this should be called init_iospace().

dreamliner787-9 · 2026-07-10T00:53:37Z

+    pub struct IODevice {
+        pub slots: Vec<CapTableEntry>,
+        pub domain_id: Word,
+        pub pci_device: (Word, Word, Word),


I know that it is obvious but:

Suggested change

pub pci_device: (Word, Word, Word),

pub pci_device: (Word, Word, Word), // bus:device.function

for folks who aren't familliar

Or make it into a struct

I think this matches the capDL spec, I don't know to what extend it can differ. (might be wrong here)

seL4/capdl#90 is the part it would have to match, and that new module is (a) not yet upstreamed and (b) doesn't have IOMMU support yet anyways. So this PR can define what that part of the spec should look like.

midnightveil · 2026-07-10T02:07:05Z

+        // since this is runtime information. The second is the spec assumes that all domain ids are
+        // valid, which is also not true since the kernel may reserve an unknown number of domain
+        // ids during boot.
+        let [cap_data] = sel4::sys::seL4_X86_IOSpace_CapData::new(


I suspect you might want to make this a bit nicer. Have a look at what Nick did for 'CNodeCapData' and where it is used with syscalls.

I think the change I made with to_sel4 could easily generalise, so a macro would be cool... I didn't implement it here though.

nspin

Thanks for this. Just a few comments, mostly nits.

nspin · 2026-07-10T08:25:05Z

+    pub struct IODevice {
+        pub slots: Vec<CapTableEntry>,
+        pub domain_id: Word,
+        pub pci_device: (Word, Word, Word), // bus:device.function


Could you change this to be a struct?

That would also eliminate the need for trait ToSel4.

yep, so we don't have to match the C/haskell spec identically, which represents this as a tuple?

X-ref: #358 (comment)

@nspin, apologies it looks like you might have missed this one, we just wanted to confirm whether its necessary to match how the C/haskell implementation defined these types. (I doesn't look like there is a full implementation in the C/haskell yet...)

I agree having this as a structure would be way better if its allowed :)

Answered here: #358 (comment)

Ty for the clarification below :)

nspin · 2026-07-10T08:27:42Z

    PageTable(object::PageTable),
    AsidPool(object::AsidPool),
+    IODevice(object::IODevice),
+    IOPT(object::IOPT),


Could you expand IOPT to IOPageTable? Just to match the convention of the surrounding code.

Just to confirm, so rust sel4 naming doesn't need to correspond to the c/haskell capdl?

Not the main part of the Haskell CapDL tool. Just this part:

seL4/capdl#90

which doesn't have IOMMU support yet. So no need to worry about matching, this PR will determine with the JSON spec looks like.

nspin · 2026-07-10T08:29:58Z

+            ))
+        }
+
+        pub fn new_from_pci_tuple(domain_id: Word, pci_device: (Word, Word, Word)) -> Self {


Is a tuple much better than three arguments? This could be a structured type, and could be the target of a .to_sel4() method of a corresponding structured type in sel4-capdl-initializer-types.

Yeah fair, I simplified it to the interface to just the three arg new :)

nspin · 2026-07-10T08:30:41Z

    }
+
+    #[sel4_cfg(IOMMU)]
+    pub const fn from_level_iopt(_level: usize) -> Option<Self> {


Could you expand this to from_level_io_page_table?

nspin · 2026-07-10T08:34:46Z

        Ok(())
    }

+    fn init_iospaces(&mut self) -> Result<()> {


I think it might be cleaner to #[cfg] this method and then sel4_cfg_if its invocation above, like init_sched_contexts does.

yep, will change it for now, but in future if SMMU support, (the ARM version), is added some form of Arch ifdef will be needed...

nspin · 2026-07-10T08:37:25Z

+        match dst.mint(&src, CapRights::all(), cap_data.into()) {
+            Ok(_) => Ok(self.orig_cap::<cap_type::IOSpace>(obj_id)),
+            Err(err) => {
+                panic!("Error: {err} when minting an x86 IOSpace capability.")
+            }
+        }


This might read more cleanly with unwrap_or_else(|err| ...) rather than a match.

nspin · 2026-07-14T06:45:49Z

    PageTable(object::PageTable),
    AsidPool(object::AsidPool),
+    IODevice(object::IODevice),
+    IOPT(object::IOPT),


Not the main part of the Haskell CapDL tool. Just this part:

seL4/capdl#90

which doesn't have IOMMU support yet. So no need to worry about matching, this PR will determine with the JSON spec looks like.

nspin · 2026-07-14T06:46:13Z

+    pub struct IODevice {
+        pub slots: Vec<CapTableEntry>,
+        pub domain_id: Word,
+        pub pci_device: (Word, Word, Word), // bus:device.function


Answered here: #358 (comment)

This commit adds support for the creation of IOMMU address spaces on x86. The capdl spec for defining an IO Address Space on x86 is a root IOSpace object, which contains in slot 0 the root IOPageTable object and in slots 1.. spare IOPageTable objects. These IOPageTable objects are similar to the normal x86 page table structures. At runtime, the initialiser will calculate how many of the spare page tables must be mapped. It does this by taking the difference of what seL4 reports to be the number of page table levels and the configured number of levels we define in the x86_io_address_space module. This means that capdl enforces a fixed upper limit on the maximum IO virtual address and will fail if seL4 reports that the IOMMU supports less than this maximum. If seL4 reports support for a larger maximum IO virtual address, this design works by mapping in the spare page tables into the highest levels of the hierarchy in slot 0, until we reach the page table responsible for translating the first valid bits of the maximum IO virtual address. Signed-off-by: Callum <c.berry@student.unsw.edu.au>

cazb2 requested a review from nspin as a code owner July 8, 2026 02:59

cazb2 force-pushed the callumb_and_cheng/iommu_capdl_support branch 3 times, most recently from 5770590 to 91d501c Compare July 8, 2026 03:20

midnightveil mentioned this pull request Jul 8, 2026

Add iommu support for capdl initializer and sel4 crate #337

Closed

cazb2 force-pushed the callumb_and_cheng/iommu_capdl_support branch from 91d501c to db76418 Compare July 8, 2026 03:44