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