IOMMU Management in seL4
Honours Thesis — UNSW Trustworthy Systems Group
- Benchmarked 10GbE (Intel X550 on x86) and 1GbE (Cadence GEM on ARM Xilinx ZCU102) network throughput degradation under strict per-packet vs. batched lazy IOMMU mapping.
- Measured hardware IOTLB invalidation and miss costs at the CPU cycle level using custom DMA microbenchmarks and x86 queued invalidation ring buffers.
- Designed static (seL4 Microkit) and dynamic IOMMU address-space management architectures for the seL4 Device Driver Framework (sDDF).
CseL4Linux Kernelx86 IOMMUARM SMMUDMA