Skip to content

IOMMU: Add SDF Support#528

Open
cazb2 wants to merge 9 commits into
seL4:mainfrom
au-ts:callumb_and_cheng/sdf_iommu_support
Open

IOMMU: Add SDF Support#528
cazb2 wants to merge 9 commits into
seL4:mainfrom
au-ts:callumb_and_cheng/sdf_iommu_support

Conversation

@cazb2

@cazb2 cazb2 commented Jun 18, 2026

Copy link
Copy Markdown
Contributor

This commit adds iommu support to microkit sdfs.

Define a constant to represent the a tool enforced limitation on the maximum virtual address suported for an IO address space. This is due to current x86 IOMMU behaviour in the kernel which dynamically detects the maximum virtual address for an IO address space. For more info read: BOOT_CODE bool_t vtd_init_num_iopts(uint32_t num_drhu) in seL4/src/plat/pc99/machine/intel-vtd.c.

Add PciDevice struct and PCIDeviceParseError enum. This types allow us to implement the Display trait which gives a consistent way to output PCI information. The FromStr trait implemented for PCIDevice avoid duplicating logic required to parse the PCI identifier from the xml. When combined with the display trait on the PCIDeviceParseError, we get consistent error messages and avoid repeating code.

Add IOMMUDeviceIdentifier and IOMMUDeviceIdentifierParseError to support parsing the sdf based on the current architecture. This allows the sdf parsing to easily support ARM SMMU and RISCV IOMMU. The Display traits again remove repeated code when outputting IOMMUDeviceIdentifer or IOMMUDeviceIdentifierParseError, particularly useful for error messages.

Add SysIOMapPerms. Representing the perms in an enum completely removes the existence of invalid IOMapPerms once we parse the sdf.

Add SysIOMap. The dual to SysMap, used to represent a mapping in a devices IO virtual address space.

Replace ExecutionContext trait with a Map trait. The previous trait was primarily used in the check_maps function to handle memory regions in virtual machines and normal pds. This Map trait allowed the one check_maps function to handle both SysIOMaps and SysMaps uniformly. The additional information that was provided by the polymorhpic ExecutionContext is just passed as a string to be used in the respective error message. This is because outside of the check_maps function a protection_domain and a virtual_machine are handled as distinct types.

Add error checking cases to check_maps. If the map_start + mr.size overflows alot of the pre-exisiting logic breaks so check for it. Also check that we don't overflow the top of user_virtual memory accouting for the differences between protection_domains, virtual_machines and io address spaces.

Add check_io_maps adapter. Required because check_maps is designed to error check within one address space. Therefore we collect all the mappings that have been made on a per IO address space basis.

capdl/irq.rs waas using the old pci_bus,pci_dev,pci_func form. Since we have a real type now, we updated the expected match form.

@midnightveil

Copy link
Copy Markdown
Collaborator

For comparison's sake: #467.

@midnightveil midnightveil linked an issue Jun 18, 2026 that may be closed by this pull request
@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from 617dcab to dc2bb15 Compare June 18, 2026 02:36

@midnightveil midnightveil left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, so so far this is good :)

There's a few relatively minor changes, but I think I'm happy with this format in the SDF.

I don't know if you've yet to do it, but documentation in the manual would be good.

(also like the rest of the implementation, ha).

Comment thread tool/microkit/src/sdf.rs Outdated
Comment thread tool/microkit/src/sdf.rs Outdated
Comment thread tool/microkit/src/sdf.rs
Comment thread tool/microkit/src/sdf.rs
Comment thread tool/microkit/src/sdf.rs
Comment thread tool/microkit/src/sdf.rs Outdated
Comment thread tool/microkit/src/sdf.rs Outdated
Comment thread tool/microkit/src/sdf.rs
@cazb2

cazb2 commented Jun 18, 2026

Copy link
Copy Markdown
Contributor Author

OK, so so far this is good :)

There's a few relatively minor changes, but I think I'm happy with this format in the SDF.

I don't know if you've yet to do it, but documentation in the manual would be good.

(also like the rest of the implementation, ha).

Yep, I thought it would be easier to make a few smaller PRs rather than one big one.

@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch 6 times, most recently from 2d6348c to 6871f48 Compare June 18, 2026 05:13
@midnightveil

Copy link
Copy Markdown
Collaborator

Ok, last thing:

Can you add this sort of check?

if !config.hypervisor {
return Err(value_error(
xml_sdf,
node,
"seL4 has not been built as a hypervisor, virtual machines are disabled".to_string()
));
}

So that until the IOMMU is enabled by default it should be impossible to make these.

(It will be based off the KernelHaveIOMMU define, like for hypervisor).

@cazb2 cazb2 marked this pull request as ready for review June 18, 2026 06:28
@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from 7082a72 to b157ad0 Compare June 18, 2026 06:40
@midnightveil

Copy link
Copy Markdown
Collaborator

Note: this is pending follow-up PRs for functionality, to be merged as a group.

Comment thread docs/manual.md Outdated
* permissions (read, write and execute)

*Note:* On x86 a memory region can also be *mapped* into one or more
io address spaces. This type of mapping is known as an *iomap*. It supports

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
io address spaces. This type of mapping is known as an *iomap*. It supports
IO address spaces. This type of mapping is known as an *iomap*. It supports

Can you please capitalise this since it's an abbreviation, need to be done elsewhere in the manual too, but leave io_address_space as is.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should be done now

@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch 4 times, most recently from 43b0567 to dd66aeb Compare July 8, 2026 01:05
@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch 4 times, most recently from 5e715bd to dfc3853 Compare July 9, 2026 23:50
cazb2 added 2 commits July 10, 2026 10:52
Hex formatting.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
Replace ExecutionContext trait with a Map trait. The previous trait was
primarily used in the check_maps function to handle memory regions in
virtual machines and normal pds. This Map trait will allow the one
check_maps function to handle both SysIOMaps and SysMaps uniformly. The
additional information that was provided by the polymorhpic
ExecutionContext is just passed as a string to be used in the respective
error message. This is because outside of the check_maps function a
protection_domain and a virtual_machine are handled as distinct types.

Add error checking cases to check_maps. If the map_start + mr.size
overflows alot of the pre-exisiting logic breaks so check for it. Also
check that we don't overflow the top of user_virtual memory accouting
for the differences between protection_domains, virtual_machines and io
address spaces.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
cazb2 added 6 commits July 10, 2026 10:52
Add PciDevice struct and PCIDeviceParseError enum. This types allow us
to implement the Display trait which gives a consistent way to output
PCI information. The FromStr trait implemented for PCIDevice avoid
duplicating logic required to parse the PCI identifier from the xml.
When combined with the display trait on the PCIDeviceParseError, we get
consistent error messages and avoid repeating code.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
This commit adds iommu support to microkit sdfs.

Define a constant to represent the a tool enforced limitation on the
maximum virtual address suported for an IO address space. This is due to
current x86 IOMMU behaviour in the kernel which dynamically detects the
maximum virtual address for an IO address space.  For more info read:
BOOT_CODE bool_t vtd_init_num_iopts(uint32_t num_drhu) in
seL4/src/plat/pc99/machine/intel-vtd.c.

Add IOMMUDeviceIdentifier and IOMMUDeviceIdentifierParseError to support
parsing the sdf based on the current architecture. This allows the sdf
parsing to easily support ARM SMMU and RISCV IOMMU. The Display traits
again remove repeated code when outputting IOMMUDeviceIdentifer or
IOMMUDeviceIdentifierParseError, particularly useful for error messages.

Add SysIOMapPerms. Representing the perms in an enum completely removes
the existence of invalid IOMapPerms once we parse the sdf.

Add SysIOMap. The dual to SysMap, used to represent a mapping in a
devices IO virtual address space.

Add check_io_maps adapter. Required because check_maps is designed to
error check within one address space. Therefore we collect all the
mappings that have been made on a per IO address space basis.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
Update the manual to include IOMMU information.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
Ensure that the sel4::Config struct has the
iommu flag asserted, indicating the kernel was
built with IOMMU support. If not we fail parsing any
io address space elements encountered in the sdf.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
Address Feedback from Bill.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
Fix a test that was assuming a fixed max virtual address.

Instead make the memory region large enough that it will be out of
bounds on any realistic max virtual address reported by seL4 via
user_top().

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from dfc3853 to 7070554 Compare July 10, 2026 00:52
Comment thread docs/manual.md
@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from 7070554 to d13bf6b Compare July 10, 2026 01:12

@midnightveil midnightveil left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since you have commits in here that are a refactoring I have to review this at a per-commit level. However, as it stands you have fixup commits that have been added later that mean you change earlier code added. I'd appreciate if you cleaned up the commit history so that each change is standalone and you don't go back and change things you just added. You now have commits that contain changes of several previous commits.

Comment thread tool/microkit/src/sdf.rs Outdated
// that they do not have any IOVA to physyical address mappings that conflict, and that they share the same
// IOPT objects, this because the source identifier aka the PCI BDF is not used in all caches.
// See section 6.2.1 and table 17 in the intel VT-D manual.
// https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://cdrdv2-public.intel.com/671081/vt-directed-io-spec.pdf&ved=2ahUKEwiN_YawksWVAxUDmFYBHfzzCEQQFnoECA0QAQ&usg=AOvVaw3fO9wnba58SqsP2HNKwdfu

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please don't link a google link. Link the static Intel page and the full name of the manual.

Comment thread tool/microkit/src/sdf.rs Outdated
));
}

// In microkit enforcing uniqueness for domain ids is hugely simplifying and enforces better designs.

@midnightveil midnightveil Jul 10, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please be a bit more formal with your comments. These sentences are very long and run on and could be a bit more brief.

@cazb2

cazb2 commented Jul 10, 2026

Copy link
Copy Markdown
Contributor Author

Since you have commits in here that are a refactoring I have to review this at a per-commit level. However, as it stands you have fixup commits that have been added later that mean you change earlier code added. I'd appreciate if you cleaned up the commit history so that each change is standalone and you don't go back and change things you just added. You now have commits that contain changes of several previous commits.

Right my bad. All new code from when it was reviewed previously is in separate commits from capitalising IO in the manual to the domain ID support. I haven't changed any of the previously reviewed commits but I get what you mean about GitHub being a pain for looking at individual commits.

Add domain ids to microkit system descriptions.

Signed-off-by: Callum <c.berry@student.unsw.edu.au>
@cazb2 cazb2 force-pushed the callumb_and_cheng/sdf_iommu_support branch from d13bf6b to ad35214 Compare July 10, 2026 07:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Support IOMMU on x86-64

3 participants