seL4 is currently built with PCIDs disabled because QEMU TCG lacks support. This ensured the x86_64_generic and x86_64_generic_vtx configurations remained universally compatible.
Keeping PCIDs disabled leaves x86-64 performance on the table for real silicon.
We should investigate a better build or runtime strategy to enable PCIDs on bare metal while maintaining QEMU TCG compatibility.
seL4 is currently built with PCIDs disabled because QEMU TCG lacks support. This ensured the
x86_64_genericandx86_64_generic_vtxconfigurations remained universally compatible.Keeping PCIDs disabled leaves x86-64 performance on the table for real silicon.
We should investigate a better build or runtime strategy to enable PCIDs on bare metal while maintaining QEMU TCG compatibility.