Hi Kent, Here another problem relevant intel-vtd needs to consider about when working the patch(maybe you've already done that:). In kernel/src/arch/x86/object/iospace.c::decodeX86IOPTInvocation, when do `X86IOPageTableMap`, first we look up the last existing PTE for the new PT mapping: ``` lu_ret = lookupIOPTSlot(vtd_pte, io_address); ``` Because `io_address` comes from user space, it can be any value(bits 0~20 masked out). Let's assume x86KSnumIOPTLevels=4(0~3). If level 3 PT for `io_address` already existed and entry 0 was free, the `lu_ret` would give: ``` { .status = EXCEPTION_NONE; .ioptSlot = free level 3 PTE address; .level = 0; } ``` Thereafter the code would create a valid page mapping instead of PT mapping, and the cap's level field would be set to 4 - violate the seL4 specification I think. So when checking `lookupIOPTSlot` return value, we should also check the `.status = EXCEPTION_NONE && .level = 0` condition, and figure out that it is another EXCEPTION_SYSCALL_ERROR. If I misunderstood something, please let me know. Regards, laokz