libsel4vmmplatsupport: Update documentation

This commit refreshes the interface documentation in
libsel4vmmplatsupport. This commit patches in missing documentation
and additionally ensures all interface documentation conforms to
Doxygen style comments.
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/ac_device.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/ac_device.h
index ca931ab..a175ab3 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/ac_device.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/ac_device.h
@@ -12,6 +12,14 @@
 
 #pragma once
 
+/***
+ * @module ac_device.h
+ * The ARM access control device interface facilitates the creation of generic virtual devices in a VM instance with
+ * access control permissions over the devices addressable memory. An access controlled device is often used to abstract
+ * the memory of a specific platform hardware device e.g a clock device. This allows the user to present hardware devices
+ * to a VM instance but limit their permissions with regards to modifying its register state.
+ */
+
 #include <sel4vm/guest_vm.h>
 
 #include <sel4vmmplatsupport/device.h>
@@ -27,23 +35,24 @@
     VACDEV_REPORT_AND_MASK
 };
 
-/**
+/***
+ * @function vm_install_generic_ac_device(vm, d, mask, size, action)
  * Installs a generic access controlled device
- * @param[in] vm     The VM to install the device into
- * @param[in] d      A description of the device to install
- * @param[in] mask   An access mask. The mask provides a map of device bits that
- *                   are modifiable by the guest.
- *                   '1' represents bits that the guest can read and write
- *                   '0' represents bits that can only be read by the guest
- *                   Underlying memory for the mask should remain accessible for
- *                   the life of this device. The mask may be updated at run time
- *                   on demand.
- * @param[in] size   The size of the mask. This is useful for conserving memory in
- *                   cases where the underlying device does not occupy a full
- *                   page. If an access lies outside of the range of the mask,
- *                   guest access.
- * @param[in] action Action to take when access is violated.
- * @return           0 on success
+ * @param {vm_t *} vm                       The VM to install the device into
+ * @param {const struct device *} d         A description of the device to install
+ * @param {void *} mask                     An access mask. The mask provides a map of device bits that
+ *                                          are modifiable by the guest.
+ *                                          '1' represents bits that the guest can read and write
+                                            '0' represents bits that can only be read by the guest
+ *                                          Underlying memory for the mask should remain accessible for
+ *                                          the life of this device. The mask may be updated at run time
+ *                                          on demand.
+ * @param {size_t} size                     The size of the mask. This is useful for conserving memory in
+ *                                          cases where the underlying device does not occupy a full
+ *                                          page. If an access lies outside of the range of the mask,
+ *                                          guest access.
+ * @param {enum vacdev_action} action       Action to take when access is violated.
+ * @return                                  0 on success, -1 on error
  */
 int vm_install_generic_ac_device(vm_t *vm, const struct device *d, void *mask,
                                  size_t size, enum vacdev_action action);
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/generic_forward_device.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/generic_forward_device.h
index 4428cd0..a941bc1 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/generic_forward_device.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/generic_forward_device.h
@@ -11,25 +11,40 @@
  */
 #pragma once
 
+/***
+ * @module generic_forward_device.h
+ * This interface facilitates the creation of a virtual device used for
+ * dispatching faults to external handlers. For example when using CAmkES,
+ * a device frame for a real device can be given to a different CAmkES component
+ * and this virtual device will forward read and write faults over a CAmkES
+ * interface so the component can perform or emulate the actions.
+ */
+
 #include <stdint.h>
 #include <sel4vm/guest_vm.h>
 #include <sel4vmmplatsupport/device.h>
 
-/**
- * This virtual device is used for dispatching faults to external handlers.
- * For example when using CAmkES, a device frame for a real device can be given
- * to a different CAmkES component and this virtual device will forward read and
- * write faults over a CAmkES interface so the component can perform or emulate
- * the actions.
- */
-
 typedef void (*forward_write_fn)(uint32_t addr, uint32_t value);
 typedef uint32_t (*forward_read_fn)(uint32_t addr);
 
+/***
+ * @struct generic_forward_cfg
+ * Interface for forwarding read and write faults
+ * @param {forward_write_fn} write_fn   A callback for forwarding write faults
+ * @param {forward_read_fn} read_fn     A callback for forwarding read faults
+ */
 struct generic_forward_cfg {
     forward_write_fn write_fn;
     forward_read_fn read_fn;
 };
 
+/***
+ * @function vm_install_generic_forward_device(vm, d, cfg)
+ * Install the virtual forwarding device into a VM instance
+ * @param {vm_t *} vm                   A handle to the VM
+ * @param {const struct device *}       Virtual device being forwarded
+ * @param {struct generic_forward_cfg}  Interface for forwarding the devices read and write faults
+ * @return                              -1 for error, otherwise 0 for success
+ */
 int vm_install_generic_forward_device(vm_t *vm, const struct device *d,
                                       struct generic_forward_cfg cfg);
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_boot_init.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_boot_init.h
index 14b3912..18644cc 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_boot_init.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_boot_init.h
@@ -10,21 +10,27 @@
  * @TAG(DATA61_BSD)
  */
 
+/***
+ * @module guest_boot_init.h
+ * The libsel4vmmplatsupport arm guest boot init interface provides helpers to initialise the booting state of
+ * a VM instance. This currently only targets booting a Linux guest OS.
+ */
+
 #include <sel4/sel4.h>
 
 #include <sel4vm/guest_vm.h>
 
-/**
+/***
+ * @function vcpu_set_bootargs(vcpu, pc, mach_type, atags)
  * Set the boot args and pc for the VM.
  * For linux:
  *   r0 -> 0
  *   r1 -> MACH_TYPE  (e.g #4151 for EXYNOS5410 eval. platform smdk5410)
  *   r2 -> atags/dtb address
- * @param[in] vm        A handle to a VM
- * @param[in] pc        The initial PC for the VM
- * @param[in] mach_type Linux specific machine ID
- *                      see http://www.arm.linux.org.uk/developer/machines/
- * @param[in] atags     Linux specific IPA of atags. Can also be substituted with dtb address
- * @return              0 on success, otherwise -1 for failure
+ * @param {vm_vcpu_t *} vcpu        A handle to the boot VCPU
+ * @param {seL4_Word} pc            The initial PC for the VM
+ * @param {seL4_Word} mach_type     Linux specific machine ID see http://www.arm.linux.org.uk/developer/machines/
+ * @param {seL4_Word} atags         Linux specific IPA of atags. Can also be substituted with dtb address
+ * @return                          0 on success, otherwise -1 for failure
  */
 int vcpu_set_bootargs(vm_vcpu_t *vcpu, seL4_Word pc, seL4_Word mach_type, seL4_Word atags);
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_reboot.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_reboot.h
index 42551b3..2b0a4f2 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_reboot.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_reboot.h
@@ -12,38 +12,60 @@
 
 #pragma once
 
+/***
+ * @module guest_reboot.h
+ * The guest reboot interface provides a series of helpers for registering callbacks when rebooting the VMM.
+ * This interface giving various VMM components and drivers the ability to reset necessary state on a reboot.
+ */
+
 typedef int (*reboot_hook_fn)(vm_t *vm, void *token);
 
+/***
+ * @struct reboot_hook
+ * Datastructure representing a reboot hook, containing a callback function to invoke when processing the
+ * hook
+ * @param {reboot_hook_fn} fn       Function pointer to reboot callback
+ * @param {void *} token            Cookie passed to reboot callback when invoked
+ */
 typedef struct reboot_hook {
     reboot_hook_fn fn;
     void *token;
 } reboot_hook_t;
 
+/***
+ * @struct reboot_hooks_list
+ * Reboot hooks management datastructure. Contains a list of reboot hooks that a VMM registers
+ * @param {reboot_hook_t *} rb_hooks        List of reboot hooks
+ * @param {size_t} nhooks                   Number of reboot hooks in `rb_hooks` member
+ */
 typedef struct reboot_hooks_list {
     reboot_hook_t *rb_hooks;
     size_t nhooks;
 } reboot_hooks_list_t;
 
-/**
+/***
+ * @function vmm_init_reboot_hooks_list(rb_hooks_list)
  * Initialise state of a given reboot hooks list
- * @param[in] rb_hooks_list     Handle to reboot hooks list
- * @return                      0 for success, otherwise -1 for error
+ * @param {reboot_hooks_list_t *} rb_hooks_list     Handle to reboot hooks list
+ * @return                                          0 for success, otherwise -1 for error
  */
 int vmm_init_reboot_hooks_list(reboot_hooks_list_t *rb_hooks_list);
 
-/**
+/***
+ * @function vmm_register_reboot_callback(rb_hooks_list, hook, token)
  * Register a reboot callback within a given reboot hooks list
- * @param[in] rb_hooks_list     Handle to reboot hooks list
- * @param[in] hook              Reboot callback to be invoked when list is processed
- * @param[in] token             Cookie passed to reboot callback when invoked
- * @return                      0 for success, otherwise -1 for error
+ * @param {reboot_hooks_list_t *} rb_hooks_list     Handle to reboot hooks list
+ * @param {rb_hook_fn} hook                         Reboot callback to be invoked when list is processed
+ * @param {void *} token                            Cookie passed to reboot callback when invoked
+ * @return                                          0 for success, otherwise -1 for error
  */
 int vmm_register_reboot_callback(reboot_hooks_list_t *rb_hooks_list, reboot_hook_fn hook, void *token);
 
-/**
-*  Process the reboot hooks registered in a reboot hooks list
- * @param[in] vm                Handle to vm - passed onto reboot callback
- * @param[in] rb_hooks_list     Handle to reboot hooks list
- * @return                      0 for success, otherwise -1 for error
+/***
+ * @function vmm_process_reboot_callbacks(vm, rb_hooks_list)
+ * Process the reboot hooks registered in a reboot hooks list
+ * @param {vm_t *} vm                               Handle to vm - passed onto reboot callback
+ * @param {reboot_hooks_list_t *} rb_hooks_list     Handle to reboot hooks list
+ * @return                                          0 for success, otherwise -1 for error
  */
 int vmm_process_reboot_callbacks(vm_t *vm, reboot_hooks_list_t *rb_hooks_list);
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_fault.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_fault.h
index f9c6cb4..ee90108 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_fault.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_fault.h
@@ -14,20 +14,30 @@
 
 #include <sel4vm/guest_vm.h>
 
+/***
+ * @module guest_vcpu_fault.h
+ * The arm guest vcpu fault interface provides a module for registering
+ * and processing vcpu faults. The module can be used such that it directly hooks
+ * into an ARM VMMs unhandled vcpu callback interface or wrapped over by another driver. This
+ * module particularly provides useful handlers to vcpu faults relating to SMC and MSR/MRS instructions.
+ */
+
 typedef int (*vcpu_exception_handler_fn)(vm_vcpu_t *vcpu, uint32_t hsr);
 
-/**
+/***
+ * @function vmm_handle_arm_vcpu_exception(vcpu, hsr, cookie)
  * Handle a vcpu exception given the HSR value - Syndrome information
- * The handler can be used such that an ARM VMM can either hook it into
- * the unhandled vcpu callback interface or wrap over it
- * @param[in] vcpu      A handle to the VCPU
- * @param[in] hsr       Syndrome information value describing the exception/fault
+ * @param {vm_vcpu_t *} vcpu        A handle to the faulting VCPU
+ * @param {uint32_t } hsr           Syndrome information value describing the exception/fault
+ * @param {void *} cookie           User supplied cookie to pass onto exception
+ * @return                          -1 on error, otherwise 0 for success
  */
 int vmm_handle_arm_vcpu_exception(vm_vcpu_t *vcpu, uint32_t hsr, void *cookie);
 
-/**
+/***
+ * @function register_arm_vcpu_exception_handler(ec_class, exception_handler)
  * Register a handler to a vcpu exception class
- * @param[in] ec_class              The exception class the handler will be called on
- * @param[in] exception_handler     Pointer to the exception handler
+ * @param {uint32_t} ec_class                               The exception class the handler will be called on
+ * @param {vcpu_exception_handler_fn} exception_handler     Function pointer to the exception handler
  */
 int register_arm_vcpu_exception_handler(uint32_t ec_class, vcpu_exception_handler_fn exception_handler);
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_util.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_util.h
index 68de714..630c960 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_util.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/guest_vcpu_util.h
@@ -10,6 +10,19 @@
  * @TAG(DATA61_BSD)
  */
 
+/***
+ * @module guest_vcpu_util.h
+ * The ARM guest vcpu util interface provides abstractions and helpers for managing libsel4vm vcpus on an ARM platform.
+ */
+
 #include <sel4vmmplatsupport/plat/guest_vcpu_util.h>
 
+/***
+ * @function fdt_generate_plat_vcpu_node(vm, fdt)
+ * Generate a CPU device node for a given fdt. This taking into account
+ * the vcpus created for the VM.
+ * @param {vm_t *} vm       A handle to the VM
+ * @param {void *} fdt      FDT blob to append generated device node
+ * @return                  0 for success, -1 for error
+ */
 int fdt_generate_plat_vcpu_node(vm_t *vm, void *fdt);
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vpci.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vpci.h
index 30dcc36..fd76499 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vpci.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vpci.h
@@ -11,11 +11,37 @@
  */
 #pragma once
 
+/***
+ * @module vpci.h
+ * The libsel4vmmplatsupport vpci interface presents a Virtual PCI driver for ARM-based VM's.
+ * Using the `vmm_pci_space_t` management interface, the vpci driver establishes the configuration
+ * space in the guest VM. The driver also handles and processes all subsequent memory and ioport accesses to the
+ * virtual pci device.
+ */
+
 #include <sel4vm/guest_vm.h>
 #include <sel4vmmplatsupport/plat/vpci.h>
 
 /* Mask to retrieve PCI bar size */
 #define PCI_CFG_BAR_MASK 0xFFFFFFFF
 
+/***
+ * @function vm_install_vpci(vm, io_port, pci)
+ * @param {vm_t *} vm                           A handle to the VM
+ * @param {vmm_io_port_list_t *} io_port        IOPort library instance to emulate io accesses with
+ * @param {vmm_pci_space_t } pci                PCI library instance to emulate PCI device accesses with
+ * @return                                      0 for success, -1 for error
+ */
 int vm_install_vpci(vm_t *vm, vmm_io_port_list_t *io_port, vmm_pci_space_t *pci);
+
+/***
+ * @function fdt_generate_vpci_node(vm, pci, fdt, gic_phandle)
+ * Generate a PCI device node for a given fdt. This taking into account
+ * the virtual PCI device configuration space.
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {vmm_pci_space_t *}       PCI library instance to generate fdt node
+ * @param {void *} fdt              FDT blob to append generated device node
+ * @param {int} gic_phandle         Phandle of IRQ controller to generate a correct interrupt map property
+ * @return                          0 for success, -1 for error
+ */
 int fdt_generate_vpci_node(vm_t *vm, vmm_pci_space_t *pci, void *fdt, int gic_phandle);
diff --git a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vusb.h b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vusb.h
index 555c8da..ed3c261 100644
--- a/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vusb.h
+++ b/libsel4vmmplatsupport/arch_include/arm/sel4vmmplatsupport/arch/vusb.h
@@ -11,6 +11,11 @@
  */
 #pragma once
 
+/***
+ * @module vusb.h
+ * The libsel4vmmplatsupport vusb interface presents a Virtual USB driver for ARM-based VM's.
+ */
+
 #include <autoconf.h>
 #include <sel4vm/gen_config.h>
 #include <usbdrivers/gen_config.h>
@@ -21,33 +26,32 @@
 #include <sel4/sel4.h>
 
 typedef struct vusb_device vusb_device_t;
-/**
+
+/***
+ * @function vm_install_vusb(vm, hcd, pbase, virq, vmm_ncap, vm_ncap, badge)
  * Install a virtual usb device
- * @param[in] vm       The VM in which to install the device
- * @param[in] hcd      The USB host controller that should be used for USB
- *                     transactions. Calls made to this hcd may be redirected
- *                     for filtering.
- * @param[in] pbase    The guest physical address of the device (2 pages)
- * @param[in] virq     The virtual IRQ number for this device
- * @param[in] vmm_ncap The capability to the endpoint at which the VMM waits
- *                     for notifications.
- * @param[in] vm_ncap  The index at which to install a notification capability
- *                     into the VM
- * @param[in] badge    The seL4 badge which should be applied to the
- *                     notification capability.
- * @return             A handle to the virtual usb device, or NULL on failure
+ * @param {vm_t *} vm               The VM in which to install the device
+ * @param {usb_host_t *} hcd        The USB host controller that should be used for USB transactions.
+ *                                  Calls made to this hcd may be redirected for filtering.
+ * @param {uintptr_t} pbase         The guest physical address of the device (2 pages)
+ * @param {int} virq                The virtual IRQ number for this device
+ * @param {seL4_CPtr} vmm_ncap      The capability to the endpoint at which the VMM waits for notifications.
+ * @param {seL4_CPtr} vm_ncap       The index at which to install a notification capability into the VM
+ * @param {int} badge               The seL4 badge which should be applied to the notification capability.
+ * @return                          A handle to the virtual usb device, or NULL on failure
  */
 vusb_device_t *vm_install_vusb(vm_t *vm, usb_host_t *hcd, uintptr_t pbase,
                                int virq, seL4_CPtr vmm_ncap, seL4_CPtr vm_ncap,
                                int badge);
 
 
-/**
+/***
+ * @function vm_vusb_notify(vusb)
  * This function should be called when a notification is received from the
  * VM. The notification is identifyable by a message on the fault endpoint
  * of the VM which has a badge that matches that which was passed into the
  * vm_install_vusb function.
- * @param[in] vusb  A handle to a virtual usb device
+ * @param {vusb_device_t *} vusb        A handle to a virtual usb device
  */
 void vm_vusb_notify(vusb_device_t *vusb);
 
diff --git a/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/acpi.h b/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/acpi.h
index 275b310..4a290eb 100644
--- a/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/acpi.h
+++ b/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/acpi.h
@@ -12,6 +12,12 @@
 
 #pragma once
 
+/***
+ * @module acpi.h
+ * The ACPI module provides support for generating ACPI table in a guest x86 VM. This being particularly leveraged
+ * for booting a guest Linux VM.
+ */
+
 #define LOWER_BIOS_START (0xE0000)
 #define LOWER_BIOS_SIZE (0xFFFF)
 
@@ -22,4 +28,10 @@
 
 #include <sel4vm/guest_vm.h>
 
+/***
+ * @function make_guest_acpi_tables(vm)
+ * Creates ACPI table for the guest VM
+ * @param {vm_t *} vm       A handle to the guest VM instance
+ * @return                  0 for success, -1 for error
+ */
 int make_guest_acpi_tables(vm_t *vm);
diff --git a/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/drivers/vmm_pci_helper.h b/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/drivers/vmm_pci_helper.h
index ffe988d..75e581b 100644
--- a/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/drivers/vmm_pci_helper.h
+++ b/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/drivers/vmm_pci_helper.h
@@ -10,6 +10,11 @@
  * @TAG(DATA61_BSD)
  */
 
+/***
+ * @module vmm_pci_helper.h
+ * The interface presents a series of helpers for establishing VMM PCI support on x86 platforms.
+ */
+
 #include <sel4vm/guest_vm.h>
 #include <sel4vm/arch/ioports.h>
 #include <sel4vmmplatsupport/drivers/pci_helper.h>
@@ -17,10 +22,36 @@
 #include <pci/virtual_pci.h>
 #include <pci/helper.h>
 
+/***
+ * @function vmm_pci_helper_map_bars(vm, cfg, bars)
+ * Given a PCI device config, map the PCI device bars into the VM, effectively passing-through the
+ * PCI device. This will map MMIO and IO-based bars.
+ * @param {vm_t *} vm                       A handle to the VM
+ * @param {libpci_device_iocfg_t *} cfg     PCI device config
+ * @param {vmm_pci_bar_t *} bars            Resulting PCI bars mapped into the VM
+ * @return                                  -1 for error, otherwise the number of bars mapped into the VM (>=0)
+ */
 int vmm_pci_helper_map_bars(vm_t *vm, libpci_device_iocfg_t *cfg, vmm_pci_bar_t *bars);
 
 /* Functions for emulating PCI config spaces over IO ports */
+/***
+ * @function vmm_pci_io_port_in(vcpu, cookie, port_no, size, result)
+ * Emulates IOPort in access on the VMM Virtual PCI device
+ * @param {vm_vcpu_t *} vcpu            Faulting vcpu performing ioport access
+ * @param {unsigned int} port_no        Port address being accessed
+ * @param {unsigned int} size           Size of ioport access
+ * @param {unsigned int *} result       Pointer that will be populated with resulting data of io-in op
+ */
 ioport_fault_result_t vmm_pci_io_port_in(vm_vcpu_t *vcpu, void *cookie, unsigned int port_no, unsigned int size,
                                          unsigned int *result);
+
+/***
+ * @function vmm_pci_io_port_out(vcpu, cookie, port_no, size, value)
+ * Emulates IOPort out access on the VMM Virtual PCI device
+ * @param {vm_vcpu_t *} vcpu            Faulting vcpu performing ioport access
+ * @param {unsigned int} port_no        Port address being accessed
+ * @param {unsigned int} size           Size of ioport access
+ * @param {unsigned int} value          Value being written in io-out op
+ */
 ioport_fault_result_t vmm_pci_io_port_out(vm_vcpu_t *vcpu, void *cookie, unsigned int port_no, unsigned int size,
                                           unsigned int value);
diff --git a/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/guest_boot_init.h b/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/guest_boot_init.h
index e166f27..6c716b2 100644
--- a/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/guest_boot_init.h
+++ b/libsel4vmmplatsupport/arch_include/x86/sel4vmmplatsupport/arch/guest_boot_init.h
@@ -12,13 +12,39 @@
 
 #pragma once
 
+/***
+ * @module guest_boot_init.h
+ * The libsel4vmmplatsupport x86 guest boot init interface provides helpers to initialise the booting state of
+ * a VM instance. This currently only targets booting a Linux guest OS.
+ */
+
 #include <stdint.h>
 
 #include <sel4vmmplatsupport/guest_image.h>
 
+/***
+ * @function vmm_plat_init_guest_boot_structure(vm, cmdline, guest_kernel_image, guest_ramdisk_image, guest_boot_info_addr)
+ * Establish the necessary BIOS boot structures to initialise and boot a guest Linux OS. This includes the creation of a BIOS
+ * boot info structure, an e820 map and ACPI tables.
+ * @param {vm_t *} vm                                   A handle to the guest VM
+ * @param {const char *} cmdline                        The guest Linux boot commandline
+ * @param {guest_kernel_image_t} guest_kernel_image     Guest kernel image (preloaded into the VM's memory)
+ * @param {guest_image_t} guest_ramdisk_image           Guest ramdisk image (preloaded into the VM's memory)
+ * @param {uintptr_t *} guest_boot_info_addr            Resulting address of loaded generated guest boot info structure
+ *                                                      (in guest physical address space)
+ * @return                                              0 for success, -1 for error
+ */
 int vmm_plat_init_guest_boot_structure(vm_t *vm, const char *cmdline,
                                        guest_kernel_image_t guest_kernel_image, guest_image_t guest_ramdisk_image,
                                        uintptr_t *guest_boot_info_addr);
+
+/***
+ * @function vmm_plat_init_guest_thread_state(vcpu, guest_entry_addr, guest_boot_info_addr)
+ * Initialise the booting state of a guest VM, establishing the necessary thread state to launch a guest Linux OS
+ * @param {vm_vcpu_t *} vcpu                A handle to the boot vcpu
+ * @param {uintptr_t} guest_entry_addr      Address of VM entry point (often entry point defined in kernel elf image)
+ * @param {uintptr_t} guest_boot_info_addr  Address of loaded guest boot info structure
+ * @return                                  0 for success, -1 for error
+ */
 int vmm_plat_init_guest_thread_state(vm_vcpu_t *vcpu, uintptr_t guest_entry_addr,
                                      uintptr_t guest_boot_info_addr);
-
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/device.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/device.h
index ecac81b..f9a8104 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/device.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/device.h
@@ -12,50 +12,65 @@
 
 #pragma once
 
+/***
+ * @module device.h
+ * The device.h interface provides a series of datastructures and helpers to manage VMM devices.
+ */
+
 #include <stdint.h>
 #include <sel4vm/guest_vm.h>
 
-/* Device Management Object */
+/***
+ * @struct device
+ * Device Management Object
+ * @param {const char *} name                                           A string representation of the device. Useful for debugging
+ * @param {seL4_Word} pstart                                            The physical address of the device
+ * @param {seL4_Word} size                                              Device mapping size
+ * @param {int *(vm_t, vm_vcpu_t, dev, addr, len)} handle_device_fault  Fault handler
+ * @param {void *} priv                                                 Device emulation private data
+ *
+ */
 struct device {
-    /* A string representation of the device. Useful for debugging */
     const char *name;
-    /* The physical address of the device */
     seL4_Word pstart;
-    /* Device mapping size */
     seL4_Word size;
-    /* Fault handler */
     int (*handle_device_fault)(vm_t *vm, vm_vcpu_t *vcpu, struct device *dev, uintptr_t addr, size_t len);
-    /* Device emulation private data */
     void *priv;
 };
 
-/*
+/***
+ * @struct device_list
  * Management for a list of devices
+ * @param {struct device *} devices     List of registered devices
+ * @param {int} num_devices             Total number of registered devices
  */
 typedef struct device_list {
     struct device *devices;
     int num_devices;
 } device_list_t;
 
-/*
+/***
+ * @function device_list_init(list)
  * Initialise an empty device list
- * @param list      device list to initialise
- * @return          0 on success, otherwise -1 for error
+ * @param {device_list_t *} list    device list to initialise
+ * @return                          0 on success, otherwise -1 for error
  */
 int device_list_init(device_list_t *list);
 
-/*
+/***
+ * @function add_device(dev_list, d)
  * Add a generic device to a given device list without performing any initialisation of the device
- * @param dev_list  A handle to the device list that the device should be installed into
- * @param device    A description of the device
- * @return          0 on success, otherwise -1 for error
+ * @param {device_list_t *} dev_list        A handle to the device list that the device should be installed into
+ * @param {const struct device *} device    A description of the device
+ * @return                                  0 on success, otherwise -1 for error
  */
 int add_device(device_list_t *dev_list, const struct device *d);
 
-/*
+/***
+ * @function find_device_by_pa(dev_list, addr)
  * Find a device by a given addr within a device list
- * @param dev_list  Device list to search within
- * @param addr      Add to search with
- * @return          Pointer to device if found, otherwise NULL if not found
+ * @param {device_list_t *} dev_list    Device list to search within
+ * @param {uintptr_t} addr              Add to search with
+ * @return                              Pointer to device if found, otherwise NULL if not found
  */
 struct device *find_device_by_pa(device_list_t *dev_list, uintptr_t addr);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/device_utils.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/device_utils.h
index 827e710..5434251 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/device_utils.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/device_utils.h
@@ -12,29 +12,38 @@
 
 #pragma once
 
+/***
+ * @module device_utils.h
+ * The device utils interface provides various helpers to establish different types devices for a given VM
+ * instance.
+ */
+
 #include <sel4vm/guest_vm.h>
 #include <sel4vmmplatsupport/device.h>
 
-/**
+/***
+ * @function vm_install_passthrough_device(vm, device)
  * Install a passthrough device into a VM
- * @param[in] vm     A handle to the VM that the device should be install to
- * @param[in] device A description of the device
- * @return           0 on success
+ * @param {vm_t *} vm                       A handle to the VM that the device should be install to
+ * @param {const struct device *} device    A description of the device
+ * @return                                  0 on success, -1 for error
  */
 int vm_install_passthrough_device(vm_t *vm, const struct device *device);
 
-/**
+/***
+ * @function vm_install_ram_only_device(vm, device)
  * Install a device backed by ram into a VM
- * @param[in] vm     A handle to the VM that the device should be install to
- * @param[in] device A description of the device
- * @return           0 on success
+ * @param {vm_t *} vm                       A handle to the VM that the device should be install to
+ * @param {const struct device *} device    A description of the device
+ * @return                                  0 on success, -1 for error
  */
 int vm_install_ram_only_device(vm_t *vm, const struct device *device);
 
-/**
+/***
+ * @function vm_install_listening_device(vm, device)
  * Install a passthrough device into a VM, but trap and print all access
- * @param[in] vm     A handle to the VM that the device should be install to
- * @param[in] device A description of the device
- * @return           0 on success
+ * @param {vm_t *} vm                       A handle to the VM that the device should be install to
+ * @param {const struct device *} device    A description of the device
+ * @return                                  0 on success, -1 for error
  */
 int vm_install_listening_device(vm_t *vm, const struct device *device);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/cross_vm_connection.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/cross_vm_connection.h
index 8ea5b58..da8ff9b 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/cross_vm_connection.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/cross_vm_connection.h
@@ -12,6 +12,13 @@
 
 #pragma once
 
+/***
+ * @module cross_vm_connection.h
+ * The crossvm connection module facilitates the creation of communication channels between VM's and other
+ * components on a seL4-based system. The module exports registered cross vm connections to a Linux VM such that
+ * processes can access them from userlevel. This being facilitated over a virtual PCI device.
+ */
+
 #include <sel4vm/guest_vm.h>
 
 #include <sel4vmmplatsupport/drivers/virtio.h>
@@ -23,40 +30,55 @@
 typedef int (*consume_callback_fn)(event_callback_fn, void *arg);
 typedef int (*alloc_free_interrupt_fn)(void);
 
-/* Datastructure representing a dataport of a crossvm connection */
+/***
+ * @struct crossvm_dataport_handle
+ * Datastructure representing a dataport of a crossvm connection
+ * @param {size_t} size         The size of the crossvm dataport
+ * @param {int} num_frames      Total number of frames in the `frames` member
+ * @param {seL4_CPtr *} frames  The set of frames backing the dataport
+ */
 typedef struct crossvm_dataport_handle {
     size_t size;
     unsigned int num_frames;
     seL4_CPtr *frames;
 } crossvm_dataport_handle_t;
 
-/* Datastructure representing a single crossvm connection */
+/***
+ * @struct crossvm_handle
+ * Datastructure representing a single crossvm connection
+ * @param {crossvm_dataport_handle_t *} dataport    The dataport associated with the crossvm connection
+ * @param {emit_fn} emit_fn                         The function pointer to the crossvm emit method
+ * @param {seL4_Word} consume_id                    The identifier used for the crossvm connection when receiving incoming notifications
+ *                                                  This is matched on when invoking `consume_connection_event`
+ */
 typedef struct crossvm_handle {
     crossvm_dataport_handle_t *dataport;
     emit_fn emit_fn;
     seL4_Word consume_id;
 } crossvm_handle_t;
 
-/**
+/***
+ * @function cross_vm_connections_init_common(vm, connection_base_addr, connections, num_connections, pci, alloc_irq)
  * Install a set of cross vm connections into a guest VM (for either x86 or ARM VM platforms)
- * @param[in] vm                        A handle to the VM
- * @param[in] connection_base_addr      The base guest physical address that can be used to reserve memory
- *                                      for the crossvm connectors
- * @param[in] connections               The set of crossvm connections to be initialised and installed in the guest
- * @param[in] num_connection            The number of connections passed in through the 'connections' parameter
- * @param[in] pci                       A handle to the VM's host PCI device. The connections are advertised through the
- *                                      PCI device
- * @param[in] alloc_irq                 A function that is used to allocated an irq number for the crossvm connections
- * @return                              -1 on failure otherwise 0 for success
+ * @param {vm_t *} vm                           A handle to the VM
+ * @param {uintptr_t} connection_base_addr      The base guest physical address that can be used to reserve memory
+ *                                              for the crossvm connectors
+ * @param {crossvm_handle_t *} connections      The set of crossvm connections to be initialised and installed in the guest
+ * @param {int} num_connection                  The number of connections passed in through the 'connections' parameter
+ * @param {vmm_pci_space_t *} pci               A handle to the VM's host PCI device. The connections are advertised through the
+ *                                              PCI device
+ * @param {alloc_free_interrupt_fn} alloc_irq   A function that is used to allocated an irq number for the crossvm connections
+ * @return                                      -1 on failure otherwise 0 for success
  */
 int cross_vm_connections_init_common(vm_t *vm, uintptr_t connection_base_addr, crossvm_handle_t *connections,
                                      int num_connections, vmm_pci_space_t *pci, alloc_free_interrupt_fn alloc_irq);
 
-/**
+/***
+ * @function consume_connection_event(vm, event_id, inject_irq)
  * Handler to consume a cross vm connection event. This being called by the VMM when it recieves a notification from an
  * external process. The event is then relayed onto the VM.
- * @param[in] vm                        A handle to the VM
- * @param[in] event_id                  The id that corresponds to the occuring event
- * @param[in] inject_irq                Whether to inject an interrupt into the VM
+ * @param {vm_t *} vm                   A handle to the VM
+ * @param {seL4_Word} event_id          The id that corresponds to the occuring event
+ * @param {bool} inject_irq             Whether to inject an interrupt into the VM
  */
 void consume_connection_event(vm_t *vm, seL4_Word event_id, bool inject_irq);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci.h
index 1557687..24eabf8 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci.h
@@ -9,14 +9,24 @@
  *
  * @TAG(DATA61_BSD)
  */
-/* VMM PCI Driver, which manages the host's PCI devices, and handles guest OS PCI config space
- * read & writes.
-*/
 
 #pragma once
 
+/***
+ * @module pci.h
+ * This interface presents a VMM PCI Driver. This manages the host's PCI devices, and handles guest OS PCI config space
+ * read & writes.
+ */
+
 #include <stdint.h>
 
+/***
+ * @struct vmm_pci_address
+ * Represents a PCI address by Bus/Device/Function
+ * @param {uint8_t} bus     Bus value
+ * @param {uint8_t} dev     Device value
+ * @param {uint8_t} fun     Function value
+ */
 typedef struct vmm_pci_address {
     uint8_t bus;
     uint8_t dev;
@@ -34,31 +44,63 @@
     void (*iowrite32)(void *cookie, vmm_pci_address_t addr, unsigned int offset, uint32_t val);
 } vmm_pci_config_t;
 
-/* Abstract virtual PCI thing. Could be a device or anything. This
- * can be inserted into the virtual PCI configuration space */
+/***
+ * @struct vmm_pci_entry
+ * Abstracts the virtual PCI device. This is is inserted into the virtual PCI configuration space
+ * @param {void *} cookie                                                           User supplied cookie to pass onto callback functions
+ * @param {int *(void *cookie, int offset, int size, uint32_t *result)} ioread      Configuration space read callback
+ * @param {int *(void *cookie, int offset, int size, uint32_t value)} iowrite       Configuration space write callback
+ */
 typedef struct vmm_pci_entry {
-    /* Callback functions for reading or writing its configuration space.
-     * Returns 0 on success, nonzero if an error occured */
     void *cookie;
     int (*ioread)(void *cookie, int offset, int size, uint32_t *result);
     int (*iowrite)(void *cookie, int offset, int size, uint32_t value);
 } vmm_pci_entry_t;
 
+/***
+ * @struct vmm_pci_sapce
+ * Represents a single host virtual PCI space
+ * @param {vmm_pci_entry_t *} bus       The PCI bus, representing 32 devices, each of which has 8 functions
+                                        This only supports one bus at the moment.
+ * @param {uint32_t} conf_port_addr     The current config address for IO port emulation
+ */
 typedef struct vmm_pci_space {
-    /* Only support one bus at the moment. */
     vmm_pci_entry_t *bus0[32][8];
-    /* For IO port emulation this is the current config address */
     uint32_t conf_port_addr;
 } vmm_pci_space_t;
 
-/* Initialize PCI space */
+/***
+ * @function vmm_pci_init(space)
+ * Initialize PCI space
+ * @param {vmm_pci_space_t **} space    Pointer to PCI space being initialised
+ * @return                              0 on success, -1 on error
+ */
 int vmm_pci_init(vmm_pci_space_t **space);
 
-/* Add a PCI entry. Optionally reports where it is located */
+/***
+ * @function vmm_pci_add_entry(space, entry, addr)
+ * Add a PCI entry. Optionally reports where it is located
+ * @param {vmm_pci_space_t *} space         PCI space handle
+ * @param {vmm_pci_entry_t} entry           PCI entry being addr
+ * @param {vmm_pci_addr_t *} addr           Resulting PCI address where entry gets located
+ * @return                                  0 on success, -1 on error
+ */
 int vmm_pci_add_entry(vmm_pci_space_t *space, vmm_pci_entry_t entry, vmm_pci_address_t *addr);
 
-/* Convert config to pci address */
+/***
+ * @function make_addr_reg_from_config(conf, addr, reg)
+ * Convert config to pci address
+ * @param {uint32_t} conf                   Configuration value to convert to pci address
+ * @param {vmm_pci_address_t *} addr        Resulting PCI address
+ * @param {uint8_t *} reg                   Resulting register value
+ */
 void make_addr_reg_from_config(uint32_t conf, vmm_pci_address_t *addr, uint8_t *reg);
 
-/* Find pci device given a pci address (Bus/Dev/Func) */
+/***
+ * @function find_device(self, addr)
+ * Find PCI device given a PCI address (Bus/Dev/Func)
+ * @param {vmm_pci_space_t *} self      PCI space handle
+ * @param {vmm_pci_address_t} addr      PCI address of device
+ * @return                              NULL on error, otherwise pointer to registered pci entry
+ */
 vmm_pci_entry_t *find_device(vmm_pci_space_t *self, vmm_pci_address_t addr);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci_helper.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci_helper.h
index c17c862..ae20aca 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci_helper.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/pci_helper.h
@@ -12,6 +12,12 @@
 
 #pragma once
 
+/***
+ * @module pci.h
+ * This interface presents a series of helpers when using the VMM PCI Driver. These helpers assisting with
+ * the creation of pci device entries and accessors the their configuration spaces.
+ */
+
 #include <stdint.h>
 #include <pci/pci.h>
 
@@ -19,9 +25,44 @@
 
 #define PCI_BAR_OFFSET(b)   (offsetof(vmm_pci_device_def_t, bar##b))
 
-/* Struct definition of a PCI device. This is used for emulating a device from
+/***
+ * @struct vmm_pci_device_def
+ * Struct definition of a PCI device. This is used for emulating a device from
  * purely memory reads. This is not generally useful on its own, but provides
- * a nice skeleton */
+ * a nice skeleton
+ * @param {uint16_t} vendor_id
+ * @param {uint16_t} device_id
+ * @param {uint16_t} command
+ * @param {uint16_t} status
+ * @param {uint8_t} revision_id
+ * @param {uint8_t} prog_if
+ * @param {uint8_t} subclass
+ * @param {uint8_t} class_code
+ * @param {uint8_t} cache_line_size
+ * @param {uint8_t} latency_timer
+ * @param {uint8_t} header_type
+ * @param {uint8_t} bist
+ * @param {uint32_t} bar0
+ * @param {uint32_t} bar1
+ * @param {uint32_t} bar2
+ * @param {uint32_t} bar3
+ * @param {uint32_t} bar4
+ * @param {uint32_t} bar5
+ * @param {uint32_t} cardbus
+ * @param {uint16_t} subsystem_vendor_id
+ * @param {uint16_t} subsystem_id
+ * @param {uint32_t} expansion_rom
+ * @param {uint8_t} caps_pointer
+ * @param {uint8_t} reserved1
+ * @param {uint16_t} reserved2
+ * @param {uint32_t} reserved3
+ * @param {uint8_t} interrupt_line
+ * @param {uint8_t} interrupt_pin
+ * @param {uint8_t} min_grant
+ * @param {uint8_t} max_latency
+ * @param {int} caps_len
+ * @param {void *} caps
+ */
 typedef struct vmm_pci_device_def {
     uint16_t vendor_id;
     uint16_t device_id;
@@ -64,6 +105,13 @@
     PREFETCH_MEM
 } pci_mem_type_t;
 
+/***
+ * @struct vmm_pci_bar
+ * Represents a PCI bar within a device
+ * @param {pci_mem_type_t} mem_type     Type of memory supporting PCI bar
+ * @param {uintptr_t} address           Address of PCI bar
+ * @param {size_t} size_bits            Size of PCI bar in bits
+ */
 typedef struct vmm_pci_bar {
     pci_mem_type_t mem_type;
     /* Address must be size aligned */
@@ -71,6 +119,16 @@
     size_t size_bits;
 } vmm_pci_bar_t;
 
+/***
+ * @struct pci_bar_emulation
+ * Wrapper datastructure over a pci entry and its configuration space. This is leveraged to emulate
+ * BAR accesses in an entries configuration space
+ * @param {vmm_pci_entry_t} passthrough     PCI entry being emulated
+ * @param {int} num_bars                    Number of PCI bars
+ * @param {vmm_pci_bar_t} bars              Set of PCI bars being emulated in the PCI entry
+ * @param {uint32_t} bar_writes             Most recent write to each PCI bar in the configuration space. This avoids
+ *                                          the guest OS over-writing elements in the configuration space
+ */
 typedef struct pci_bar_emulation {
     vmm_pci_entry_t passthrough;
     int num_bars;
@@ -78,18 +136,41 @@
     uint32_t bar_writes[6];
 } pci_bar_emulation_t;
 
+/***
+ * @struct pci_irq_emulation
+ * Wrapper datastructure over a pci entry and its configuration space. This is leveraged to emulate
+ * IRQ line accesses in an entries configuration space
+ * @param {vmm_pci_entry_t} passthrough     PCI entry being emulated
+ * @param {int} irq                         IRQ line value in PCI entry
+ */
 typedef struct pci_irq_emulation {
     vmm_pci_entry_t passthrough;
     int irq;
 } pci_irq_emulation_t;
 
+/***
+ * @struct pci_passthrough_device
+ * Datastructure providing direct passthrough access to a pci entry configuration space
+ * @param {vmm_pci_address_t} addr          Address of PCI device
+ * @param {vmm_pci_config_t} config         Ops for accessing config space
+ */
 typedef struct pci_passthrough_device {
     /* The address on the host system of this device */
     vmm_pci_address_t addr;
-    /* Ops for accessing config space */
     vmm_pci_config_t config;
 } pci_passthrough_device_t;
 
+/***
+ * @struct pci_cap_emulation
+ * Wrappper datastructure over a pci entry and its configuration space. This is leveraged to emulate
+ * capabilities in an entries configuration space.
+ * @param {vmm_pci_entry_t} passthrough     PCI entry being emulation
+ * @param {int} num_caps                    Number of caps in capability space
+ * @param {uint8_t *} caps                  Capability list
+ * @param {int} num_ignore                  Number of disallowed/ignored capability ranges e.g. MSI capabilities
+ * @param {uint8_t *} ignore_start          Array of starting indexes of ignored capability ranges
+ * @param {uint8_t *} ignore_end            Array of ending idexes of ignored capabilities range
+ */
 typedef struct pci_cap_emulation {
     vmm_pci_entry_t passthrough;
     int num_caps;
@@ -99,48 +180,104 @@
     uint8_t *ignore_end;
 } pci_cap_emulation_t;
 
-/* Helper write function that just ignores any writes */
+/***
+ * @function vmm_pci_entry_ignore_write(cookie, offset, size, value)
+ * Helper write function that just ignores any writes
+ * @param {void *} cookie           User supplied PCI entry cookie
+ * @param {int} offset              Offset into PCI device header
+ * @param {int} size                Size of data to be written
+ * @param {uint32_t} value          value to write to PCI device header offset
+ * @return                          Returns 0
+ */
 int vmm_pci_entry_ignore_write(void *cookie, int offset, int size, uint32_t value);
 
-/* Read and write methods for a memory device
- * @param cookie PCI device header
- * @param offset offset into PCI device header
- * @param size size of data to be read
- * @result resulting value read back from PCI device header
- * @return 0 if success, -1 if error
+/***
+ * @function vmm_pci_mem_device_read(cookie, offset, size, result)
+ * Read method for a PCI devices memory
+ * @param {void *} cookie       PCI device header
+ * @param {int} offset          Offset into PCI device header
+ * @param {int} size            Size of data to be read
+ * @result {uint32_t *} result  Resulting value read back from PCI device header
+ * @return                      0 if success, -1 if error
  */
 int vmm_pci_mem_device_read(void *cookie, int offset, int size, uint32_t *result);
 
-/* Read and write methods for a memory device
- * @param cookie PCI device header
- * @param offset offset into PCI device header
- * @param size size of data to be read
- * @value value to write to PCI device header offset
- * @return 0 if success, -1 if error
+/***
+ * @function vmm_pci_mem_device_write(cookie, offset, size, value)
+ * Write method for a PCI devices memory
+ * @param {void *} cookie       PCI device header
+ * @param {int} offset          Offset into PCI device header
+ * @param {int} size            Size of data to be read
+ * @value {uint32_t} value      Value to write to PCI device header offset
+ * @return                      0 if success, -1 if error
  */
 int vmm_pci_mem_device_write(void *cookie, int offset, int size, uint32_t value);
 
+/***
+ * @function define_pci_host_bridge(bridge)
+ * Defines the configuration space values of the PCI host bridge
+ * @param {vmm_pci_device_def_t *} bridge       PCI bridge device definition
+ */
 void define_pci_host_bridge(vmm_pci_device_def_t *bridge);
 
-/* Construct a pure passthrough device based on the real PCI. This is almost always useless as
- * you will almost certainly want to rebase io memory */
+/***
+ * @function vmm_pci_create_passthrough(addr, config)
+ * Construct a pure passthrough device based on the real PCI. This is almost always useless as
+ * you will almost certainly want to rebase io memory
+ * @param {vmm_pci_address_t} addr      Address of passthrough PCI device
+ * @param {vmm_pci_config_t} config     Ops for accessing the passthrough config space
+ * @return                              `vmm_pci_entry_t` for passthrough device
+ */
 vmm_pci_entry_t vmm_pci_create_passthrough(vmm_pci_address_t addr, vmm_pci_config_t config);
 
-/* Bar read/write emulation, rest passed on */
+/***
+ * @function vmm_pci_create_bar_emulation(existing, num_bars, bars)
+ * Construct a pci entry that emulates configuration space bar read/write's. The rest of the configuration space is passed on
+ * @param {vmm_pci_entry_t} existing    Existing PCI entry to wrap over and emulate its bar accesses
+ * @param {int} num_bars                Number of emulated bars in PCI entry
+ * @param {vmm_pci_bar_t *} bars        Set of bars to emulate access to
+ * @return                              `vmm_pci_entry_t` for emulated bar device
+ */
 vmm_pci_entry_t vmm_pci_create_bar_emulation(vmm_pci_entry_t existing, int num_bars, vmm_pci_bar_t *bars);
 
-/* All bar read/writes passed through to emulated io(read/write) handlers */
+/***
+ * @function vmm_pci_create_passthrough_bar_emulation(existing, num_bars, bars)
+ * Construct a pci entry that passes through all bar read/writes through to emulated io(read/write) handlers. This is the
+ * inverse of `vmm_pci_create_bar_emulation`
+ * @param {vmm_pci_entry_t} existing    Existing PCI entry to wrap over and passthrough bar read/writes
+ * @param {int} num_bars                Number of emulated bars in PCI entry
+ * @param {vmm_pci_bar_t *} bars        Set of bars to passthrough access to
+ * @return                               `vmm_pci_entry_t` for passthrough bar device
+ */
 vmm_pci_entry_t vmm_pci_create_passthrough_bar_emulation(vmm_pci_entry_t existing, int num_bars, vmm_pci_bar_t *bars);
 
-/* Interrupt read/write emulation, rest passed on */
+/***
+ * @function vmm_pci_create_irq_emulation(existing, irq)
+ * Construct a pci entry the emulates configuration space interrupt read/write's. The rest of the configuration space is passed on
+ * @param {vmm_pci_entry_t} existing    Existing PCI entry to wrap over and emulate its IRQ accesses
+ * @param {int} irq                     IRQ line value in PCI entry
+ * @return                              `vmm_pci_entry_t` for emulated irq device
+ */
 vmm_pci_entry_t vmm_pci_create_irq_emulation(vmm_pci_entry_t existing, int irq);
 
-/* Capability space emulation. Takes list of addresses to use to form a capability
- * linked list, as well as a ranges of the capability space that should be
- * directly disallowed. Assumes a type 0 device.
+/***
+ * @function vmm_pci_create_cap_emulation(existing, num_caps, cap, num_ranges, range_starts, range_ends)
+ * Capability space emulation. Takes list of addresses to use to form a capability linked list, as well as a
+ * ranges of the capability space that should be directly disallowed. Assumes a type 0 device.
+ * @param {vmm_pci_entry_t} existing    Existing PCI entry to wrap over and emulated it capability space accesses
+ * @param {int} num_caps                Number of caps in capability space
+ * @param {uint8_t *} caps              Capability list
+ * @param {int} num_ranges              Number of disallowed/ignored capability ranges e.g. MSI capabilities
+ * @param {uint8_t *} range_starts      Array of starting indexes of ignored capability ranges
+ * @param {uint8_t *} range_end         Array of ending idexes of ignored capabilities range
+ * @return                              `vmm_pci_entry_t` with an emulated capability space
  */
 vmm_pci_entry_t vmm_pci_create_cap_emulation(vmm_pci_entry_t existing, int num_caps, uint8_t *caps, int num_ranges,
                                              uint8_t *range_starts, uint8_t *range_ends);
 
-/* Finds the MSI capabilities and uses vmm_pci_create_cap_emulation to remove them */
+/***
+ * Finds the MSI capabilities and uses vmm_pci_create_cap_emulation to register them as ignored
+ * @param {vmm_pci_entry_t} existing    Existing PCI entry to wrap over with ignored MSI capabilities
+ * @return                              `vmm_pci_entry_t` with an emulated capability space (ignoring MSI capabilties)
+ */
 vmm_pci_entry_t vmm_pci_no_msi_cap_emulation(vmm_pci_entry_t existing);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_con.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_con.h
index 4f972e4..8dcdb3c 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_con.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_con.h
@@ -12,36 +12,47 @@
 
 #pragma once
 
+/***
+ * @module virtio_con.h
+ * This interface provides the ability to initalise a VMM virtio console driver. This creating a virtio
+ * PCI device in the VM's virtual pci. This can subsequently be accessed through '/dev/hvc0' in the guest.
+ */
+
 #include <sel4vm/guest_vm.h>
 
 #include <sel4vmmplatsupport/ioports.h>
 #include <sel4vmmplatsupport/drivers/pci.h>
 #include <sel4vmmplatsupport/drivers/virtio_pci_emul.h>
 
-/* Virtio console driver interface */
+/***
+ * @struct virtio_con
+ * Virtio Console Driver Interface
+ * @param {unsigned int} iobase                             IO Port base for virtio con device
+ * @param {virtio_emul_t *} emul                            Virtio console emulation interface: VMM <-> Guest
+ * @param {struct console_passthrough} emul_driver_funcs    Virtio console emulation functions: VMM <-> Guest
+ * @param {ps_io_ops_t} ioops                               Platform support io ops datastructure
+ */
 typedef struct virtio_con {
-    /* IO Port base for virtio con device */
     unsigned int iobase;
-    /* Virtio console emulation interface: VMM <-> Guest */
     virtio_emul_t *emul;
-    /* Virtio console emulation functions: VMM <-> Guest */
     struct console_passthrough emul_driver_funcs;
     ps_io_ops_t ioops;
 } virtio_con_t;
 
-/**
+/***
+ * @function common_make_virtio_con(vm, pci, ioport, ioport_range, port_type, interrupt_pin, interrupt_lin, backend)
  * Initialise a new virtio_con device with Base Address Registers (BARs) starting at iobase and backend functions
  * specified by the console_passthrough struct.
- * @param vm vm handle
- * @param pci PCI library instance to register virtio con device
- * @param ioport IOPort library instance to register virtio con ioport
- * @param ioport_range BAR port for front end emulation
- * @param iotype type of ioport i.e. whether to alloc or use given range
- * @param interrupt_pin PCI interrupt pin e.g. INTA = 1, INTB = 2 ,...
- * @param interrupt_line PCI interrupt line for virtio con IRQS
- * @param backend function pointers to backend implementation. Can be initialised by
- *  virtio_con_default_backend for default methods.
- * @return pointer to an initialised virtio_con_t, NULL if error.
+ * @param {vm_t *} vm                               Handle to the VM
+ * @param {vmm_pci_space_t *} pci                   PCI library instance to register virtio con device
+ * @param {vmm_io_port_list_t *} ioport             IOPort library instance to register virtio con ioport
+ * @param {ioport_range_t} ioport_range             BAR port for front end emulation
+ * @param {ioport_type_t} iotype                    Type of ioport i.e. whether to alloc or use given range
+ * @param {unsigned int} interrupt_pin              PCI interrupt pin e.g. INTA = 1, INTB = 2 ,...
+ * @param {unsigned int} interrupt_line             PCI interrupt line for virtio con IRQS
+ * @param {struct console_passthrough} backend      Function pointers to backend implementation. Can be initialised by
+ *                                                  virtio_con_default_backend for default methods.
+ * @return                                          Pointer to an initialised virtio_con_t, NULL if error.
  */
 virtio_con_t *common_make_virtio_con(vm_t *vm,
                                      vmm_pci_space_t *pci,
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_net.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_net.h
index c6a6831..2aa961a 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_net.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/drivers/virtio_net.h
@@ -12,48 +12,59 @@
 
 #pragma once
 
+/***
+ * @module virtio_net.h
+ * This interface provides the ability to initalise a VMM virtio net driver. This creating a virtio
+ * PCI device in the VM's virtual pci. This can subsequently be accessed as an ethernet interface in the
+ * guest.
+ */
+
 #include <sel4vm/guest_vm.h>
 
 #include <sel4vmmplatsupport/ioports.h>
 #include <sel4vmmplatsupport/drivers/pci.h>
 #include <sel4vmmplatsupport/drivers/virtio_pci_emul.h>
 
-/* Virtio net driver interface */
+/***
+ * @struct virtio_net
+ * Virtio Net Driver Interface
+ * @param {unsigned int} iobase                         IO Port base for Virtio Net device
+ * @param {virtio_emul_t *} emul                        Virtio Ethernet emulation interface: VMM <-> Guest
+ * @param {struct eth_driver *} emul_driver             Backend Ethernet driver interface: VMM <-> Ethernet driver
+ * @param {struct raw_iface_funcs} emul_driver_funcs    Virtio Ethernet emulation functions: VMM <-> Guest
+ * @param {ps_io_ops_t} ioops                           Platform support ioops for dma management
+ */
 typedef struct virtio_net {
-    /* IO Port base for Virtio net device */
     unsigned int iobase;
-    /* Virtio Ethernet emulation interface: VMM <-> Guest */
     virtio_emul_t *emul;
-    /* Backend  Ethernet driver interface: VMM <-> Ethernet driver */
     struct eth_driver *emul_driver;
-    /* Virtio Ethernet emulation functions: VMM <-> Guest */
     struct raw_iface_funcs emul_driver_funcs;
-    /* ioops for dma management */
     ps_io_ops_t ioops;
 } virtio_net_t;
 
-/**
+/***
+ * @function common_make_virtio_net(vm, pci, ioport, ioport_range, port_type, interrupt_pin, interrupt_line, backend, emulate_bar_access)
  * Initialise a new virtio_net device with Base Address Registers (BARs) starting at iobase and backend functions
- *
  * specified by the raw_iface_funcs struct.
- * @param vm vm handle
- * @param pci PCI library instance to register virtio net device
- * @param ioport IOPort library instance to register virtio net ioport
- * @param ioport_range BAR port for front end emulation
- * @param iotype type of ioport i.e. whether to alloc or use given range
- * @param interrupt_pin PCI interrupt pin e.g. INTA = 1, INTB = 2 ,...
- * @param interrupt_line PCI interrupt line for virtio net IRQS
- * @param backend function pointers to backend implementation. Can be initialised by
- *  virtio_net_default_backend for default methods.
- * @param emulate_bar Emulate read and writes accesses to the PCI device Base Address Registers.
- * @return pointer to an initialised virtio_net_t, NULL if error.
+ * @param {vm_t *} vm                       A handle to the VM
+ * @param {vmm_pci_space_t *} pci           PCI library instance to register virtio net device
+ * @param {vmm_io_port_list_t *} ioport     IOPort library instance to register virtio net ioport
+ * @param {ioport_range_t} ioport_range     BAR port for front end emulation
+ * @param {ioport_type_t} port_type         Type of ioport i.e. whether to alloc or use given range
+ * @param {unsigned int} interrupt_pin      PCI interrupt pin e.g. INTA = 1, INTB = 2 ,...
+ * @param {unsigned int} interrupt_line     PCI interrupt line for virtio net IRQS
+ * @param {struct raw_iface_funcs} backend  Function pointers to backend implementation. Can be initialised by
+ *                                          virtio_net_default_backend for default methods.
+ * @param {bool} emulate_bar                Emulate read and writes accesses to the PCI device Base Address Registers.
+ * @return                                  Pointer to an initialised virtio_net_t, NULL if error.
  */
 virtio_net_t *common_make_virtio_net(vm_t *vm, vmm_pci_space_t *pci, vmm_io_port_list_t *ioport,
                                      ioport_range_t ioport_range, ioport_type_t port_type, unsigned int interrupt_pin, unsigned int interrupt_line,
                                      struct raw_iface_funcs backend, bool emulate_bar_access);
 
-/**
-* @return a struct with a default virtio_net backend. It is the responsibility of the caller to
-*  update these function pointers with its own custom backend.
-*/
+/***
+ * @function virtio_net_default_backend()
+ * @return          A struct with a default virtio_net backend. It is the responsibility of the caller to
+ *                  update these function pointers with its own custom backend.
+ */
 struct raw_iface_funcs virtio_net_default_backend(void);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_image.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_image.h
index 20e057f..33122ed 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_image.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_image.h
@@ -12,46 +12,63 @@
 
 #pragma once
 
+/***
+ * @module guest_image.h
+ * The guest image interface provides general utilites to load guest vm images (e.g. kernel, initrd, modules).
+ * This interface probably stops being relevant/useful after we start running a VM instance.
+ */
+
 #include <sel4vm/guest_vm.h>
 #include <sel4vmmplatsupport/arch/guest_image_arch.h>
 
 typedef struct guest_kernel_image_arch guest_kernel_image_arch_t;
 
+/***
+ * @struct guest_image
+ * General datastructure for managing a guest image
+ * @param {uintptr_t} load_paddr    Base address (in guest physical) where the image was loaded
+ * @param {size_t} alignment        Alignment we used when loading the image
+ * @param {size_t} size             Size of guest image
+ */
 typedef struct guest_image {
-    /* Base address (in guest physical) where the image was loaded */
     uintptr_t load_paddr;
-    /* Alignment we used when loading the image */
     size_t alignment;
-    /* Size of guest image */
     size_t size;
 } guest_image_t;
 
-/* Stores information about the guest kernel image we are loading. This information probably stops
- * being relevant / useful after we start running. */
+/***
+ * @struct guest_kernel_image
+ * Stores information about the guest kernel image we are loading.
+ * @param {guest_image_t} kernel_image                      Datastructure referring to guest kernel image
+ * @param {guest_kernel_image_arch_t} kernel_image_arch     Architecture specific information for loaded guest image
+ */
 typedef struct guest_kernel_image {
     guest_image_t kernel_image;
-    /* Architecture specific information for loaded guest image */
     guest_kernel_image_arch_t kernel_image_arch;
 } guest_kernel_image_t;
 
-/* Load guest kernel image
- * @param vm            Handle to the VM
- * @param kernel_name   Name of the kernel image
- * @param load_address  Address to load guest kernel image at
- * @param alignment     Alignment for loading kernel image
- * @param guest_kernel_image   Handle to information regarding the resulted loading of the guest kernel image
- * @return              0 on success, otherwise -1 on error
+/***
+ * @function vm_load_guest_kernel(vm, kernel_name, load_address, alignment, guest_kernel_image)
+ * Load guest kernel image
+ * @param {vm_t *} vm                                           Handle to the VM
+ * @param {const char *} kernel_name                            Name of the kernel image
+ * @param {uintptr_t} load_address                              Address to load guest kernel image at
+ * @param {size_t} alignment                                    Alignment for loading kernel image
+ * @param {guest_kernel_image_t *} guest_kernel_image           Handle to information regarding the resulted loading of the guest kernel image
+ * @return                                                      0 on success, otherwise -1 on error
  */
 int vm_load_guest_kernel(vm_t *vm, const char *kernel_name, uintptr_t load_address, size_t alignment,
                          guest_kernel_image_t *guest_kernel_image);
 
-/* Load guest kernel module e.g. initrd
- * @param vm            Handle to the VM
- * @param module_name   Name of the module image
- * @param load_address  Address to load guest kernel image at
- * @param alignment     Alignment for loading module image
- * @param guest_image   Handle to information regarding the resulted loading of the guest module image
- * @return              0 on success, otherwise -1 on error
+/***
+ * @function vm_load_guest_module(vm, module_name, load_address, alignment, guest_image)
+ * Load guest kernel module e.g. initrd
+ * @param {vm_t *} vm                           Handle to the VM
+ * @param {const char *} module_name            Name of the module image
+ * @param {uintptr_t} load_address              Address to load guest kernel image at
+ * @param {size_t} alignment                    Alignment for loading module image
+ * @param {guest_image_t *} guest_image         Handle to information regarding the resulted loading of the guest module image
+ * @return                                      0 on success, otherwise -1 on error
  */
 int vm_load_guest_module(vm_t *vm, const char *module_name, uintptr_t load_address, size_t alignment,
                          guest_image_t *guest_image);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_memory_util.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_memory_util.h
index d12c669..366494c 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_memory_util.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_memory_util.h
@@ -10,62 +10,73 @@
  * @TAG(DATA61_BSD)
  */
 
+/***
+ * @module guest_memory_util.h
+ * The guest memory util interface provides various utilities and helpers for using the libsel4vm guest memory
+ * interface. The methods in the interface cover common usage patterns when managing memory for a VM instance.
+ */
+
 #include <sel4vm/guest_vm.h>
 #include <sel4vm/guest_memory.h>
 
-/**
+/***
+ * @function create_allocated_reservation_frame(vm, addr, rights, alloc_fault_callback, alloc_fault_cookie)
  * Create and map a reservation for a vka allocated frame. The allocated frame is mapped in both the vm and vmm vspace
- * @param[in] vm                    A handle to the VM
- * @param[in] addr                  Address of emulated frame
- * @param[in] rights                Rights for mapping the allocated frame into the vm's vspace
- * @param[in] alloc_fault_callback   Fault callback for allocated frame
- * @param[in] alloc_fault_cookie     Cookie for fault callback
- * @return                          Address of allocated frame in vmm vspace
+ * @param {vm_t *} vm                                       A handle to the VM
+ * @param {uintptr_t} addr                                  Address of emulated frame
+ * @param {seL4_CapRights_t} rights                         Rights for mapping the allocated frame into the vm's vspace
+ * @param {memory_fault_callback_fn} alloc_fault_callback   Fault callback for allocated frame
+ * @param {void *} alloc_fault_cookie                       Cookie for fault callback
+ * @return                                                  Address of allocated frame in vmm vspace
  */
 void *create_allocated_reservation_frame(vm_t *vm, uintptr_t addr, seL4_CapRights_t rights,
                                          memory_fault_callback_fn alloc_fault_callback, void *alloc_fault_cookie);
-/**
+/***
+ * @function create_device_reservation_frame(vm, addr, rights, fault_callback, fault_cookie)
  * Create and map a reservation for a device frame. The device frame is mapped in both the vm and vmm vspace
- * @param[in] vm                    A handle to the VM
- * @param[in] addr                  Address of emulated frame
- * @param[in] rights                Rights for mapping the device frame into the vm's vspace
- * @param[in] fault_callback        Fault callback for the frame
- * @param[in] fault_cookie          Cookie for fault callback
- * @return                          Address of device frame in vmm vspace
+ * @param {vm_t *} vm                                       A handle to the VM
+ * @param {uintptr_t} addr                                  Address of emulated frame
+ * @param {seL4_CapRights_t} rights                         Rights for mapping the device frame into the vm's vspace
+ * @param {memory_fault_callback_fn} fault_callback         Fault callback for the frame
+ * @param {void *} fault_cookie                             Cookie for fault callback
+ * @return                                                  Address of device frame in vmm vspace
  */
 void *create_device_reservation_frame(vm_t *vm, uintptr_t addr, seL4_CapRights_t rights,
                                       memory_fault_callback_fn fault_callback, void *fault_cookie);
-
-/**
+/***
+ * @function map_ut_alloc_reservation_with_base_paddr(vm, paddr, reservation)
  * Map a guest reservation backed with untyped frames allocated from a base paddr
- * @param[in] vm                    A handle to the VM
- * @param[in] paddr                 Base paddr to allocate from
- * @param[in] reservation           Pointer to reservation object being mapped
- * @return                          -1 on failure otherwise 0 for success
+ * @param {vm_t *} vm                               A handle to the VM
+ * @param {uintptr_t} paddr                         Base paddr to allocate from
+ * @param {vm_memory_reservation_t *} reservation   Pointer to reservation object being mapped
+ * @return                                          -1 on failure otherwise 0 for success
  */
 int map_ut_alloc_reservation_with_base_paddr(vm_t *vm, uintptr_t paddr,
                                              vm_memory_reservation_t *reservation);
 
-/**
+/***
+ * @function map_ut_alloc_reservation(vm, reservation)
  * Map a guest reservation backed with untyped frames
- * @param[in] vm                    A handle to the VM
- * @param[in] reservation           Pointer to reservation object being mapped
- * @return                          -1 on failure otherwise 0 for success
+ * @param {vm_t *} vm                               A handle to the VM
+ * @param {vm_memory_reservation_t *} reservation   Pointer to reservation object being mapped
+ * @return                                          -1 on failure otherwise 0 for success
  */
 int map_ut_alloc_reservation(vm_t *vm, vm_memory_reservation_t *reservation);
 
-/**
+/***
+ * @function map_frame_alloc_reservation(vm, reservation)
  * Map a guest reservation backed with free vka frames
- * @param[in] vm                    A handle to the VM
- * @param[in] reservation           Pointer to reservation object being mapped
- * @return                          -1 on failure otherwise 0 for success
+ * @param {vm_t *} vm                                   A handle to the VM
+ * @param {vm_memory_reservation_t *} reservation       Pointer to reservation object being mapped
+ * @return                                              -1 on failure otherwise 0 for success
  */
 int map_frame_alloc_reservation(vm_t *vm, vm_memory_reservation_t *reservation);
 
-/**
+/***
+ * @function map_maybe_device_reservation(vm, reservation)
  * Map a guest reservation backed with device frames
- * @param[in] vm                    A handle to the VM
- * @param[in] reservation           Pointer to reservation object being mapped
- * @return                          -1 on failure otherwise 0 for success
+ * @param {vm_t *} vm                                   A handle to the VM
+ * @param {vm_memory_reservation_t *} reservation       Pointer to reservation object being mapped
+ * @return                                              -1 on failure otherwise 0 for success
  */
 int map_maybe_device_reservation(vm_t *vm, vm_memory_reservation_t *reservation);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_vcpu_util.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_vcpu_util.h
index 0074bcf..aa61be9 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_vcpu_util.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/guest_vcpu_util.h
@@ -12,7 +12,20 @@
 
 #pragma once
 
+/***
+ * @module guest_vcpu_util.h
+ * The guest vcpu util interface provides abstractions and helpers for managing libsel4vm vcpus.
+ */
+
 #include <sel4vm/guest_vm.h>
 #include <sel4vmmplatsupport/arch/guest_vcpu_util.h>
 
+/***
+ * @function create_vmm_plat_vcpu(vm, priority)
+ * Create a new platform vcpu. This is a wrapper around the libsel4vm function `vm_create_vcpu` however
+ * further intialises and configures the vcpu with platform specific attributes
+ * @param {vm_t *} vm       A handle to the VM
+ * @param {int} priority    Priority of the new vcpu thread
+ * @return                  NULL for error, otherwise pointer to created vm_vcpu_t object
+ */
 vm_vcpu_t *create_vmm_plat_vcpu(vm_t *vm, int priority);
diff --git a/libsel4vmmplatsupport/include/sel4vmmplatsupport/ioports.h b/libsel4vmmplatsupport/include/sel4vmmplatsupport/ioports.h
index 3149d7f..c7ab0a4 100644
--- a/libsel4vmmplatsupport/include/sel4vmmplatsupport/ioports.h
+++ b/libsel4vmmplatsupport/include/sel4vmmplatsupport/ioports.h
@@ -11,6 +11,14 @@
  */
 #pragma once
 
+/***
+ * @module ioports.h
+ * The ioports interface provides a useful abstraction for initialising, registering and handling ioport events
+ * for a guest VM instance. This is independent from the x86 libsel4vm ioports interface. This interface is intended
+ * to be more generic and architecture independent, useful for usecases that require ioports without architecture
+ * support (virtio PCI).
+ */
+
 #include <stdlib.h>
 #include <stdint.h>
 #include <stdbool.h>
@@ -23,26 +31,52 @@
     IOPORT_ADDR
 } ioport_type_t;
 
+/***
+ * @struct ioport_range
+ * Range of ioport handler
+ * @param {uint16_t} start  Start address of ioport range
+ * @param {uint16_t} end    End address of ioport range
+ * @param {uint16_t} size   Size of ioport range
+ */
 typedef struct ioport_range {
     uint16_t start;
     uint16_t end;
     uint16_t size;
 } ioport_range_t;
 
+/***
+ * @struct ioport_interface
+ * Datastructure used for ioport emulation, containing handlers for the ioport range
+ * @param {void *} cookie           User supplied cookie to pass onto handlers
+ * @param {ioport_in_fn} port_in    IO in operation handler
+ * @param {ioport_out_fn} port_out  IO out operation handler
+ * @param {const char *} desc       IOPort description, useful for debugging
+ */
 typedef struct ioport_interface {
     void *cookie;
-    /* ioport handler functions */
     ioport_in_fn port_in;
     ioport_out_fn port_out;
-    /* ioport description (for debugging) */
     const char *desc;
 } ioport_interface_t;
 
+/***
+ * @struct ioport_entry
+ * Datastructure used to present a registered ioport range
+ * @param {ioport_range_t} range            IO address range of ioport entry
+ * @param {ioport_interface_t} interface    Emulation interface for ioport range
+ */
 typedef struct ioport_entry {
     ioport_range_t range;
     ioport_interface_t interface;
 } ioport_entry_t;
 
+/***
+ * @struct vmm_io_list
+ * Parent datastructure used to maintain a list of registered ioports
+ * @param {int} num_ioports         Total number of registered ioports
+ * @param {ioport_entry_t **}       List of registered ioport objects
+ * @param {uint16_t} alloc_addr      Base ioport address we can safely bump allocate from, used when registering ioport handlers of type 'IOPORT_FREE'
+ */
 typedef struct vmm_io_list {
     int num_ioports;
     /* Sorted list of ioport functions */
@@ -50,26 +84,36 @@
     uint16_t alloc_addr;
 } vmm_io_port_list_t;
 
-/*
+/***
+ * @function vmm_io_port_init(io_list, ioport_alloc_addr)
  * Initialize the io port list manager.
- * @param io_list Pointer to io_port list handle. This will be allocated and initialised
- * @param ioport_alloc_addr Base ioport address we can safely bump allocate from (doesn't conflict with other ioports).
- *                          This is used when registering ioport handlers of type 'IOPORT_FREE'
- * @return 0 if handler, otherwise -1 for error
+ * @param {vmm_io_port_list_t **} io_list       Pointer to io_port list handle. This will be allocated and initialised
+ * @param {uint16_t} ioport_alloc_addr          Base ioport address we can safely bump allocate from (doesn't conflict with other ioports).
+ *                                              This is used when registering ioport handlers of type 'IOPORT_FREE'
+ * @return                                      0 for success, otherwise -1 for error
  */
 int vmm_io_port_init(vmm_io_port_list_t **io_list, uint16_t ioport_alloc_addr);
 
-/* Add an io port range for emulation */
+/***
+ * @function vmm_io_port_add_handler(io_list, ioport_range, ioport_interface, port_type)
+ * Add an io port range for emulation
+ * @param {vmm_io_port_list_t *} io_list            Handle to ioport list. This is where the new ioport handler will be appended to
+ * @param {ioport_range_t} ioport_range             Range the ioport handler will emulate
+ * @param {ioport_interface_t} ioport_interface     IOPort emulation interface
+ * @param {ioport_type_t} port_type                 The type of ioport being registered - IOPORT_FREE, IOPORT_ADDR
+ * @return                                          NULL for error, otherwise pointer to newly created ioport entry
+ */
 ioport_entry_t *vmm_io_port_add_handler(vmm_io_port_list_t *io_list, ioport_range_t ioport_range,
                                         ioport_interface_t ioport_interface, ioport_type_t port_type);
 
-/*
+/***
+ * @function emulate_io_handler(io_port, port_no, is_in, size, data)
  * From a set of registered ioports, emulate an io instruction given a current ioport access.
- * @param io_port List of registered ioports with in/out handlers
- * @param port_no ioport address being accessed
- * @param is_in true if we are performing an io in operation, otherwise false
- * @param size size of io access
- * @param data pointer with the data being written if io-out op, otherwise will be populated with data from an io-in op
- * @return 0 if handled, 1 if unhandled, otherwise -1 for error
+ * @param {vmm_io_port_list_t *} io_port        List of registered ioports with in/out handlers
+ * @param {unsigned int} port_no                IOPort address being accessed
+ * @param {bool} is_in                          True if we are performing an io in operation, otherwise False
+ * @param {size_t} size                         Size of io access
+ * @param {unsigned int *} data                 Pointer with the data being written if io-out op, otherwise will be populated with data from an io-in op
+ * @return                                      0 if handled, 1 if unhandled, otherwise -1 for error
  */
 int emulate_io_handler(vmm_io_port_list_t *io_port, unsigned int port_no, bool is_in, size_t size, unsigned int *data);