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..bc8458a83 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 ), )); } @@ -2194,9 +2188,24 @@ 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(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(()) @@ -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/src/sel4.rs b/tool/microkit/src/sel4.rs index 2868c2871..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, @@ -425,6 +426,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)] @@ -476,6 +490,7 @@ pub enum ObjectType { PageTable, Vcpu, AsidPool, + IOPageTable, } impl ObjectType { @@ -490,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..e8f8457db 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, }; @@ -908,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", ) }