IOMMU: Add SDF Support

docs/manual.md

@@ -109,6 +109,7 @@ This document attempts to clearly describe all of these terms, however as the co
 * [interrupt](#irq)
 * [fault](#fault)
 * [ioport](#ioport)
+* [io address space](#io_address_space)
 
 ## System {#system}
 
@@ -242,6 +243,13 @@ The mapping has a number of attributes, which include:
 * caching attributes (mostly relevant for device memory)
 * 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
+a number of attributes, which include:
+
+* the io virtual address at which the region is mapped in the io address space
+* permissions (read, write)
+
 **Note:** When a memory region is mapped into multiple protection
 domains, the attributes used for different mappings may vary.
 
@@ -356,6 +364,12 @@ delivered to another PD, the fault being handled depends on when the parent PD i
 
 I/O ports are x86 mechanisms to access certain physical devices (e.g. PC serial ports or PCI) using the `in` and `out` CPU instructions. The system description specifies if a protection domain have access to certain port address ranges. These accesses will be executed by seL4 and the result returned to protection domains.
 
+## IO Address Spaces {#io_address_space}
+
+IO Address Spaces provide a way to isolate device memory accesses within a fixed virtual address space. The isolation provided by the address space is enforced by the underlying hardware IOMMU or SMMU.
+
+IO Address Spaces allow *memory regions* to be mapped to a provided base IO virtual address. These IO virtual addresses will be translated by the hardware IOMMU or SMMU to the underlying physical memory that backs the memory region.
+
 # SDK {#sdk}
 
 Microkit is distributed as a software development kit (SDK).
@@ -1056,6 +1070,23 @@ See the 'cap_sharing' example packaged in your SDK or [on GitHub](https://github
 All capability elements (currently) all support the `pd` attribute, the name of the protection domain that the capability is from.
 For instance, `<cap_tcb slot="1" pd="alpha">` will place the TCB of PD 'alpha' in the CSpace of the current PD.
 
+## `io_address_space`
+
+The `io_address_space` element describes an address space used to isolate a given device.
+
+It supports the following attributes:
+* `name`: A unique name for the io address space
+* `peripheral_id`: A unique identifier. This must match the identifier used by the hardware IOMMU or SMMU to identify devices.
+
+The `io_address_space` element supports the following elements as children:
+
+* `iomap`: This is used to map a *memory_region* into the io address space.
+
+The `iomap` element supports the following attributes:
+* `mr`: Identifies the memory region to map.
+* `iovaddr`: Identifies the io virtual address at which to map the memory region.
+* `perms`: Identifies the permissions with which to map the memory region. Can be a combination of `r` (read), and `w` (write).
+           Defaults to read-write.
 
 ### Page sizes by architecture
 

example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.system

@@ -0,0 +1,20 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <memory_region name="edu_mmio_window" size="0x10_0000" page_size="0x1000" phys_addr="0xfe00_0000" />
+    <memory_region name="dma_buffer" size="0x1000" page_size="0x1000" />
+    <io_address_space name="QEMU EDU" peripheral_id="0:4.0">
+        <iomap mr="dma_buffer" iovaddr="0x10_0000" />
+    </io_address_space>
+
+    <protection_domain name="x86_64_iommu_dma_test" priority="100">
+        <program_image path="x86_64_iommu_dma_test.elf" />
+        <map mr="edu_mmio_window" vaddr="0x2000_0000" perms="rw" cached="false" setvar_vaddr="edu_mmio_window_vaddr" />
+        <map mr="dma_buffer" vaddr="0x3000_0000" perms="rw" cached="true" setvar_vaddr="dma_buffer_vaddr" />
+        <ioport id="0" addr="0xcf8" size="8" setvar_id="pci_config_ioport_id" />
+    </protection_domain>
+</system>

tool/microkit/src/capdl/irq.rs

@@ -86,18 +86,14 @@ fn create_irq_obj(
             }),
         }),
         SysIrqKind::MSI {
-            pci_bus,
-            pci_dev,
-            pci_func,
-            handle,
-            ..
+            pci_device, handle, ..
         } => Object::IrqMsi(object::IrqMsi {
             slots: [].to_vec(),
             extra: Box::new(object::IrqMsiExtraInfo {
                 handle: Word(handle),
-                pci_bus: Word(pci_bus),
-                pci_dev: Word(pci_dev),
-                pci_func: Word(pci_func),
+                pci_bus: Word(pci_device.bus as u64),
+                pci_dev: Word(pci_device.device as u64),
+                pci_func: Word(pci_device.function as u64),
             }),
         }),
     };

tool/microkit/src/main.rs

@@ -210,6 +210,11 @@ fn main() -> Result<(), String> {
         _ => false,
     };
 
+    let iommu = match arch {
+        Arch::X86_64 => json_str_as_bool(&kernel_config_json, "IOMMU")?,
+        _ => false,
+    };
+
     let arm_pa_size_bits = match arch {
         Arch::Aarch64 => {
             if json_str_as_bool(&kernel_config_json, "ARM_PA_SIZE_BITS_40")? {
@@ -248,6 +253,7 @@ fn main() -> Result<(), String> {
             "MAX_NUM_BOOTINFO_UNTYPED_CAPS",
         )?,
         hypervisor,
+        iommu,
         benchmark: args.config == "benchmark",
         num_cores: if json_str_as_bool(&kernel_config_json, "ENABLE_SMP_SUPPORT")? {
             json_str_as_u64(&kernel_config_json, "MAX_NUM_NODES")?