On Fri, Nov 30, 2012 at 04:47:40PM +0000, Christoffer Dall wrote:

On Fri, Nov 30, 2012 at 10:15 AM, Will Deacon [off-list ref] wrote:

quoted

At this point, VM1 is running and VM0:VCPU1 is running. VM0:VCPU0 is not
running because physical CPU0 is handling an interrupt. The problem is that
when VCPU0 *is* resumed, it will update the VMID of VM0 and could be
scheduled in parallel with VCPU1 but with a different VMID.

How do you avoid this in the current code?

I don't. Nice catch. Please apply your interesting brain to the following fix:)

I'm far too sober to look at your patch right now, but I'll think about it
over the weekend [I can't break it at a quick glance] :)

In the meantime, can you think about whether the TLB operations need to run
on every CPU please?

Will