[seL4] AMD CPUs and SMP scalability

My understanding is that seL4 plans on scaling to large multi-core server processors by using Intel TSX. However, AMD has not implemented TSX, and TSX has been involved in many recent side-channel attacks. AMD systems are attractive both from a performance and a security perspective, but my understanding is that the performance of seL4 on them will be terrible.

Are there plans to implement and verify a version of seL4 that scales to multicore AMD server-class CPUs? The problem with a multikernel is that not having thread migration is likely to cause starvation on many practical workloads

Sincerely,

Demi