421a422,431
> * Get a pointer to the event queue owning devices.
> *
> * Devices always live in a separate device event queue when
> * running in multi-core mode. We need to temporarily migrate to
> * this queue when accessing devices. By convention, devices and
> * the VM use the same event queue.
> */
> EventQueue *deviceEventQueue() { return vm.eventQueue(); }
>
> /**