diff --git a/.gitignore b/.gitignore
index 6ba393481..e1be4ea72 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
 build/
 *.pdf
+zig-out/
+zig-cache/
 
diff --git a/board/qemu_arm_virt_hyp/systems/two_vms.system b/board/qemu_arm_virt_hyp/systems/two_vms.system
deleted file mode 100644
index 787a9f745..000000000
--- a/board/qemu_arm_virt_hyp/systems/two_vms.system
+++ /dev/null
@@ -1,35 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!--
- Copyright 2022, UNSW (ABN 57 195 873 179)
-
- SPDX-License-Identifier: BSD-2-Clause
--->
-<system>
-    <memory_region name="serial" size="0x1_000" phys_addr="0x9000000" />
-    <memory_region name="guest_ram-1" size="0x10_000_000" page_size="0x200_000" />
-    <memory_region name="guest_ram-2" size="0x10_000_000" page_size="0x200_000" />
-    <memory_region name="gic_vcpu" size="0x1_000" phys_addr="0x8040000" />
-
-    <protection_domain name="VMM-1" priority="254">
-        <program_image path="vmm.elf" />
-        <map mr="guest_ram-1" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
-        <virtual_machine name="linux" id="0">
-            <map mr="guest_ram-1" vaddr="0x40000000" perms="rwx" />
-
-            <map mr="serial" vaddr="0x9000000" perms="rw" />
-            <map mr="gic_vcpu" vaddr="0x8010000" perms="rw" />
-        </virtual_machine>
-        <irq irq="33" id="1" />
-    </protection_domain>
-
-    <protection_domain name="VMM-2" priority="254">
-        <program_image path="vmm.elf" />
-        <map mr="guest_ram-2" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
-        <virtual_machine name="linux" id="0">
-            <map mr="guest_ram-2" vaddr="0x40000000" perms="rwx" />
-
-            <map mr="serial" vaddr="0x9000000" perms="rw" />
-            <map mr="gic_vcpu" vaddr="0x8010000" perms="rw" />
-        </virtual_machine>
-    </protection_domain>
-</system>
diff --git a/examples/simple/Makefile b/examples/simple/Makefile
new file mode 100644
index 000000000..b5bddeabd
--- /dev/null
+++ b/examples/simple/Makefile
@@ -0,0 +1,143 @@
+#
+# Copyright 2021, Breakaway Consulting Pty. Ltd.
+# Copyright 2022, UNSW (ABN 57 195 873 179)
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(SEL4CP_SDK)),)
+$(error SEL4CP_SDK must be specified)
+endif
+
+ifeq ($(strip $(BOARD)),)
+$(error BOARD must be specified)
+endif
+
+ifeq ($(strip $(CONFIG)),)
+$(error CONFIG must be specified)
+endif
+
+ifeq ($(strip $(SYSTEM)),)
+$(error SYSTEM must be specified)
+endif
+
+# @ivanv: Check for dependencies and make sure they are installed/in the path
+
+# @ivanv: check that all dependencies exist
+# Specify that we use bash for all shell commands
+SHELL=/bin/bash
+# All dependencies needed to compile the VMM
+QEMU := qemu-system-aarch64
+DTC := dtc
+
+ifndef TOOLCHAIN
+	# Get whether the common toolchain triples exist
+	TOOLCHAIN_AARCH64_LINUX_GNU := $(shell command -v aarch64-linux-gnu-gcc 2> /dev/null)
+	TOOLCHAIN_AARCH64_UNKNOWN_LINUX_GNU := $(shell command -v aarch64-unknown-linux-gnu-gcc 2> /dev/null)
+	# Then check if they are defined and select the appropriate one
+	ifdef TOOLCHAIN_AARCH64_LINUX_GNU
+		TOOLCHAIN := aarch64-linux-gnu
+	else ifdef TOOLCHAIN_AARCH64_UNKNOWN_LINUX_GNU
+		TOOLCHAIN := aarch64-unknown-linux-gnu
+	else
+		$(error "Could not find an AArch64 cross-compiler")
+	endif
+endif
+
+CC := $(TOOLCHAIN)-gcc
+LD := $(TOOLCHAIN)-ld
+AS := $(TOOLCHAIN)-as
+SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
+
+# @ivanv: need to have a step for putting in the initrd node into the DTB,
+# 		  right now it is unfortunately hard-coded.
+
+# @ivanv: check that the path of SDK_PATH/BOARD exists
+# @ivanv: Have a list of supported boards to check with, if it's not one of those
+# have a helpful message that lists all the support boards.
+
+# @ivanv: incremental builds don't work with IMAGE_DIR changing
+
+BOARD_DIR := $(SEL4CP_SDK)/board/$(BOARD)/$(CONFIG)
+VMM_SRC_DIR := ../../src
+SYSTEM_DESCRIPTION := board/$(BOARD)/$(SYSTEM)
+
+IMAGE_DIR := board/$(BOARD)
+KERNEL_IMAGE := $(IMAGE_DIR)/linux
+DTS := $(IMAGE_DIR)/linux.dts
+DTB_IMAGE := $(BUILD_DIR)/linux.dtb
+INITRD_IMAGE := $(IMAGE_DIR)/rootfs.cpio.gz
+IMAGES := vmm.elf
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+
+# @ivanv: should only compile printf.o in debug
+VMM_OBJS := vmm.o printf.o virq.o linux.o guest.o psci.o smc.o fault.o util.o vgic.o package_guest_images.o
+
+# @ivanv: hack...
+# This step should be done based on the DTB
+ifeq ($(BOARD),imx8mm_evk)
+	VMM_OBJS += vgic_v3.o
+else
+	VMM_OBJS += vgic_v2.o
+endif
+
+# Toolchain flags
+# FIXME: For optimisation we should consider providing the flag -mcpu.
+# FIXME: We should also consider whether -mgeneral-regs-only should be
+# used to avoid the use of the FPU and therefore seL4 does not have to
+# context switch the FPU.
+CFLAGS := -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall -Wno-unused-function -Werror -I$(VMM_SRC_DIR)/arch/aarch64 -I$(VMM_SRC_DIR)/util -I$(BOARD_DIR)/include -DBOARD_$(BOARD) -DCONFIG_$(CONFIG)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lsel4cp -Tsel4cp.ld
+
+all: directories $(IMAGE_FILE)
+
+run: all
+	# @ivanv: check that the amount of RAM given to QEMU is at least the number of RAM that QEMU is setup with for seL4.
+	if ! command -v $(QEMU) &> /dev/null; then echo "Could not find dependenyc: qemu-system-aarch64"; exit 1; fi
+	$(QEMU) -machine virt,virtualization=on,highmem=off,secure=off \
+			-cpu cortex-a53 \
+			-serial mon:stdio \
+			-device loader,file=$(IMAGE_FILE),addr=0x70000000,cpu-num=0 \
+			-m size=2G \
+			-nographic
+
+directories:
+	$(shell mkdir -p $(BUILD_DIR))
+
+$(DTB_IMAGE): $(DTS)
+	if ! command -v $(DTC) &> /dev/null; then echo "Could not find dependency: Device Tree Compiler (dtc)"; exit 1; fi
+	# @ivanv: Shouldn't supress warnings
+	$(DTC) -q -I dts -O dtb $< > $@
+
+$(BUILD_DIR)/package_guest_images.o: package_guest_images.S $(IMAGE_DIR) $(KERNEL_IMAGE) $(INITRD_IMAGE) $(DTB_IMAGE)
+	$(CC) -c -g3 -x assembler-with-cpp \
+					-DGUEST_KERNEL_IMAGE_PATH=\"$(KERNEL_IMAGE)\" \
+					-DGUEST_DTB_IMAGE_PATH=\"$(DTB_IMAGE)\" \
+					-DGUEST_INITRD_IMAGE_PATH=\"$(INITRD_IMAGE)\" \
+					$< -o $@
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/util/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/arch/aarch64/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/arch/aarch64/vgic/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/vmm.elf: $(addprefix $(BUILD_DIR)/, $(VMM_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) $(SYSTEM_DESCRIPTION) $(IMAGE_DIR)
+	$(SEL4CP_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
diff --git a/board/qemu_arm_virt_hyp/images/README.md b/examples/simple/board/qemu_arm_virt_hyp/README.md
similarity index 100%
rename from board/qemu_arm_virt_hyp/images/README.md
rename to examples/simple/board/qemu_arm_virt_hyp/README.md
diff --git a/board/qemu_arm_virt_hyp/images/buildroot_config b/examples/simple/board/qemu_arm_virt_hyp/buildroot_config
similarity index 100%
rename from board/qemu_arm_virt_hyp/images/buildroot_config
rename to examples/simple/board/qemu_arm_virt_hyp/buildroot_config
diff --git a/board/qemu_arm_virt_hyp/images/linux b/examples/simple/board/qemu_arm_virt_hyp/linux
similarity index 100%
rename from board/qemu_arm_virt_hyp/images/linux
rename to examples/simple/board/qemu_arm_virt_hyp/linux
diff --git a/board/qemu_arm_virt_hyp/images/linux.dts b/examples/simple/board/qemu_arm_virt_hyp/linux.dts
similarity index 100%
rename from board/qemu_arm_virt_hyp/images/linux.dts
rename to examples/simple/board/qemu_arm_virt_hyp/linux.dts
diff --git a/board/qemu_arm_virt_hyp/images/linux_config b/examples/simple/board/qemu_arm_virt_hyp/linux_config
similarity index 100%
rename from board/qemu_arm_virt_hyp/images/linux_config
rename to examples/simple/board/qemu_arm_virt_hyp/linux_config
diff --git a/board/qemu_arm_virt_hyp/images/rootfs.cpio.gz b/examples/simple/board/qemu_arm_virt_hyp/rootfs.cpio.gz
similarity index 100%
rename from board/qemu_arm_virt_hyp/images/rootfs.cpio.gz
rename to examples/simple/board/qemu_arm_virt_hyp/rootfs.cpio.gz
diff --git a/board/qemu_arm_virt_hyp/systems/simple.system b/examples/simple/board/qemu_arm_virt_hyp/simple.system
similarity index 95%
rename from board/qemu_arm_virt_hyp/systems/simple.system
rename to examples/simple/board/qemu_arm_virt_hyp/simple.system
index 2dc6e74f2..e87fcdea6 100644
--- a/board/qemu_arm_virt_hyp/systems/simple.system
+++ b/examples/simple/board/qemu_arm_virt_hyp/simple.system
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!--
- Copyright 2022, UNSW (ABN 57 195 873 179)
+ Copyright 2023, UNSW
 
  SPDX-License-Identifier: BSD-2-Clause
 -->
@@ -35,7 +35,7 @@
             starting address of RAM is 0x40000000, so we map in the guest RAM
             at the same address in the VMMs virutal address space.
         -->
-        <map mr="guest_ram" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
+        <map mr="guest_ram" vaddr="0x40000000" perms="rw" />
         <virtual_machine name="linux" id="0">
             <!--
              The device tree given to Linux specifies that RAM will start
diff --git a/examples/simple/build.zig b/examples/simple/build.zig
new file mode 100644
index 000000000..d11f81b69
--- /dev/null
+++ b/examples/simple/build.zig
@@ -0,0 +1,144 @@
+const std = @import("std");
+
+pub fn build(b: *std.Build) void {
+    const target = b.standardTargetOptions(.{});
+    // @ivanv: need to somehow relate sel4cp config with this optimisation level?
+    const optimize = b.standardOptimizeOption(.{});
+
+    // @ivanv sort out
+    const sdk_path = "/Users/ivanv/ts/sel4cp_dev/release/sel4cp-sdk-1.2.6";
+    const board = "qemu_arm_virt_hyp";
+    const config = "debug";
+    // Since we are relying on Zig to produce the final ELF, it needs to do the
+    // linking step as well.
+    const sdk_board_dir = sdk_path ++ "/board/" ++ board ++ "/" ++ config;
+
+    const vmmlib = b.addStaticLibrary(.{
+        .name = "vmm",
+        .target = target,
+        .optimize = optimize,
+    });
+
+    // The paths are required to have quotes around them
+    const linux_image_path = "\"board/" ++ board ++ "/linux\"";
+    // @ivanv: come back to
+    const dtb_image_path = "\"build/linux.dtb\"";
+    const initrd_image_path = "\"board/" ++ board ++ "/rootfs.cpio.gz\"";
+
+    const vmm_src_dir = "../../src/";
+    // @ivanv: obviously for other archs we want a different dir
+    const vmm_src_arch_dir = vmm_src_dir ++ "arch/aarch64/";
+    vmmlib.addCSourceFiles(&.{
+        vmm_src_dir ++ "guest.c",
+        vmm_src_dir ++ "util/util.c",
+        vmm_src_dir ++ "util/printf.c",
+        vmm_src_arch_dir ++ "vgic/vgic.c",
+        vmm_src_arch_dir ++ "vgic/vgic_v2.c",
+        vmm_src_arch_dir ++ "fault.c",
+        vmm_src_arch_dir ++ "psci.c",
+        vmm_src_arch_dir ++ "smc.c",
+        vmm_src_arch_dir ++ "virq.c",
+        vmm_src_arch_dir ++ "linux.c",
+    }, &.{
+        "-Wall",
+        "-Werror",
+        "-Wno-unused-function",
+        "-mstrict-align",
+        "-DBOARD_qemu_arm_virt_hyp",
+    });
+
+    vmmlib.addIncludePath(vmm_src_dir);
+    vmmlib.addIncludePath(vmm_src_dir ++ "util/");
+    vmmlib.addIncludePath(vmm_src_arch_dir);
+    vmmlib.addIncludePath(vmm_src_arch_dir ++ "vgic/");
+    vmmlib.addIncludePath(sdk_board_dir ++ "/include");
+
+    b.installArtifact(vmmlib);
+
+    const exe = b.addExecutable(.{
+        .name = "vmm.elf",
+        .target = target,
+        .optimize = optimize,
+    });
+
+    // Add sel4cp.h to be used by the API wrapper.
+    exe.addIncludePath(sdk_board_dir ++ "/include");
+    exe.addIncludePath(vmm_src_dir);
+    exe.addIncludePath(vmm_src_arch_dir);
+    // Add the static library that provides each protection domain's entry
+    // point (`main()`), which runs the main handler loop.
+    exe.addObjectFile(sdk_board_dir ++ "/lib/libsel4cp.a");
+    exe.linkLibrary(vmmlib);
+    // Specify the linker script, this is necessary to set the ELF entry point address.
+    exe.setLinkerScriptPath(.{ .path = sdk_board_dir ++ "/lib/sel4cp.ld"});
+
+    exe.addCSourceFiles(&.{"vmm.c"}, &.{
+        "-Wall",
+        "-Werror",
+        "-Wno-unused-function",
+        "-mstrict-align",
+        "-DBOARD_qemu_arm_virt_hyp",
+    });
+
+    const guest_images = b.addObject(.{
+        .name = "guest_images",
+        .target = target,
+        .optimize = optimize,
+    });
+
+    guest_images.addCSourceFiles(&.{"package_guest_images.S"}, &.{
+        "-DGUEST_KERNEL_IMAGE_PATH=" ++ linux_image_path,
+        "-DGUEST_DTB_IMAGE_PATH=" ++ dtb_image_path,
+        "-DGUEST_INITRD_IMAGE_PATH=" ++ initrd_image_path,
+        "-x",
+        "assembler-with-cpp",
+    });
+
+    exe.addObject(guest_images);
+    b.installArtifact(exe);
+
+    const system_description_path = "board/" ++ board ++ "/simple.system";
+    const sel4cp_tool_cmd = b.addSystemCommand(&[_][]const u8{
+       sdk_path ++ "/bin/sel4cp",
+       system_description_path,
+       "--search-path",
+       "zig-out/bin",
+       "--board",
+       board,
+       "--config",
+       config,
+       "-o",
+       "zig-out/bin/loader.img",
+       "-r",
+       "zig-out/report.txt",
+    });
+    // Running the seL4CP tool depends on 
+    sel4cp_tool_cmd.step.dependOn(b.getInstallStep());
+    // Add the "sel4cp" step, and make it the default step when we execute `zig build`>
+    const sel4cp_step = b.step("sel4cp", "Compile and build the final bootable image");
+    sel4cp_step.dependOn(&sel4cp_tool_cmd.step);
+    b.default_step = sel4cp_step;
+
+    // This is setting up a `simulate` command for running the system via QEMU,
+    // which we only want to do when we have a board that we can actually simulate.
+    // @ivanv we should try get renode working as well
+    if (std.mem.eql(u8, board, "qemu_arm_virt_hyp")) {
+        const simulate_cmd = b.addSystemCommand(&[_][]const u8{
+            "qemu-system-aarch64",
+            "-machine",
+            "virt,virtualization=on,highmem=off,secure=off",
+            "-cpu",
+            "cortex-a53",
+            "-serial",
+            "mon:stdio",
+            "-device",
+            "loader,file=zig-out/bin/loader.img,addr=0x70000000,cpu-num=0",
+            "-m",
+            "2G",
+            "-nographic",
+        });
+        simulate_cmd.step.dependOn(b.default_step);
+        const simulate_step = b.step("simulate", "Simulate the image via QEMU");
+        simulate_step.dependOn(&simulate_cmd.step);
+    }
+}
diff --git a/examples/simple/package_guest_images.S b/examples/simple/package_guest_images.S
new file mode 100644
index 000000000..e12efb9ad
--- /dev/null
+++ b/examples/simple/package_guest_images.S
@@ -0,0 +1,32 @@
+/*
+ * Copyright 2023, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+/* @probits is used to say that this section contains data. */
+/* The attributes "aw" is to say that the section is allocatable and that it is writeable. */
+
+#if defined(GUEST_KERNEL_IMAGE_PATH)
+.section .guest_kernel_image, "aw", @progbits
+.global _guest_kernel_image, _guest_kernel_image_end
+_guest_kernel_image:
+.incbin GUEST_KERNEL_IMAGE_PATH
+_guest_kernel_image_end:
+#endif
+
+#if defined(GUEST_DTB_IMAGE_PATH)
+.section .guest_dtb_image, "aw", @progbits
+.global _guest_dtb_image, _guest_dtb_image_end
+_guest_dtb_image:
+.incbin GUEST_DTB_IMAGE_PATH
+_guest_dtb_image_end:
+#endif
+
+#if defined(GUEST_INITRD_IMAGE_PATH)
+.section .guest_initrd_image, "aw", @progbits
+.global _guest_initrd_image, _guest_initrd_image_end
+_guest_initrd_image:
+.incbin GUEST_INITRD_IMAGE_PATH
+_guest_initrd_image_end:
+#endif
diff --git a/examples/simple/vmm.c b/examples/simple/vmm.c
new file mode 100644
index 000000000..b5ee8d5ba
--- /dev/null
+++ b/examples/simple/vmm.c
@@ -0,0 +1,186 @@
+/*
+ * Copyright 2023, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stddef.h>
+#include <sel4cp.h>
+// @ivanv: sort these include lines out!
+#include "../../src/util/util.h"
+#include "../../src/arch/aarch64/vgic/vgic.h"
+#include "../../src/arch/aarch64/linux.h"
+#include "../../src/arch/aarch64/tcb.h"
+#include "../../src/arch/aarch64/vcpu.h"
+#include "../../src/arch/aarch64/fault.h"
+#include "../../src/guest.h"
+#include "../../src/virq.h"
+
+#include <stdint.h>
+
+// @ivanv: ideally we would have none of these hardcoded values
+// initrd, ram size come from the DTB
+// We can probably add a node for the DTB addr and then use that.
+// Part of the problem is that we might need multiple DTBs for the same example
+// e.g one DTB for VMM one, one DTB for VMM two. we should be able to hide all
+// of this in the build system to avoid doing any run-time DTB stuff.
+#if defined(BOARD_qemu_arm_virt_hyp)
+#define GUEST_DTB_VADDR 0x4f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x4d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_rpi4b_hyp)
+#define GUEST_DTB_VADDR 0x2e000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x2d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_odroidc2_hyp)
+#define GUEST_DTB_VADDR 0x2f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x2d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_odroidc4_hyp)
+#define GUEST_DTB_VADDR 0x2f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x2d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_imx8mm_evk_hyp)
+#define GUEST_DTB_VADDR 0x4f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x4d700000
+#define GUEST_RAM_SIZE 0x10000000
+#else
+#error Need to define VM image address and DTB address
+#endif
+
+/* For simplicity we just enforce the serial IRQ channel to be the same across platforms. */
+#define SERIAL_IRQ_CH 1
+
+#if defined(BOARD_qemu_arm_virt_hyp)
+#define SERIAL_IRQ 33
+#elif defined(BOARD_odroidc2_hyp) || defined(BOARD_odroidc4_hyp)
+#define SERIAL_IRQ 225
+#elif defined(BOARD_rpi4b_hyp)
+#define SERIAL_IRQ 57
+#elif defined(BOARD_imx8mm_evk_hyp)
+#define SERIAL_IRQ 79
+#else
+#error Need to define serial interrupt
+#endif
+
+/* Data for the guest's kernel image. */
+extern char _guest_kernel_image[];
+extern char _guest_kernel_image_end[];
+/* Data for the device tree to be passed to the kernel. */
+extern char _guest_dtb_image[];
+extern char _guest_dtb_image_end[];
+/* Data for the initial RAM disk to be passed to the kernel. */
+extern char _guest_initrd_image[];
+extern char _guest_initrd_image_end[];
+/* seL4CP will set this variable to the start of the guest RAM memory region. */
+// @ivanv come back to
+uintptr_t guest_ram_vaddr = 0x40000000;
+
+static void serial_ack(size_t vcpu_id, int irq, void *cookie) {
+    /*
+     * For now we by default simply ack the serial IRQ, we have not
+     * come across a case yet where more than this needs to be done.
+     */
+    sel4cp_irq_ack(SERIAL_IRQ_CH);
+}
+
+void init(void) {
+    /* Initialise the VMM, the VCPU(s), and start the guest */
+    LOG_VMM("starting \"%s\"\n", sel4cp_name);
+    /* Place all the binaries in the right locations before starting the guest */
+    size_t kernel_size = _guest_kernel_image_end - _guest_kernel_image;
+    size_t dtb_size = _guest_dtb_image_end - _guest_dtb_image;
+    size_t initrd_size = _guest_initrd_image_end - _guest_initrd_image;
+    uintptr_t kernel_pc = linux_setup_images(guest_ram_vaddr,
+                                      (uintptr_t) _guest_kernel_image,
+                                      kernel_size,
+                                      (uintptr_t) _guest_dtb_image,
+                                      GUEST_DTB_VADDR,
+                                      dtb_size,
+                                      (uintptr_t) _guest_initrd_image,
+                                      GUEST_INIT_RAM_DISK_VADDR,
+                                      initrd_size
+                                      );
+    if (!kernel_pc) {
+        LOG_VMM_ERR("Failed to initialise guest images\n");
+        return;
+    }
+    /* Initialise the virtual GIC driver */
+    bool success = virq_controller_init(GUEST_VCPU_ID);
+    if (!success) {
+        LOG_VMM_ERR("Failed to initialise emulated interrupt controller\n");
+        return;
+    }
+    // @ivanv: Note that remove this line causes the VMM to fault if we
+    // actually get the interrupt. This should be avoided by making the VGIC driver more stable.
+    success = virq_register(GUEST_VCPU_ID, SERIAL_IRQ, &serial_ack, NULL);
+    /* Just in case there is already an interrupt available to handle, we ack it here. */
+    sel4cp_irq_ack(SERIAL_IRQ_CH);
+    /* Finally start the guest */
+    guest_start(GUEST_VCPU_ID, kernel_pc, GUEST_DTB_VADDR, GUEST_INIT_RAM_DISK_VADDR);
+}
+
+void notified(sel4cp_channel ch) {
+    switch (ch) {
+        case SERIAL_IRQ_CH: {
+            bool success = virq_inject(GUEST_VCPU_ID, SERIAL_IRQ);
+            if (!success) {
+                LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", SERIAL_IRQ, GUEST_VCPU_ID);
+            }
+            break;
+        }
+        default:
+            printf("Unexpected channel, ch: 0x%lx\n", ch);
+    }
+}
+
+/*
+ * The primary purpose of the VMM after initialisation is to act as a fault-handler,
+ * whenever our guest causes an exception, it gets delivered to this entry point for
+ * the VMM to handle.
+ */
+void fault(sel4cp_id id, sel4cp_msginfo msginfo) {
+    if (id != GUEST_VCPU_ID) {
+        LOG_VMM_ERR("Unexpected fault from entity with ID 0x%lx\n", id);
+        return;
+    }
+
+    size_t label = sel4cp_msginfo_get_label(msginfo);
+    bool success = false;
+    switch (label) {
+        case seL4_Fault_VMFault:
+            success = handle_vm_fault(id);
+            break;
+        case seL4_Fault_UnknownSyscall:
+            success = handle_unknown_syscall(id);
+            break;
+        case seL4_Fault_UserException:
+            success = handle_user_exception(id);
+            break;
+        case seL4_Fault_VGICMaintenance:
+            success = handle_vgic_maintenance(id);
+            break;
+        case seL4_Fault_VCPUFault:
+            success = handle_vcpu_fault(id);
+            break;
+        case seL4_Fault_VPPIEvent:
+            success = handle_vppi_event(id);
+            break;
+        default:
+            /* We have reached a genuinely unexpected case, stop the guest. */
+            LOG_VMM_ERR("unknown fault label 0x%lx, stopping guest with ID 0x%lx\n", label, id);
+            sel4cp_vm_stop(id);
+            /* Dump the TCB and vCPU registers to hopefully get information as
+             * to what has gone wrong. */
+            tcb_print_regs(id);
+            vcpu_print_regs(id);
+            return;
+    }
+
+    if (success) {
+        /* Now that we have handled the fault successfully, we reply to it so
+         * that the guest can resume execution. */
+        sel4cp_fault_reply(sel4cp_msginfo_new(0, 0));
+    } else {
+        LOG_VMM_ERR("Failed to handle %s fault\n", fault_to_string(label));
+    }
+}