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.
Hmm. Could be the mailbox communication for VPUCPU communication timing out? BCM should be able to repro and fix that. They could also be able to make enabling HYP mode less of a hack.
As for the lack of an accessible GIC, the VPU runs ThreadX, which has a software timer infrastructure: no reason I can see they couldn't expose those if they wanted.