diff --git a/examples/rust/src/vmm.rs b/examples/rust/src/vmm.rs
index 321b57ba..e27a789c 100644
--- a/examples/rust/src/vmm.rs
+++ b/examples/rust/src/vmm.rs
@@ -100,7 +100,7 @@ impl Handler for VmmHandler {
         match channel {
             UART_CH => {
                 unsafe {
-                    let success = virq_inject(GUEST_VCPU_ID, UART_IRQ as i32);
+                    let success = virq_inject(UART_IRQ as i32);
                     if !success {
                         debug_println!("VMM|ERROR: could not inject UART IRQ");
                     }
diff --git a/examples/simple/vmm.c b/examples/simple/vmm.c
index ce260e2e..f418617f 100644
--- a/examples/simple/vmm.c
+++ b/examples/simple/vmm.c
@@ -121,9 +121,9 @@ void init(void) {
 void notified(microkit_channel ch) {
     switch (ch) {
         case SERIAL_IRQ_CH: {
-            bool success = virq_inject(GUEST_VCPU_ID, SERIAL_IRQ);
+            bool success = virq_inject(SERIAL_IRQ);
             if (!success) {
-                LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", SERIAL_IRQ, GUEST_VCPU_ID);
+                LOG_VMM_ERR("IRQ %d dropped\n", SERIAL_IRQ);
             }
             break;
         }
diff --git a/examples/virtio-snd/snd_driver_vmm.c b/examples/virtio-snd/snd_driver_vmm.c
index d408a178..9e1b7021 100644
--- a/examples/virtio-snd/snd_driver_vmm.c
+++ b/examples/virtio-snd/snd_driver_vmm.c
@@ -185,16 +185,16 @@ void notified(microkit_channel ch) {
         virtio_console_handle_rx(&virtio_console);
         break;
     case SND_CLIENT_CH:
-        success = virq_inject(GUEST_VCPU_ID, UIO_SND_IRQ);
+        success = virq_inject(UIO_SND_IRQ);
         if (!success) {
-            LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", UIO_SND_IRQ, GUEST_VCPU_ID);
+            LOG_VMM_ERR("IRQ %d dropped\n", UIO_SND_IRQ);
         }
         break;
     default:
         if (passthrough_irq_map[ch]) {
-            success = virq_inject(GUEST_VCPU_ID, passthrough_irq_map[ch]);
+            success = virq_inject(passthrough_irq_map[ch]);
             if (!success) {
-                LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", passthrough_irq_map[ch], GUEST_VCPU_ID);
+                LOG_VMM_ERR("IRQ %d dropped\n", passthrough_irq_map[ch]);
             }
         } else {
             printf("Unexpected channel, ch: 0x%lx\n", ch);
diff --git a/examples/virtio/blk_driver_vmm.c b/examples/virtio/blk_driver_vmm.c
index b1f54f06..ad78b673 100644
--- a/examples/virtio/blk_driver_vmm.c
+++ b/examples/virtio/blk_driver_vmm.c
@@ -145,7 +145,7 @@ void notified(microkit_channel ch)
 
     switch (ch) {
     case UIO_CH: {
-        int success = virq_inject(GUEST_VCPU_ID, UIO_IRQ);
+        int success = virq_inject(UIO_IRQ);
         if (!success) {
             LOG_VMM_ERR("Failed to inject UIO IRQ 0x%lx\n", UIO_IRQ);
         }
diff --git a/examples/zig/src/vmm.zig b/examples/zig/src/vmm.zig
index 51f9cd82..b0d5cf9e 100644
--- a/examples/zig/src/vmm.zig
+++ b/examples/zig/src/vmm.zig
@@ -118,9 +118,9 @@ export fn init() callconv(.C) void {
 export fn notified(ch: microkit.microkit_channel) callconv(.C) void {
     switch (ch) {
         SERIAL_IRQ_CH => {
-            const success = c.virq_inject(GUEST_BOOT_VCPU_ID, SERIAL_IRQ);
+            const success = c.virq_inject(SERIAL_IRQ);
             if (!success) {
-                log.err("IRQ {x} dropped on vCPU {x}\n", .{ SERIAL_IRQ, GUEST_BOOT_VCPU_ID });
+                log.err("IRQ {x} dropped\n", .{ SERIAL_IRQ });
             }
         },
         else => log.err("Unexpected channel, ch: {x}\n", .{ ch })
diff --git a/include/libvmm/arch/aarch64/vgic/vgic.h b/include/libvmm/arch/aarch64/vgic/vgic.h
index dab3759f..c64bea7f 100644
--- a/include/libvmm/arch/aarch64/vgic/vgic.h
+++ b/include/libvmm/arch/aarch64/vgic/vgic.h
@@ -50,8 +50,11 @@
 #endif
 
 void vgic_init();
-bool fault_handle_vgic_maintenance(size_t vcpu_id);
-bool handle_vgic_dist_fault(size_t vcpu_id, size_t offset, size_t fsr, seL4_UserContext *regs, void *data);
-bool handle_vgic_redist_fault(size_t vcpu_id, size_t offset, size_t fsr, seL4_UserContext *regs, void *data);
+
+bool vgic_handle_fault_maintenance(size_t vcpu_id);
+
+bool vgic_handle_fault_dist(size_t vcpu_id, size_t offset, size_t fsr, seL4_UserContext *regs, void *data);
+bool vgic_handle_fault_redist(size_t vcpu_id, size_t offset, size_t fsr, seL4_UserContext *regs, void *data);
+
 bool vgic_register_irq(size_t vcpu_id, int virq_num, virq_ack_fn_t ack_fn, void *ack_data);
 bool vgic_inject_irq(size_t vcpu_id, int irq);
diff --git a/include/libvmm/virq.h b/include/libvmm/virq.h
index 0b921364..363d74a8 100644
--- a/include/libvmm/virq.h
+++ b/include/libvmm/virq.h
@@ -14,9 +14,24 @@
 
 typedef void (*virq_ack_fn_t)(size_t vcpu_id, int irq, void *cookie);
 
+/*
+ * Initialise the architecture-depedent virtual interrupt controller.
+ * On ARM, this is the virtual Generic Interrupt Controller (vGIC).
+ */
 bool virq_controller_init(size_t boot_vcpu_id);
 bool virq_register(size_t vcpu_id, size_t virq_num, virq_ack_fn_t ack_fn, void *ack_data);
-bool virq_inject(size_t vcpu_id, int irq);
+
+/*
+ * Inject an IRQ into the boot virtual CPU.
+ * Note that this API requires that the IRQ has been registered (with virq_register).
+ */
+bool virq_inject(int irq);
+
+/*
+ * The same functionality as virq_inject, but will inject the virtual IRQ into a specific
+ * virtual CPU.
+ */
+bool virq_inject_vcpu(size_t vcpu_id, int irq);
 
 /*
  * These two APIs are convenient for when you want to directly passthrough an IRQ from
diff --git a/src/arch/aarch64/fault.c b/src/arch/aarch64/fault.c
index 60908315..2362ac90 100644
--- a/src/arch/aarch64/fault.c
+++ b/src/arch/aarch64/fault.c
@@ -395,7 +395,7 @@ bool fault_handle(size_t vcpu_id, microkit_msginfo msginfo) {
             success = fault_handle_user_exception(vcpu_id);
             break;
         case seL4_Fault_VGICMaintenance:
-            success = fault_handle_vgic_maintenance(vcpu_id);
+            success = vgic_handle_fault_maintenance(vcpu_id);
             break;
         case seL4_Fault_VCPUFault:
             success = fault_handle_vcpu_exception(vcpu_id);
diff --git a/src/arch/aarch64/vgic/vgic.c b/src/arch/aarch64/vgic/vgic.c
index 3e55c266..4e51710f 100644
--- a/src/arch/aarch64/vgic/vgic.c
+++ b/src/arch/aarch64/vgic/vgic.c
@@ -1,4 +1,4 @@
-/* @ivanv double check
+/*
  * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
  * Copyright 2022, UNSW (ABN 57 195 873 179)
  *
@@ -24,13 +24,13 @@
 /* The driver expects the VGIC state to be initialised before calling any of the driver functionality. */
 extern vgic_t vgic;
 
-bool fault_handle_vgic_maintenance(size_t vcpu_id)
+bool vgic_handle_fault_maintenance(size_t vcpu_id)
 {
     // @ivanv: reivist, also inconsistency between int and bool
     bool success = true;
     int idx = microkit_mr_get(seL4_VGICMaintenance_IDX);
     /* Currently not handling spurious IRQs */
-    // @ivanv: wtf, this comment seems irrelevant to the code.
+    // @ivanv: this comment seems irrelevant to the code.
     assert(idx >= 0);
 
     // @ivanv: Revisit and make sure it's still correct.
@@ -63,14 +63,27 @@ bool fault_handle_vgic_maintenance(size_t vcpu_id)
     }
 
     if (!success) {
-        printf("VGIC|ERROR: maintenance handler failed\n");
+        LOG_VMM_ERR("vGIC maintenance handler failed\n");
         assert(0);
     }
 
     return success;
 }
 
-// @ivanv: maybe this shouldn't be here?
+bool vgic_handle_fault_dist(size_t vcpu_id, size_t offset, size_t fsr, seL4_UserContext *regs, void *data)
+{
+    bool success = false;
+    if (fault_is_read(fsr)) {
+        success = vgic_dist_reg_read(vcpu_id, &vgic, offset, fsr, regs);
+        assert(success);
+    } else {
+        success = vgic_dist_reg_write(vcpu_id, &vgic, offset, fsr, regs);
+        assert(success);
+    }
+
+    return success;
+}
+
 bool vgic_register_irq(size_t vcpu_id, int virq_num, virq_ack_fn_t ack_fn, void *ack_data) {
     assert(virq_num >= 0 && virq_num != VIRQ_INVALID);
     struct virq_handle virq = {
@@ -89,29 +102,5 @@ bool vgic_inject_irq(size_t vcpu_id, int irq)
     bool success = vgic_dist_set_pending_irq(&vgic, vcpu_id, irq);
     assert(success);
 
-    // @ivanv: explain why we don't check error before checking this fault stuff
-    // @ivanv: seperately, it seems weird to have this fault handling code here?
-    // @ivanv: revist
-    // if (!fault_handled(vcpu->vcpu_arch.fault) && fault_is_wfi(vcpu->vcpu_arch.fault)) {
-    //     // ignore_fault(vcpu->vcpu_arch.fault);
-    //     err = advance_vcpu_fault(regs);
-    // }
     return success;
 }
-
-// @ivanv: revisit this whole function
-bool handle_vgic_dist_fault(size_t vcpu_id, size_t offset, size_t fsr, seL4_UserContext *regs, void *data)
-{
-    bool success = false;
-    if (fault_is_read(fsr)) {
-        // printf("VGIC|INFO: Read dist\n");
-        success = vgic_dist_reg_read(vcpu_id, &vgic, offset, fsr, regs);
-        assert(success);
-    } else {
-        // printf("VGIC|INFO: Write dist\n");
-        success = vgic_dist_reg_write(vcpu_id, &vgic, offset, fsr, regs);
-        assert(success);
-    }
-
-    return success;
-}
\ No newline at end of file
diff --git a/src/arch/aarch64/virq.c b/src/arch/aarch64/virq.c
index 9c4f635f..5b02c25e 100644
--- a/src/arch/aarch64/virq.c
+++ b/src/arch/aarch64/virq.c
@@ -37,13 +37,13 @@ bool virq_controller_init(size_t boot_vcpu_id) {
 #endif
 
     /* Register the fault handler */
-    success = fault_register_vm_exception_handler(GIC_DIST_PADDR, GIC_DIST_SIZE, handle_vgic_dist_fault, NULL);
+    success = fault_register_vm_exception_handler(GIC_DIST_PADDR, GIC_DIST_SIZE, vgic_handle_fault_dist, NULL);
     if (!success) {
         LOG_VMM_ERR("Failed to register fault handler for GIC distributor region\n");
         return false;
     }
 #if defined(GIC_V3)
-    success = fault_register_vm_exception_handler(GIC_REDIST_PADDR, GIC_REDIST_SIZE, handle_vgic_redist_fault, NULL);
+    success = fault_register_vm_exception_handler(GIC_REDIST_PADDR, GIC_REDIST_SIZE, vgic_handle_fault_redist, NULL);
     if (!success) {
         LOG_VMM_ERR("Failed to register fault handler for GIC redistributor region\n");
         return false;
@@ -71,10 +71,14 @@ bool virq_controller_init(size_t boot_vcpu_id) {
     return true;
 }
 
-bool virq_inject(size_t vcpu_id, int irq) {
+bool virq_inject_vcpu(size_t vcpu_id, int irq) {
     return vgic_inject_irq(vcpu_id, irq);
 }
 
+bool virq_inject(int irq) {
+    return vgic_inject_irq(GUEST_VCPU_ID, irq);
+}
+
 bool virq_register(size_t vcpu_id, size_t virq_num, virq_ack_fn_t ack_fn, void *ack_data) {
     return vgic_register_irq(vcpu_id, virq_num, ack_fn, ack_data);
 }
diff --git a/src/virtio/block.c b/src/virtio/block.c
index 4844fb74..16077ae9 100644
--- a/src/virtio/block.c
+++ b/src/virtio/block.c
@@ -136,7 +136,7 @@ static void virtio_blk_used_buffer(struct virtio_device *dev, uint16_t desc)
 
 static bool virtio_blk_virq_inject(struct virtio_device *dev)
 {
-    return virq_inject(GUEST_VCPU_ID, dev->virq);
+    return virq_inject(dev->virq);
 }
 
 static void virtio_blk_set_interrupt_status(struct virtio_device *dev,
diff --git a/src/virtio/console.c b/src/virtio/console.c
index c21311a9..394dceda 100644
--- a/src/virtio/console.c
+++ b/src/virtio/console.c
@@ -162,7 +162,7 @@ static bool virtio_console_handle_tx(struct virtio_device *dev)
      * available data. In this case we do not set the IRQ status. */
     if (transferred) {
         dev->data.InterruptStatus = BIT_LOW(0);
-        bool success = virq_inject(GUEST_VCPU_ID, dev->virq);
+        bool success = virq_inject(dev->virq);
         assert(success);
 
         if (serial_require_producer_signal(&console->txq)) {
@@ -221,7 +221,7 @@ bool virtio_console_handle_rx(struct virtio_console_device *console)
      * available data. In this case we do not set the IRQ status. */
     if (transferred) {
         console->virtio_device.data.InterruptStatus = BIT_LOW(0);
-        bool success = virq_inject(GUEST_VCPU_ID, console->virtio_device.virq);
+        bool success = virq_inject(console->virtio_device.virq);
         assert(success);
 
         return success;
diff --git a/src/virtio/net.c b/src/virtio/net.c
index a47e4c96..c75ae34a 100644
--- a/src/virtio/net.c
+++ b/src/virtio/net.c
@@ -138,7 +138,7 @@ static void virtq_enqueue_used(struct virtq *virtq, uint32_t desc_head, uint32_t
 static bool virtio_net_respond(struct virtio_device *dev)
 {
     dev->data.InterruptStatus = BIT_LOW(0);
-    bool success = virq_inject(GUEST_VCPU_ID, dev->virq);
+    bool success = virq_inject(dev->virq);
     assert(success);
 
     return success;
diff --git a/src/virtio/sound.c b/src/virtio/sound.c
index a4b1c398..f32f9c0a 100644
--- a/src/virtio/sound.c
+++ b/src/virtio/sound.c
@@ -147,7 +147,7 @@ static const char *code_to_str(uint32_t code)
 static void virtio_snd_respond(struct virtio_device *dev)
 {
     dev->data.InterruptStatus = BIT_LOW(0);
-    bool success = virq_inject(GUEST_VCPU_ID, dev->virq);
+    bool success = virq_inject(dev->virq);
     assert(success);
 }