From b3191719def78e5fc2823e2a5be5cde3ab8301fd Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 13:06:29 +1000 Subject: [PATCH 1/3] IOMMU: Add IOMMU helper to config This commit adds a helper to extract the io page table index bits from the config. This currently only supports a IOMMU build on x86. Signed-off-by: Callum --- tool/microkit/src/sel4.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 2868c2871..b2e4439ab 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -425,6 +425,19 @@ impl Config { self.address_space_constants.page_table_index_bits } } + + pub fn io_page_table_index_bits(&self) -> u64 { + match (self.arch, self.iommu) { + (Arch::X86_64, true) => self + .address_space_constants + .io_page_table_index_bits + .expect( + "Error: An x86 VT-D build should have seL4_IOPageTableIndexBits + defined by seL4, captured in tool/microkit/address_space_constants.h", + ), + _ => panic!("Error: currently not supported by Microkit."), + } + } } #[derive(PartialEq, Clone, Copy, Eq)] From e80afdc315a812a89f4b137f25de0e9f48b0b91b Mon Sep 17 00:00:00 2001 From: Callum Date: Tue, 7 Jul 2026 10:22:32 +1000 Subject: [PATCH 2/3] IOMMU: Add backend support for IOMMU This commit implements support for the x86 IOMMU Capdl spec. The memory module is extended to allow for the construction of IOMMU address spaces. The Capdl spec refers to the IOSpace object as the IODevice object and the IO Page tables as IOPTs. Within microkit we use IOSpace to refer to the whole IO address space. It also provides an example using the qemu dma capable test device, demonstrating the use of the IOMMU. Note we did not need to provide physical memory addresses for any dma buffers, proving the IOMMU correctly translated our requests. Signed-off-by: Callum --- .github/workflows/sdk.yaml | 0 Cargo.lock | 60 ++--- Cargo.toml | 8 +- build_sdk.py | 3 +- example/x86_64_iommu_dma_test/Makefile | 72 ++++++ example/x86_64_iommu_dma_test/README.md | 25 ++ .../x86_64_iommu_dma_test.c | 234 ++++++++++++++++++ tool/microkit/src/capdl/builder.rs | 47 +++- tool/microkit/src/capdl/memory.rs | 127 +++++++++- tool/microkit/src/capdl/spec.rs | 5 + tool/microkit/src/sdf.rs | 20 +- tool/microkit/src/sel4.rs | 6 + tool/microkit/src/viper.rs | 2 + tool/microkit/tests/test.rs | 1 + 14 files changed, 551 insertions(+), 59 deletions(-) create mode 100644 .github/workflows/sdk.yaml create mode 100644 example/x86_64_iommu_dma_test/Makefile create mode 100644 example/x86_64_iommu_dma_test/README.md create mode 100644 example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c diff --git a/.github/workflows/sdk.yaml b/.github/workflows/sdk.yaml new file mode 100644 index 000000000..e69de29bb diff --git a/Cargo.lock b/Cargo.lock index 744b0db89..dfb1bb2f4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -439,7 +439,7 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "sel4" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "cfg-if", "sel4-config", @@ -449,7 +449,7 @@ dependencies = [ [[package]] name = "sel4-alloca" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "cfg-if", ] @@ -457,7 +457,7 @@ dependencies = [ [[package]] name = "sel4-bitfield-ops" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "rustversion", ] @@ -465,12 +465,12 @@ dependencies = [ [[package]] name = "sel4-build-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-capdl-initializer" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "log", "rkyv", @@ -488,7 +488,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "miniz_oxide", "rkyv", @@ -500,7 +500,7 @@ dependencies = [ [[package]] name = "sel4-capdl-initializer-types-derive" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "proc-macro2", "quote", @@ -510,7 +510,7 @@ dependencies = [ [[package]] name = "sel4-config" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "prettyplease", "proc-macro2", @@ -524,7 +524,7 @@ dependencies = [ [[package]] name = "sel4-config-data" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "sel4-build-env", "sel4-config-types", @@ -534,7 +534,7 @@ dependencies = [ [[package]] name = "sel4-config-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "fallible-iterator", "proc-macro2", @@ -547,7 +547,7 @@ dependencies = [ [[package]] name = "sel4-config-types" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "serde", ] @@ -555,12 +555,12 @@ dependencies = [ [[package]] name = "sel4-ctors-dtors" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-dlmalloc" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "dlmalloc", "lock_api", @@ -569,17 +569,17 @@ dependencies = [ [[package]] name = "sel4-immediate-sync-once-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-immutable-cell" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-initialize-tls" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "cfg-if", "sel4-alloca", @@ -588,7 +588,7 @@ dependencies = [ [[package]] name = "sel4-logging" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "lock_api", "log", @@ -597,12 +597,12 @@ dependencies = [ [[package]] name = "sel4-no-allocator" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-panicking" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "cfg-if", "sel4-immediate-sync-once-cell", @@ -613,12 +613,12 @@ dependencies = [ [[package]] name = "sel4-panicking-env" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-phdrs" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "sel4-phdrs-constants", ] @@ -626,12 +626,12 @@ dependencies = [ [[package]] name = "sel4-phdrs-constants" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-phdrs-patched" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "sel4-phdrs", "sel4-rodata-static", @@ -640,12 +640,12 @@ dependencies = [ [[package]] name = "sel4-rodata-static" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-root-task" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "sel4", "sel4-dlmalloc", @@ -660,7 +660,7 @@ dependencies = [ [[package]] name = "sel4-root-task-macros" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "proc-macro2", "quote", @@ -670,7 +670,7 @@ dependencies = [ [[package]] name = "sel4-runtime-common" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "cfg-if", "sel4", @@ -686,12 +686,12 @@ dependencies = [ [[package]] name = "sel4-stack" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" [[package]] name = "sel4-sync" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "lock_api", "sel4", @@ -701,7 +701,7 @@ dependencies = [ [[package]] name = "sel4-sys" version = "0.1.0" -source = "git+https://github.com/seL4/rust-sel4?rev=2541371f62dd097f7d47127125c44a0922145fa5#2541371f62dd097f7d47127125c44a0922145fa5" +source = "git+https://github.com/au-ts/rust-sel4?rev=121798b0260d0ff5ca1185702a0d3285d01ef439#121798b0260d0ff5ca1185702a0d3285d01ef439" dependencies = [ "bindgen", "glob", diff --git a/Cargo.toml b/Cargo.toml index b9d265064..dd4d4ab25 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,12 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/seL4/rust-sel4" -rev = "2541371f62dd097f7d47127125c44a0922145fa5" +git = "https://github.com/au-ts/rust-sel4" +rev = "121798b0260d0ff5ca1185702a0d3285d01ef439" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/seL4/rust-sel4" -rev = "2541371f62dd097f7d47127125c44a0922145fa5" +git = "https://github.com/au-ts/rust-sel4" +rev = "121798b0260d0ff5ca1185702a0d3285d01ef439" [profile.release.package.microkit-tool] strip = true diff --git a/build_sdk.py b/build_sdk.py index e9c180f53..3019bd526 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -67,8 +67,7 @@ DEFAULT_KERNEL_OPTIONS_X86_64 = { "KernelPlatform": "pc99", "KernelX86MicroArch": "generic", - # See https://github.com/seL4/microkit/issues/418 for details. - "KernelIOMMU": False, + "KernelIOMMU": True, } | DEFAULT_KERNEL_OPTIONS diff --git a/example/x86_64_iommu_dma_test/Makefile b/example/x86_64_iommu_dma_test/Makefile new file mode 100644 index 000000000..ef104c251 --- /dev/null +++ b/example/x86_64_iommu_dma_test/Makefile @@ -0,0 +1,72 @@ +# +# Copyright 2026, UNSW +# +# SPDX-License-Identifier: BSD-2-Clause +# +ifeq ($(strip $(BUILD_DIR)),) +$(error BUILD_DIR must be specified) +endif + +ifeq ($(strip $(MICROKIT_SDK)),) +$(error MICROKIT_SDK must be specified) +endif + +ifeq ($(strip $(MICROKIT_BOARD)),) +$(error MICROKIT_BOARD must be specified) +endif + +ifeq ($(strip $(MICROKIT_CONFIG)),) +$(error MICROKIT_CONFIG must be specified) +endif + +BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG) + +ARCH := ${shell grep 'CONFIG_SEL4_ARCH ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4} + +ifeq ($(ARCH),x86_64) + TOOLCHAIN := x86_64-linux-gnu + CFLAGS_ARCH := -march=x86-64 -mtune=generic +else +$(error Unsupported ARCH) +endif + +CC := $(TOOLCHAIN)-gcc +LD := $(TOOLCHAIN)-ld +AS := $(TOOLCHAIN)-as +OBJCOPY := $(TOOLCHAIN)-objcopy +MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit + +IMAGES := x86_64_iommu_dma_test.elf +CFLAGS := -nostdlib -ffreestanding -g3 -O3 -I$(BOARD_DIR)/include $(CFLAGS_ARCH) +LDFLAGS := -L$(BOARD_DIR)/lib -z noexecstack +LIBS := -lmicrokit -Tmicrokit.ld + +INITIAL_TASK = $(BUILD_DIR)/initialiser.elf +KERNEL = $(BUILD_DIR)/sel4.elf +KERNEL_32B = $(BUILD_DIR)/sel4_32.elf +REPORT = $(BUILD_DIR)/report.txt +SPEC = $(BUILD_DIR)/capdl_spec.json + +all: $(KERNEL) $(INITIAL_TASK) +qemu: $(KERNEL_32B) $(INITIAL_TASK) + +$(BUILD_DIR)/x86_64_iommu_dma_test.o: x86_64_iommu_dma_test.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ + +$(BUILD_DIR)/x86_64_iommu_dma_test.elf: $(BUILD_DIR)/x86_64_iommu_dma_test.o + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(KERNEL) $(KERNEL_32B) $(INITIAL_TASK): $(addprefix $(BUILD_DIR)/, $(IMAGES)) x86_64_iommu_dma_test.system + $(MICROKIT_TOOL) x86_64_iommu_dma_test.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(INITIAL_TASK) -r $(REPORT) --capdl-json $(SPEC) + +qemu: + qemu-system-x86_64 \ + -machine q35 \ + -cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \ + -m "4G" \ + -display none \ + -serial mon:stdio \ + -device intel-iommu,intremap=off,aw-bits=39 \ + -device edu,dma_mask=0xffffffffffffffff,bus=pcie.0,addr=0x04.0 \ + -kernel $(KERNEL_32B) \ + -initrd $(INITIAL_TASK) diff --git a/example/x86_64_iommu_dma_test/README.md b/example/x86_64_iommu_dma_test/README.md new file mode 100644 index 000000000..d22406841 --- /dev/null +++ b/example/x86_64_iommu_dma_test/README.md @@ -0,0 +1,25 @@ + +# x86_64_iommu_dma_test + +This example checks x86 IOMMU mappings with QEMU's EDU PCI device. It maps one +RAM page into the EDU device's IOSpace, asks the device to DMA from that page +into its internal SRAM, then asks the device to DMA the SRAM contents back into +a second offset in the same RAM page and verifies the data. + +The QEMU command in the Makefile pins the EDU device at PCI BDF `00:04.0`, which +must match the `pcidev="0:4.0"` attribute in the system description. + +To build and run: + +```sh +mkdir build +make -C example/x86_64_iommu_dma_test \ + BUILD_DIR=build \ + MICROKIT_SDK=/path/to/microkit-sdk \ + MICROKIT_BOARD=x86_64_generic \ + MICROKIT_CONFIG=debug \ + qemu +``` diff --git a/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c b/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c new file mode 100644 index 000000000..fff25ad74 --- /dev/null +++ b/example/x86_64_iommu_dma_test/x86_64_iommu_dma_test.c @@ -0,0 +1,234 @@ +/* + * Copyright 2026, UNSW + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include +#include + +#include + +#define PCI_CONFIG_ADDRESS 0xcf8u +#define PCI_CONFIG_DATA 0xcfcu +#define PCI_ENABLE 0x80000000u +#define PCI_COMMAND 0x04u +#define PCI_BAR0 0x10u +#define PCI_COMMAND_MEMORY 0x0002u +#define PCI_COMMAND_MASTER 0x0004u + +#define EDU_BUS 0u +#define EDU_DEV 4u +#define EDU_FUNC 0u +#define EDU_DEVICE_ID 0xedu +#define EDU_PCI_VENDOR_ID 0x1234u +#define EDU_PCI_DEVICE_ID 0x11e8u + +#define EDU_MMIO_PADDR 0xfe000000ull +#define EDU_MMIO_SIZE 0x00100000ull +#define EDU_BAR_SIZE 0x00100000ull +#define EDU_DMA_SRAM 0x40000ull +#define DMA_BUFFER_IOVA 0x00100000ull +#define DMA_TEST_BYTES 64u +#define DMA_RETURN_OFFSET 0x100u +#define DMA_TIMEOUT 10000000u + +#define EDU_REG_ID 0x00u +#define EDU_REG_ALIVE 0x04u +#define EDU_REG_DMA_SRC 0x80u +#define EDU_REG_DMA_DST 0x88u +#define EDU_REG_DMA_COUNT 0x90u +#define EDU_REG_DMA_CMD 0x98u + +#define EDU_DMA_START 0x1u +#define EDU_DMA_TO_RAM 0x2u + +uint64_t edu_mmio_window_vaddr; +uint64_t dma_buffer_vaddr; +uint64_t pci_config_ioport_id; + +static void put_hex64(uint64_t value) +{ + char buf[19] = "0x0000000000000000"; + for (size_t i = 0; i < 16; i++) { + unsigned int nibble = (value >> ((15 - i) * 4)) & 0xf; + buf[2 + i] = nibble < 10 ? '0' + nibble : 'a' + (nibble - 10); + } + microkit_dbg_puts(buf); +} + +static uint32_t pci_config_read32(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset) +{ + uint32_t address = + PCI_ENABLE | ((uint32_t)bus << 16) | ((uint32_t)dev << 11) | ((uint32_t)func << 8) | (offset & 0xfcu); + + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_ADDRESS, address); + return microkit_x86_ioport_read_32(pci_config_ioport_id, PCI_CONFIG_DATA); +} + +static uint16_t pci_config_read16(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset) +{ + uint32_t value = pci_config_read32(bus, dev, func, offset); + return (value >> ((offset & 2u) * 8)) & 0xffffu; +} + +static void pci_config_write16(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset, uint16_t value) +{ + uint32_t address = + PCI_ENABLE | ((uint32_t)bus << 16) | ((uint32_t)dev << 11) | ((uint32_t)func << 8) | (offset & 0xfcu); + + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_ADDRESS, address); + microkit_x86_ioport_write_16(pci_config_ioport_id, PCI_CONFIG_DATA + (offset & 2u), value); +} + +static void pci_config_write32(uint8_t bus, uint8_t dev, uint8_t func, uint8_t offset, uint32_t value) +{ + uint32_t address = + PCI_ENABLE | ((uint32_t)bus << 16) | ((uint32_t)dev << 11) | ((uint32_t)func << 8) | (offset & 0xfcu); + + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_ADDRESS, address); + microkit_x86_ioport_write_32(pci_config_ioport_id, PCI_CONFIG_DATA, value); +} + +static volatile uint32_t *edu_reg32(uintptr_t edu_base, uint32_t offset) +{ + return (volatile uint32_t *)(edu_base + offset); +} + +static volatile uint64_t *edu_reg64(uintptr_t edu_base, uint32_t offset) +{ + return (volatile uint64_t *)(edu_base + offset); +} + +static uint32_t edu_read32(uintptr_t edu_base, uint32_t offset) +{ + return *edu_reg32(edu_base, offset); +} + +static void edu_write32(uintptr_t edu_base, uint32_t offset, uint32_t value) +{ + *edu_reg32(edu_base, offset) = value; +} + +static void edu_write64(uintptr_t edu_base, uint32_t offset, uint64_t value) +{ + *edu_reg64(edu_base, offset) = value; +} + +static void wait_for_dma(uintptr_t edu_base) +{ + while ((edu_read32(edu_base, EDU_REG_DMA_CMD) & EDU_DMA_START)) + ; +} + +static void fill_dma_buffer(void) +{ + volatile uint32_t *buf = (volatile uint32_t *)(uintptr_t)dma_buffer_vaddr; + + for (size_t i = 0; i < DMA_TEST_BYTES / sizeof(uint32_t); i++) { + buf[i] = 0x5a000000u | (uint32_t)i; + buf[(DMA_RETURN_OFFSET / sizeof(uint32_t)) + i] = 0; + } +} + +static bool check_dma_return_buffer(void) +{ + volatile uint32_t *buf = (volatile uint32_t *)(uintptr_t)dma_buffer_vaddr; + + for (size_t i = 0; i < DMA_TEST_BYTES / sizeof(uint32_t); i++) { + uint32_t expected = 0x5a000000u | (uint32_t)i; + uint32_t actual = buf[(DMA_RETURN_OFFSET / sizeof(uint32_t)) + i]; + if (actual != expected) { + microkit_dbg_puts("DMA return buffer mismatch at word "); + put_hex64(i); + microkit_dbg_puts(": expected "); + put_hex64(expected); + microkit_dbg_puts(", got "); + put_hex64(actual); + microkit_dbg_puts("\n"); + return false; + } + } + return true; +} + +static bool check_edu_liveness(uintptr_t edu_base) +{ + const uint32_t probe = 0xa5a55a5au; + + edu_write32(edu_base, EDU_REG_ALIVE, probe); + return edu_read32(edu_base, EDU_REG_ALIVE) == ~probe; +} + +void init(void) +{ + microkit_dbg_puts("x86_64_iommu_dma_test: starting\n"); + + uint32_t id = pci_config_read32(EDU_BUS, EDU_DEV, EDU_FUNC, 0x00); + if ((id & 0xFFFFu) != EDU_PCI_VENDOR_ID || ((id >> 16) & 0xFFFFu) != EDU_PCI_DEVICE_ID) { + microkit_dbg_puts("x86_64_iommu_dma_test: EDU PCI device not found, id="); + put_hex64(id); + microkit_dbg_puts("\n"); + return; + } + + pci_config_write32(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_BAR0, EDU_MMIO_PADDR); + + uint64_t bar0 = pci_config_read32(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_BAR0) & ~0xfu; + if (bar0 < EDU_MMIO_PADDR || bar0 + EDU_BAR_SIZE > EDU_MMIO_PADDR + EDU_MMIO_SIZE) { + microkit_dbg_puts("x86_64_iommu_dma_test: EDU BAR outside mapped MMIO window, bar="); + put_hex64(bar0); + microkit_dbg_puts("\n"); + return; + } + + uint16_t command = pci_config_read16(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_COMMAND); + command |= PCI_COMMAND_MEMORY | PCI_COMMAND_MASTER; + pci_config_write16(EDU_BUS, EDU_DEV, EDU_FUNC, PCI_COMMAND, command); + + uintptr_t edu_base = (uintptr_t)edu_mmio_window_vaddr + (uintptr_t)(bar0 - EDU_MMIO_PADDR); + microkit_dbg_puts("x86_64_iommu_dma_test: EDU BAR="); + put_hex64(bar0); + microkit_dbg_puts(", id_reg="); + uint32_t device_id = edu_read32(edu_base, EDU_REG_ID); + put_hex64(device_id); + if ((device_id & 0xFF) != EDU_DEVICE_ID) { + microkit_dbg_puts("x86_64_iommu_dma_test: Identification failed.\n"); + return; + } + microkit_dbg_puts("\n"); + + if (!check_edu_liveness(edu_base)) { + microkit_dbg_puts("x86_64_iommu_dma_test: EDU MMIO liveness check failed\n"); + return; + } + + /* The qemu education device works by copying from DRAM to an internal device buffer or vice-versa. */ + fill_dma_buffer(); + + edu_write64(edu_base, EDU_REG_DMA_SRC, DMA_BUFFER_IOVA); + edu_write64(edu_base, EDU_REG_DMA_DST, EDU_DMA_SRAM); + edu_write64(edu_base, EDU_REG_DMA_COUNT, DMA_TEST_BYTES); + edu_write32(edu_base, EDU_REG_DMA_CMD, EDU_DMA_START); + + wait_for_dma(edu_base); + + edu_write64(edu_base, EDU_REG_DMA_SRC, EDU_DMA_SRAM); + edu_write64(edu_base, EDU_REG_DMA_DST, DMA_BUFFER_IOVA + DMA_RETURN_OFFSET); + edu_write64(edu_base, EDU_REG_DMA_COUNT, DMA_TEST_BYTES); + edu_write32(edu_base, EDU_REG_DMA_CMD, EDU_DMA_START | EDU_DMA_TO_RAM); + + wait_for_dma(edu_base); + + if (!check_dma_return_buffer()) { + microkit_dbg_puts("x86_64_iommu_dma_test: DMA verification failed\n"); + return; + } + + microkit_dbg_puts("x86_64_iommu_dma_test: DMA verification passed\n"); +} + +void notified(microkit_channel ch) +{ + (void)ch; +} diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 51c403a0b..40671de5f 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -18,14 +18,14 @@ use sel4_capdl_initializer_types::{ use crate::{ capdl::{ irq::create_irq_handler_cap, - memory::{create_vspace, create_vspace_ept, AddressSpace}, + memory::{create_iospace, create_vspace, create_vspace_ept, AddressSpace}, spec::{capdl_obj_physical_size_bits, BytesContent, ElfContent, FillContent}, util::*, }, elf::ElfFile, sdf::{ - CapMapType, CpuCore, Map, SystemDescription, BUDGET_DEFAULT, MONITOR_PD_NAME, - MONITOR_PRIORITY, + CapMapType, CpuCore, IommuDeviceIdentifier, Map, SystemDescription, BUDGET_DEFAULT, + MONITOR_PD_NAME, MONITOR_PRIORITY, }, sel4::{Arch, Config, PageSize}, util::{ranges_overlap, round_down, round_up}, @@ -1244,7 +1244,46 @@ pub fn build_capdl_spec( } // ********************************* - // Step 6. Sort the root objects + // Step 6. Create IOMMU Address Spaces + // ********************************* + let mut iospace_by_device: HashMap = HashMap::new(); + for iomap in system.iomaps.iter() { + let address_space = iospace_by_device + .entry(iomap.identifier) + .or_insert_with(|| { + create_iospace( + &mut spec_container, + kernel_config, + &iomap.device, + iomap.identifier, + iomap.domain_id, + ) + }); + let page_size_bytes = mr_name_to_frames + .get(&iomap.mr) + .ok_or(format!( + "Error: Memory region {} referenced by iomap not found.", + iomap.mr + ))? + .first() + .map(|&object_id| 1 << capdl_util_get_frame_size_bits(&spec_container, object_id)) + .ok_or(format!( + "Error: Memory region {} referenced by iomap has no frames.", + &iomap.mr + ))?; + + map_memory_region( + &mut spec_container, + kernel_config, + iomap, + page_size_bytes, + address_space, + &mr_name_to_frames[&iomap.mr], + )?; + } + + // ********************************* + // Step 7. Sort the root objects // ********************************* // The CapDL initialiser expects objects with paddr to come first, then sorted by size so that the // allocation algorithm at run-time can run more efficiently. diff --git a/tool/microkit/src/capdl/memory.rs b/tool/microkit/src/capdl/memory.rs index 3061af1aa..0294b3047 100644 --- a/tool/microkit/src/capdl/memory.rs +++ b/tool/microkit/src/capdl/memory.rs @@ -8,9 +8,12 @@ use crate::{ spec::capdl_obj_human_name, util::capdl_util_make_cte, CapDLNamedObject, CapDLSpecContainer, FrameFill, }, + sdf::IommuDeviceIdentifier, sel4::{Arch, Config, ObjectType, PageSize}, }; -use sel4_capdl_initializer_types::{cap, object, Cap, Object, ObjectId}; +use sel4_capdl_initializer_types::{ + cap, object, x86_io_address_space, Cap, Object, ObjectId, Word, +}; use std::ops::Range; /// For naming and debugging purposes only, no functional purpose. @@ -48,6 +51,14 @@ fn get_pt_level_name(sel4_config: &Config, level: usize) -> &str { } } +fn get_iopt_level_name(level: usize) -> String { + if level == 0 { + "iospace".to_string() + } else { + format!("iopt_level_{}", level - 1) + } +} + #[derive(Debug, Clone, PartialEq, Eq)] pub enum AddressSpace { VSpace { @@ -55,17 +66,22 @@ pub enum AddressSpace { root: ObjectId, x86_ept: bool, }, + IOSpace { + name: String, + root: ObjectId, + device: IommuDeviceIdentifier, + }, } impl AddressSpace { pub fn root(&self) -> ObjectId { match self { - &Self::VSpace { root, .. } => root, + &Self::VSpace { root, .. } | &Self::IOSpace { root, .. } => root, } } pub fn name(&self) -> &str { match self { - Self::VSpace { name, .. } => name, + Self::VSpace { name, .. } | Self::IOSpace { name, .. } => name, } } @@ -105,32 +121,42 @@ impl AddressSpace { fn get_level_name(&self, sel4_config: &Config, level: usize) -> String { match self { Self::VSpace { .. } => get_pt_level_name(sel4_config, level).to_string(), + Self::IOSpace { .. } => get_iopt_level_name(level), } } fn get_addr_label(&self) -> &'static str { match self { Self::VSpace { .. } => "vaddr", + Self::IOSpace { .. } => "ioaddr", } } - fn get_leaf_bits(&self, sel4_config: &Config) -> u64 { - match self { - Self::VSpace { .. } => ObjectType::SmallPage.fixed_size_bits(sel4_config).unwrap(), - } + fn get_leaf_bits(sel4_config: &Config) -> u64 { + ObjectType::SmallPage.fixed_size_bits(sel4_config).unwrap() } fn level_index_bits(&self, sel4_config: &Config, level: usize) -> u64 { match self { Self::VSpace { .. } => sel4_config.vspace_level_index_bits(level), + Self::IOSpace { .. } => { + if level > 0 { + sel4_config.io_page_table_index_bits() + } else { + panic!("IODevice root is not indexed by address bits"); + } + } } } fn get_level_index(&self, sel4_config: &Config, level: usize, vaddr: u64) -> usize { + if matches!(self, AddressSpace::IOSpace { .. }) && level == 0 { + return x86_io_address_space::IOSPACE_ROOT_IOPT_SLOT; + } let levels = self.address_space_levels(sel4_config); assert!(level < levels); - let page_bits = self.get_leaf_bits(sel4_config); + let page_bits = Self::get_leaf_bits(sel4_config); let bits_from_higher_lvls: u64 = ((level + 1)..levels) .map(|level| self.level_index_bits(sel4_config, level)) .sum(); @@ -143,7 +169,7 @@ impl AddressSpace { fn get_level_coverage(&self, sel4_config: &Config, level: usize, vaddr: u64) -> Range { let levels = self.address_space_levels(sel4_config); - let page_bits = self.get_leaf_bits(sel4_config); + let page_bits = Self::get_leaf_bits(sel4_config); let bits_from_higher_lvls: u64 = ((level + 1)..levels) .map(|level| self.level_index_bits(sel4_config, level)) .sum(); @@ -300,12 +326,22 @@ impl AddressSpace { level: Some(level as u8), slots: vec![], }), + AddressSpace::IOSpace { .. } => { + let iopt_level = level + .checked_sub(1) + .expect("Error: cannot create an intermediate IOPT for the root level."); + Object::IOPT(object::IOPT { + slots: vec![], + level: Word(iopt_level as u64), + }) + } } } fn make_intermediate_cap(&self, object: ObjectId) -> Cap { match self { AddressSpace::VSpace { .. } => Cap::PageTable(cap::PageTable { object }), + AddressSpace::IOSpace { .. } => Cap::IOPT(cap::IOPT { object }), } } @@ -327,6 +363,13 @@ impl AddressSpace { ) -> Result<(), String> { let valid = match self { AddressSpace::VSpace { .. } => matches!(object, Object::PageTable(_)), + AddressSpace::IOSpace { .. } => { + if cur_level == 0 { + matches!(object, Object::IODevice(_)) + } else { + matches!(object, Object::IOPT(_)) + } + } }; if valid { Ok(()) @@ -343,16 +386,82 @@ impl AddressSpace { fn address_space_levels(&self, sel4_config: &Config) -> usize { match self { AddressSpace::VSpace { .. } => sel4_config.num_page_table_levels(), + // IOSpace level 0 is the IODevice root. Slot 0 points to the + // normal IOPT tree root, and slots 1.. hold spare IOPTs for + // runtime prefix levels. + AddressSpace::IOSpace { .. } => x86_io_address_space::CAPDL_NUM_IOPT_LEVELS + 1, } } fn get_root_level(&self, sel4_config: &Config) -> usize { match self { AddressSpace::VSpace { .. } => sel4_config.vspace_root_level(), + AddressSpace::IOSpace { .. } => 0, } } } +// In future supporting SMMU can be done by matching on the IommuDeviceIdentifier or creating a new function. +pub fn create_iospace( + spec_container: &mut CapDLSpecContainer, + sel4_config: &Config, + device_name: &str, + device_identifier: IommuDeviceIdentifier, + domain_id: Option, +) -> AddressSpace { + let IommuDeviceIdentifier::X86Pci(pci_device) = device_identifier; + + let root = spec_container.add_root_object(CapDLNamedObject { + name: format!("{}_{}", get_iopt_level_name(0), device_name).into(), + object: Object::IODevice(object::IODevice { + slots: vec![], + domain_id: domain_id.unwrap().into(), + pci_device: ( + Word(pci_device.bus.into()), + Word(pci_device.device.into()), + Word(pci_device.function.into()), + ), + }), + }); + + let address_space = AddressSpace::IOSpace { + name: device_name.to_string(), + root, + device: device_identifier, + }; + + // The IODevice root has two roles: slot 0 is reserved for the root of the + // normal 3-level IOPT tree, while slots 1.. hold spare IOPTs that the + // initialiser can use when seL4 reports a wider IOVA space at runtime. + for spare_idx in 0..x86_io_address_space::SPARE_NUM_LEVELS { + let slot = x86_io_address_space::IOSPACE_ROOT_IOPT_SLOT + 1 + spare_idx; + let next_obj_id = spec_container.add_root_object(CapDLNamedObject { + name: format!( + "{}_{}_spare_{}", + get_iopt_level_name(1), + address_space.name(), + slot + ) + .into(), + object: address_space.make_intermediate_object(1), + }); + let next_cap = address_space.make_intermediate_cap(next_obj_id); + + address_space + .insert_cap_into_level( + spec_container, + sel4_config, + address_space.root(), + address_space.get_root_level(sel4_config), + slot, + next_cap, + ) + .unwrap_or_else(|err| panic!("Error: create_iospace() failed allocating spare IOPT capabilities with error {err}")); + } + + address_space +} + fn create_vspace_address_space( spec_container: &mut CapDLSpecContainer, sel4_config: &Config, diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index 980f4fef8..93a9b6704 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -51,6 +51,9 @@ pub fn capdl_obj_physical_size_bits(obj: &Object, sel4_config: &Confi } } Object::AsidPool(_) => ObjectType::AsidPool.fixed_size_bits(sel4_config).unwrap(), + Object::IOPT(_) => ObjectType::IOPageTable + .fixed_size_bits(sel4_config) + .unwrap(), Object::SchedContext(sched_context) => sched_context.size_bits as u64, Object::Reply => ObjectType::Reply.fixed_size_bits(sel4_config).unwrap(), _ => 0, @@ -75,6 +78,8 @@ pub fn capdl_obj_human_name(obj: &Object, sel4_config: &Config) -> &' } Object::PageTable(_) => "PageTable", Object::AsidPool(_) => "AsidPool", + Object::IODevice(_) => "x86 IODevice", + Object::IOPT(_) => "x86 IOPT", Object::ArmIrq(_) => "ARM IRQ", Object::IrqMsi(_) => "x86 MSI IRQ", Object::IrqIOApic(_) => "x86 IOAPIC IRQ", diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 90af397ba..f7c0d09b7 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -22,7 +22,7 @@ use crate::sel4::{ use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool}; use crate::MAX_PDS; -use sel4_capdl_initializer_types::FillEntryContentBootInfoId; +use sel4_capdl_initializer_types::{x86_io_address_space, FillEntryContentBootInfoId}; use std::collections::{HashMap, HashSet}; use std::fmt; use std::fs; @@ -62,12 +62,6 @@ const PD_MAX_STACK_SIZE: u64 = 1024 * 1024 * 16; /// `src/arch/x86/object/interrupt.c` const X86_IRQ_VECTOR_MAX: i64 = 107; -// In reality the kernel dynamically determines this value. The tool assumes -// at least 512GiB of IO virtual address space. This handles all values reported -// to us by the kernel at runtime except for the 1GiB or no-iommu cases. -// This is currently applied to any iommu mapping independent of the architecture. -const IOMAP_MAX_VADDR: u64 = (1 << 39) - 1; - /// The purpose of this function is to parse an integer that could /// either be in decimal or hex format, unlike the normal parsing /// functionality that the Rust standard library provides. @@ -744,13 +738,13 @@ impl SysIOMap { let mr = checked_lookup(xml_sdf, node, "mr")?.to_string(); let iovaddr = sdf_parse_number(checked_lookup(xml_sdf, node, "iovaddr")?, node)?; - if iovaddr > IOMAP_MAX_VADDR { + if iovaddr > x86_io_address_space::CAPDL_MAX_IOVA { return Err(value_error( xml_sdf, node, format!( "iovaddr ({iovaddr:#x}) must be less than {:#x}", - IOMAP_MAX_VADDR + 1 + x86_io_address_space::CAPDL_MAX_IOVA + 1 ), )); } @@ -2196,7 +2190,13 @@ fn check_io_maps( for (identifier, maps) in by_device { let address_space = identifier.to_string(); - check_maps(xml_sdf, mrs, maps, &address_space, IOMAP_MAX_VADDR + 1)?; + check_maps( + xml_sdf, + mrs, + maps, + &address_space, + x86_io_address_space::CAPDL_MAX_IOVA + 1, + )?; } Ok(()) diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index b2e4439ab..83d66bac5 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -285,6 +285,7 @@ pub struct ObjectSizes { pub reply: u64, pub vspace: u64, pub page_table: u64, + pub io_page_table: Option, pub huge_page: u64, pub large_page: u64, pub small_page: u64, @@ -489,6 +490,7 @@ pub enum ObjectType { PageTable, Vcpu, AsidPool, + IOPageTable, } impl ObjectType { @@ -503,6 +505,10 @@ impl ObjectType { ObjectType::Reply => Some(object_sizes.reply), ObjectType::VSpace => Some(object_sizes.vspace), ObjectType::PageTable => Some(object_sizes.page_table), + ObjectType::IOPageTable => match (config.arch, config.iommu) { + (Arch::X86_64, true) => Some(object_sizes.io_page_table.unwrap()), + _ => panic!("Unexpected architecture or build asking for io_page_table_bits"), + }, ObjectType::HugePage => Some(object_sizes.huge_page), ObjectType::LargePage => Some(object_sizes.large_page), ObjectType::SmallPage => Some(object_sizes.small_page), diff --git a/tool/microkit/src/viper.rs b/tool/microkit/src/viper.rs index bc220f4da..709f2d694 100644 --- a/tool/microkit/src/viper.rs +++ b/tool/microkit/src/viper.rs @@ -143,6 +143,8 @@ pub fn get_cap_view( | Cap::DomainSet(_) | Cap::Frame(_) | Cap::SchedContext(_) + | Cap::IOSpace(_) + | Cap::IOPT(_) | Cap::Untyped(_) => { /* ^ The caps above can occupy CSpace slots, but Viper * verification currently has no use for them, so we diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 642c3fa2d..d48c3542d 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -21,6 +21,7 @@ const DEFAULT_OBJECT_SIZES: sel4::ObjectSizes = sel4::ObjectSizes { huge_page: 0, large_page: 0, small_page: 0, + io_page_table: None, asid_pool: 0, vcpu: None, }; From df27a1905e8666897e256568a7c453696a585567 Mon Sep 17 00:00:00 2001 From: Callum Date: Thu, 9 Jul 2026 19:11:40 +1000 Subject: [PATCH 3/3] IOMMU: Add large page guard While seL4 does not support large pages to be used by the IOMMU, we will raise an error at the SDF parsing stage. Signed-off-by: Callum --- tool/microkit/src/sdf.rs | 11 ++++++++++- tool/microkit/tests/test.rs | 6 +++++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index f7c0d09b7..bc8458a83 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -2188,6 +2188,15 @@ fn check_io_maps( by_device.entry(iomap.identifier).or_default().push(iomap); } + if iomaps.iter().any(|iomap| { + mrs.iter() + .any(|mr| mr.page_size == PageSize::Large && mr.name == iomap.mr_name()) + }) { + return Err( + "Error: currently seL4 does not have large page support for the IOMMU".to_string(), + ); + } + for (identifier, maps) in by_device { let address_space = identifier.to_string(); check_maps( @@ -2806,7 +2815,7 @@ pub fn parse( // Optimise page size of MRs, if the page size is not specified for mr in &mut mrs { - if mr.page_size_specified_by_user { + if mr.page_size_specified_by_user || iomaps.iter().any(|iomap| iomap.mr_name() == mr.name) { continue; } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index d48c3542d..e8f8457db 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -909,12 +909,16 @@ mod iommu { ) } + // Currently this test fails with "Error: currently seL4 does not have large page support for the IOMMU" + // When seL4 supports large pages for the iommu it should fail with: + // Error: map for 'small_region' has io address range [0x1000..0x2000) which overlaps with map for + //'large_region' [0x0..0x200000) in PCI device 00:03.0 @ " #[test] fn test_overlap_mixed_page_sizes() { check_error( &DEFAULT_X86_64_KERNEL_CONFIG, "iommu_overlap_mixed_page_sizes.system", - "Error: map for 'small_region' has io address range [0x1000..0x2000) which overlaps with map for 'large_region' [0x0..0x200000) in PCI device 00:03.0 @", + "Error: currently seL4 does not have large page support for the IOMMU", ) }