So is the interrupt thing a real HW bug in the RPi CPU or might this be solvable with some setup magic on the VC black box side? And why does isolating one core on the host side suffice, without restricting which cores the guest can run on? He's running the guest SMP enabled in the example posted.