libsel4vm: Update documentation

This commit refreshes the interface documentation in libsel4vm.
This commit patches in missing documentation and additionally
ensures all interface documentation conforms to Doxygen style
comments.
diff --git a/libsel4vm/arch_include/arm/sel4vm/arch/guest_arm_context.h b/libsel4vm/arch_include/arm/sel4vm/arch/guest_arm_context.h
index 068d15f..7681548 100644
--- a/libsel4vm/arch_include/arm/sel4vm/arch/guest_arm_context.h
+++ b/libsel4vm/arch_include/arm/sel4vm/arch/guest_arm_context.h
@@ -15,58 +15,69 @@
 #include <sel4/sel4.h>
 #include <sel4vm/guest_vm.h>
 
-/* VCPU Thread Context Getters and Setters */
+/***
+ * @module guest_arm_context.h
+ * The libsel4vm ARM context interface provides a set of useful getters and setters on ARM vcpu thread contexts.
+ * This interface is commonly leveraged by VMM's to initialise a vcpu state, process a vcpu fault and
+ * accordingly update its state.
+ */
 
-/**
+/***
+ * @function vm_set_thread_context(vcpu, context)
  * Set a VCPU's thread registers given a TCB user context
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] context   seL4_UserContext applied to VCPU's TCB
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu            Handle to the vcpu
+ * @param {seL4_UserContext} context    seL4_UserContext applied to VCPU's TCB
+ * @return                              0 on success, otherwise -1 for error
  */
 int vm_set_thread_context(vm_vcpu_t *vcpu, seL4_UserContext context);
 
-/**
+/***
+ * @function vm_set_thread_context_reg(vcpu, reg, value)
  * Set a single VCPU's TCB register
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       Index offset of register in seL4_UserContext e.g pc (seL4_UserContext.pc) => 0
- * @param[in] value     Value to set TCB register with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu        Handle to the vcpu
+ * @param {unsigned int} reg        Index offset of register in seL4_UserContext e.g pc (seL4_UserContext.pc) => 0
+ * @param {uintptr_t} value         Value to set TCB register with
+ * @return                          0 on success, otherwise -1 for error
  */
 int vm_set_thread_context_reg(vm_vcpu_t *vcpu, unsigned int reg, uintptr_t value);
 
-/**
+/***
+ * @function vm_get_thread_context(vcpu, context)
  * Get a VCPU's TCB user context
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] context   Pointer to user supplied seL4_UserContext to populate with VCPU's TCB user context
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t} vcpu              Handle to the vcpu
+ * @param {seL4_UserContext} context    Pointer to user supplied seL4_UserContext to populate with VCPU's TCB user context
+ * @return                              0 on success, otherwise -1 for error
  */
 int vm_get_thread_context(vm_vcpu_t *vcpu, seL4_UserContext *context);
 
-/**
+/***
+ * @function vm_get_thread_context_reg(vcpu, reg, value)
  * Get a single VCPU's TCB register
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       Index offset of register in seL4_UserContext e.g pc (seL4_UserContext.pc) => 0
- * @param[in] value     Pointer to user supplied variable to populate TCB register value with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu        Handle to the vcpu
+ * @param {unsigned int} reg        Index offset of register in seL4_UserContext e.g pc (seL4_UserContext.pc) => 0
+ * @param {uintptr_t *} value       Pointer to user supplied variable to populate TCB register value with
+ * @return                          0 on success, otherwise -1 for error
  */
 int vm_get_thread_context_reg(vm_vcpu_t *vcpu, unsigned int reg, uintptr_t *value);
 
 /* ARM VCPU Register Getters and Setters */
 
-/**
+/***
+ * @function vm_set_arm_vcpu_reg(vcpu, reg, value)
  * Set an ARM VCPU register
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       VCPU Register field defined in seL4_VCPUReg
- * @param[in] value     Value to set VCPU register with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu        Handle to the vcpu
+ * @param {seL4_Word} reg           VCPU Register field defined in seL4_VCPUReg
+ * @param {uintptr_t *} value       Value to set VCPU register with
+ * @return                          0 on success, otherwise -1 for error
  */
 int vm_set_arm_vcpu_reg(vm_vcpu_t *vcpu, seL4_Word reg, uintptr_t value);
 
-/**
+/***
+ * @function vm_get_arm_vcpu_reg(vcpu, reg, value)
  * Get an ARM VCPU register
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       VCPU Register field defined in seL4_VCPUReg
- * @param[in] value     Pointer to user supplied variable to populate VCPU register value with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu    Handle to the vcpu
+ * @param {seL4_Word} reg       VCPU Register field defined in seL4_VCPUReg
+ * @param {uintptr_t *} value   Pointer to user supplied variable to populate VCPU register value with
+ * @return                      0 on success, otherwise -1 for error
  */
 int vm_get_arm_vcpu_reg(vm_vcpu_t *vcpu, seL4_Word reg, uintptr_t *value);
diff --git a/libsel4vm/arch_include/arm/sel4vm/arch/guest_memory_arch.h b/libsel4vm/arch_include/arm/sel4vm/arch/guest_memory_arch.h
index e5e00cc..de1db0e 100644
--- a/libsel4vm/arch_include/arm/sel4vm/arch/guest_memory_arch.h
+++ b/libsel4vm/arch_include/arm/sel4vm/arch/guest_memory_arch.h
@@ -14,4 +14,11 @@
 
 typedef struct vm vm_t;
 
+/**
+ * Convert an intermediate physical address belonging to a guest VM to a physical address
+ * @param[in] vm            A handle to the vm
+ * @param[in] ipa_base      The intermediate physical address
+ * @param[in] size          Size of the memory region
+ * @return                  Physical address value
+ */
 uintptr_t vm_arm_ipa_to_pa(vm_t *vm, uintptr_t ipa_base, size_t size);
diff --git a/libsel4vm/arch_include/arm/sel4vm/arch/guest_vm_arch.h b/libsel4vm/arch_include/arm/sel4vm/arch/guest_vm_arch.h
index 6295b08..2d05d52 100644
--- a/libsel4vm/arch_include/arm/sel4vm/arch/guest_vm_arch.h
+++ b/libsel4vm/arch_include/arm/sel4vm/arch/guest_vm_arch.h
@@ -12,6 +12,12 @@
 
 #pragma once
 
+/***
+ * @module guest_vm_arch.h
+ * The guest arm vm interface is central to using libsel4vm on an ARM platform, providing definitions of the arm guest vm
+ * datastructures and primitives to configure the VM instance.
+ */
+
 #include <sel4vm/guest_vm.h>
 
 typedef struct fault fault_t;
@@ -25,11 +31,26 @@
 
 struct vm_arch {};
 
+/***
+ * @struct vm_vcpu_arch
+ * Structure representing ARM specific vcpu properties
+ * @param {fault_t *} fault                                             Current VCPU fault
+ * @param {unhandled_vcpu_fault_callback_fn} unhandled_vcpu_callback    A callback for processing unhandled vcpu faults
+ * @param {void *} unhandled_vcpu_callback_cookie                       A cookie to supply to the vcpu fault handler
+ */
 struct vm_vcpu_arch {
     fault_t *fault;
     unhandled_vcpu_fault_callback_fn unhandled_vcpu_callback;
     void *unhandled_vcpu_callback_cookie;
 };
 
+/***
+ * @function vm_register_unhandled_vcpu_fault_callback(vcpu, vcpu_fault_callback, cookie)
+ * Register a callback for processing unhandled vcpu faults
+ * @param {vm_vcpu_t *} vcpu                    A handle to the VCPU
+ * @param {unhandled_vcpu_fault_callback_fn}    A user supplied callback to process unhandled vcpu faults
+ * @param {void *}                              A cookie to supply to the vcpu fault handler
+ * @return                                      0 on success, -1 on error
+ */
 int vm_register_unhandled_vcpu_fault_callback(vm_vcpu_t *vcpu, unhandled_vcpu_fault_callback_fn vcpu_fault_callback,
                                               void *cookie);
diff --git a/libsel4vm/arch_include/x86/sel4vm/arch/guest_vm_arch.h b/libsel4vm/arch_include/x86/sel4vm/arch/guest_vm_arch.h
index 2d437e7..20d66a9 100644
--- a/libsel4vm/arch_include/x86/sel4vm/arch/guest_vm_arch.h
+++ b/libsel4vm/arch_include/x86/sel4vm/arch/guest_vm_arch.h
@@ -12,6 +12,12 @@
 
 #pragma once
 
+/***
+ * @module guest_vm_arch.h
+ * The guest x86 vm interface is central to using libsel4vm on an x86 platform, providing definitions of the x86 guest vm
+ * datastructures and primitives to configure the VM instance.
+ */
+
 #include <sel4/sel4.h>
 
 #include <sel4vm/arch/vmexit_reasons.h>
@@ -35,24 +41,36 @@
     vmcall_handler func;
 } vmcall_handler_t;
 
+/***
+ * @struct vm_vcpu
+ * Structure representing x86 specific vm properties
+ * @param {vmexit_handler_ptr} vmexit_handler                           Set of exit handler hooks
+ * @param {vmcall_handler_t *} vmcall_handlers                          Set of registered vmcall handlers
+ * @param {unsigned int} vmcall_num_handler                             Total number of registered vmcall handlers
+ * @param {uintptr_t} guest_pd                                          Guest physical address of where we built the vm's page directory
+ * @param {unhandled_ioport_callback_fn} unhandled_ioport_callback      A callback for processing unhandled ioport faults
+ * @param {void *} unhandled_ioport_callback_cookie                     A cookie to supply to the ioport callback
+ * @param {vm_io_port_list_t} ioport_list                               List of registered ioport handlers
+ * @param {i8259_t *} i8259_gs                                          PIC machine state
+ */
 struct vm_arch {
-    /* Exit handler hooks */
     vmexit_handler_ptr vmexit_handlers[VM_EXIT_REASON_NUM];
-    /* VM Call handlers */
     vmcall_handler_t *vmcall_handlers;
     unsigned int vmcall_num_handlers;
-    /* Guest physical address of where we built the vm's page directory */
     uintptr_t guest_pd;
     unhandled_ioport_callback_fn unhandled_ioport_callback;
     void *unhandled_ioport_callback_cookie;
     vm_io_port_list_t ioport_list;
-    /* PIC machine state */
     i8259_t *i8259_gs;
 };
 
+/***
+ * @struct vm_vcpu_arch
+ * Structure representing x86 specific vcpu properties
+ * @param {guest_state_t *} guest_state         Current VCPU State
+ * @param {vm_lapic_t *} lapic                  VM local apic
+ */
 struct vm_vcpu_arch {
-    /* Records vcpu context */
     guest_state_t *guest_state;
-    /* VM local apic */
     vm_lapic_t *lapic;
 };
diff --git a/libsel4vm/arch_include/x86/sel4vm/arch/guest_x86_context.h b/libsel4vm/arch_include/x86/sel4vm/arch/guest_x86_context.h
index 02142c0..8c76d90 100644
--- a/libsel4vm/arch_include/x86/sel4vm/arch/guest_x86_context.h
+++ b/libsel4vm/arch_include/x86/sel4vm/arch/guest_x86_context.h
@@ -12,6 +12,13 @@
 
 #pragma once
 
+/***
+ * @module guest_x86_context.h
+ * The libsel4vm x86 context interface provides a set of useful getters and setters on x86 vcpu thread contexts.
+ * This interface is commonly leveraged by VMM's to initialise a vcpu state, process a vcpu fault and
+ * accordingly update its state.
+ */
+
 #include <sel4/sel4.h>
 #include <sel4vm/guest_vm.h>
 
@@ -25,58 +32,62 @@
     VCPU_CONTEXT_EBP
 } vcpu_context_reg_t;
 
-/* VCPU Thread Context Getters and Setters */
-
-/**
+/***
+ * @function vm_set_thread_context(vcpu, context)
  * Set a VCPU's thread registers given a seL4_VCPUContext
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] context   seL4_VCPUContext applied to VCPU Registers
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu            Handle to the vcpu
+ * @param {seL4_VCPUContext} context    seL4_VCPUContext applied to VCPU Registers
+ * @return                              0 on success, otherwise -1 for error
  */
 int vm_set_thread_context(vm_vcpu_t *vcpu, seL4_VCPUContext context);
 
-/**
+/***
+ * @function vm_set_thread_context_reg(vcpu, reg, value)
  * Set a single VCPU's thread register in a seL4_VCPUContext
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       Register enumerated by vcpu_context_reg
- * @param[in] value     Value to set register with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu            Handle to the vcpu
+ * @param {vcpu_context_reg_t} reg      Register enumerated by vcpu_context_reg
+ * @param {uint32_t} value              Value to set register with
+ * @return                              0 on success, otherwise -1 for error
  */
 int vm_set_thread_context_reg(vm_vcpu_t *vcpu, vcpu_context_reg_t reg, uint32_t value);
 
-/**
+/***
+ * @function vm_get_thread_context(vcpu, context)
  * Get a VCPU's thread context
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] context   Pointer to user supplied seL4_VCPUContext to populate with VCPU's current context
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu                Handle to the vcpu
+ * @param {seL4_VCPUContext *} context      Pointer to user supplied seL4_VCPUContext to populate with VCPU's current context
+ * @return                                  0 on success, otherwise -1 for error
  */
 int vm_get_thread_context(vm_vcpu_t *vcpu, seL4_VCPUContext *context);
 
-/**
+/***
+ * @function vm_get_thread_context_reg(vcpu, reg, value)
  * Get a single VCPU's thread register
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       Register enumerated by vcpu_context_reg
- * @param[in] value     Pointer to user supplied variable to populate register value with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu            Handle to the vcpu
+ * @param {vcpu_context_reg_t} reg      Register enumerated by vcpu_context_reg
+ * @param {uint32_t *} value            Pointer to user supplied variable to populate register value with
+ * @return                              0 on success, otherwise -1 for error
  */
 int vm_get_thread_context_reg(vm_vcpu_t *vcpu, vcpu_context_reg_t reg, uint32_t *value);
 
 /* VMCS Getters and Setters */
 
-/**
+/***
+ * @function vm_set_vmcs_field(vcpu, field, value)
  * Set a VMCS field
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       VMCS field
- * @param[in] value     Value to set VMCS field with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu        Handle to the vcpu
+ * @param {seL4_Word} reg           VMCS field
+ * @param {uint32_t} value          Value to set VMCS field with
+ * @return                          0 on success, otherwise -1 for error
  */
 int vm_set_vmcs_field(vm_vcpu_t *vcpu, seL4_Word field, uint32_t value);
 
-/**
+/***
+ * @function vm_get_vmcs_field(vcpu, field, value)
  * Get a VMCS register
- * @param[in] vcpu      Handle to the vcpu
- * @param[in] reg       VMCS fiedl
- * @param[in] value     Pointer to user supplied variable to populate VMCS field value with
- * @return              0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu        Handle to the vcpu
+ * @param {seL4_Word} reg           VMCS field
+ * @param {uint32_t *} value        Pointer to user supplied variable to populate VMCS field value with
+ * @return                          0 on success, otherwise -1 for error
  */
 int vm_get_vmcs_field(vm_vcpu_t *vcpu, seL4_Word field, uint32_t *value);
diff --git a/libsel4vm/arch_include/x86/sel4vm/arch/ioports.h b/libsel4vm/arch_include/x86/sel4vm/arch/ioports.h
index 9e27acb..8b4df57 100644
--- a/libsel4vm/arch_include/x86/sel4vm/arch/ioports.h
+++ b/libsel4vm/arch_include/x86/sel4vm/arch/ioports.h
@@ -12,6 +12,12 @@
 
 #pragma once
 
+/***
+ * @module ioports.h
+ * The x86 ioports interface provides a useful abstraction for initialising, registering and handling ioport events
+ * for a guest VM instance. IOPort faults are directed through this interface.
+ */
+
 #include <stdint.h>
 
 #include <sel4/sel4.h>
@@ -26,11 +32,44 @@
     IO_FAULT_ERROR
 } ioport_fault_result_t;
 
+/**
+ * Type signature of ioport in handler function.
+ * @param {vm_vcpu_t *} vcpu        A handle to the VCPU handling the ioport in operation
+ * @param {void *} cookie           A cookie to supply to the handler
+ * @param {unsigned int} port_no    Base port address being accessed
+ * @param {unsigned int} size       Size of ioport access
+ * @param {unsigned int} result     Pointer referencing the resulting value of the io operation. The handler is expected to populate
+ *                                  the variable with the value being read
+ * @return                          IOPort fault handling status code: IO_FAULT_HANDLED, IO_FAULT_UNHANDLED, IO_FAULT_ERROR
+ */
 typedef ioport_fault_result_t (*vm_ioport_in_fn)(vm_vcpu_t *vcpu, void *cookie, unsigned int port_no, unsigned int size,
                                                  unsigned int *result);
+
+/**
+ * Type signature of ioport out handler function.
+ * @param {vm_vcpu_t *} vcpu        A handle to the VCPU handling the ioport in operation
+ * @param {void *} cookie           A cookie to supply to the handler
+ * @param {unsigned int} port_no    Base port address being accessed
+ * @param {unsigned int} size       Size of ioport access
+ * @param {unsigned int} value      Value being written in ioport out operation
+ * @return                          IOPort fault handling status code: IO_FAULT_HANDLED, IO_FAULT_UNHANDLED, IO_FAULT_ERROR
+ */
 typedef ioport_fault_result_t (*vm_ioport_out_fn)(vm_vcpu_t *vcpu, void *cookie, unsigned int port_no,
                                                   unsigned int size,
                                                   unsigned int value);
+
+/**
+ * Type signature of unhandled ioport fault function, invoked when a ioport fault is unable to be handled
+ * @param {vm_vcpu_t *} vcpu            A handle to the VCPU object invoking unhandled ioport operation
+ * @param {unsigned int} port_no        Base port address being accessed
+ * @param {bool} is_in                  True if it is an ioport in access. False if it is an ioport out access.
+ * @param {unsigned int *} result       Pointer referencing the resulting value of the io operation. If it is an ioport in operation,
+ *                                      the handler is expected to populate the variable with the value being read. Otherwise if it
+ *                                      is an ioport out operation, then the derefenced value is the value being written.
+ * @param {size_t} size                 Size of ioport fault
+ * @param {void *} cookie               User cookie to pass onto callback
+ * @return                              Fault handling status code: HANDLED, UNHANDLED, RESTART, ERROR
+ */
 typedef ioport_fault_result_t (*unhandled_ioport_callback_fn)(vm_vcpu_t *vcpu, unsigned int port_no, bool is_in,
                                                               unsigned int *value,
                                                               size_t size, void *cookie);
@@ -60,12 +99,34 @@
     vm_ioport_entry_t *ioports;
 } vm_io_port_list_t;
 
-/* Add an io port range for emulation */
+/***
+ * @function vm_io_port_add_handler(vm, ioport_range, ioport_interface)
+ * Add an io port range for emulation
+ * @param {vm_t *} vm                               A handle to the VM
+ * @param {vm_ioport_range_t} ioport_range          Range of ioport being emulated with the given handler
+ * @param {vm_ioport_interface_t} ioport_interface  Interface for ioport range, containing io_in and io_out handler functions
+ * @return                                          0 for success, -1 for error
+ */
 int vm_io_port_add_handler(vm_t *vm, vm_ioport_range_t ioport_range,
                            vm_ioport_interface_t ioport_interface);
 
-/* IOPort fault callback registration functions */
+/***
+ * @function vm_register_unhandled_ioport_callback(vm, ioport_callback, cookie)
+ * Register a callback for processing unhandled ioport faults (faults unknown to libsel4vm)
+ * @param {vm_t *} vm                                       A handle to the VM
+ * @param {unhandled_ioport_callback_fn} ioport_callback    A user supplied callback to process unhandled ioport faults
+ * @param {void *} cookie                                   A cookie to supply to the callback
+ * @return                                                  0 for success, -1 for error
+ */
 int vm_register_unhandled_ioport_callback(vm_t *vm, unhandled_ioport_callback_fn ioport_callback,
                                           void *cookie);
 
+/***
+ * @function vm_enable_passthrough_ioport(vcpu, port_start, port_end)
+ * Enable the passing-through of specific ioport ranges to the VM
+ * @param {vm_vcpu_t *} vcpu            A handle to the VCPU being given ioport passthrough access
+ * @param {uint16_t} port_start         Base address of ioport
+ * @param {uint16_t} port_end           End address of ioport
+ * @return                              0 for success, -1 for error
+ */
 int vm_enable_passthrough_ioport(vm_vcpu_t *vcpu, uint16_t port_start, uint16_t port_end);
diff --git a/libsel4vm/arch_include/x86/sel4vm/arch/vmcall.h b/libsel4vm/arch_include/x86/sel4vm/arch/vmcall.h
index c9a36d4..b1c08f2 100644
--- a/libsel4vm/arch_include/x86/sel4vm/arch/vmcall.h
+++ b/libsel4vm/arch_include/x86/sel4vm/arch/vmcall.h
@@ -12,10 +12,22 @@
 
 #pragma once
 
+/***
+ * @module vmcall.h
+ * The x86 vmcall interface provides methods for registering and managing vmcall handlers. These being used
+ * to process x86 guest hypercalls though the vmcall instruction.
+ */
+
 #include <sel4vm/guest_vm.h>
 
-/*
-    Simple functions for registering handlers,
-        calling a handler
-*/
+/***
+ * @function vm_reg_new_vmcall_handler(vm, func, token)
+ * Register a new vmcall handler. The being hypercalls invoked by the
+ * guest through the vmcall instruction.
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {vmcall_handler} func     A handler function for the given vmcall being registered
+ * @param {int} token               A token to associate with a vmcall handler.
+ *                                  This being matched with the value found in the vcpu EAX register on a vmcall exception
+ * @return                          0 on success, -1 on error
+ */
 int vm_reg_new_vmcall_handler(vm_t *vm, vmcall_handler func, int token);
diff --git a/libsel4vm/include/sel4vm/boot.h b/libsel4vm/include/sel4vm/boot.h
index 7fd4e31..820f5c2 100644
--- a/libsel4vm/include/sel4vm/boot.h
+++ b/libsel4vm/include/sel4vm/boot.h
@@ -18,19 +18,45 @@
 
 #include <sel4vm/guest_vm.h>
 
-/* ID of the boot vcpu in a VM */
+/***
+ * @module boot.h
+ * The libsel4vm boot interface provides us with base abstractions to create, initialise and configure VM and VCPU instances.
+ */
+
+/**
+ * ID of the boot vcpu in a VM
+ */
 #define BOOT_VCPU 0
 
-/* Initialise/Create VM */
+/***
+ * @function vm_init(vm, vka, host_simple, host_vspace, io_ops, host_endpoint, name)
+ * Initialise/Create VM
+ * @param {vm_t *} vm                   Handle to the VM being initialised
+ * @param {vka_t *} vka                 Initialised handle to virtual kernel allocator for seL4 kernel object allocation
+ * @param {simple_t *} host_simple      Initialised handle to hosts simple environment
+ * @param {vspace_t} host_vspace        Initialised handle to hosts vspace
+ * @param {ps_io_ops_t *} ps_io_ops     Initialised handle to platforms io ops
+ * @param {seL4_CPtr} host_enpoint      Host's endpoint. The library will wait and manage the endpoint when running a VM instance
+ * @param {const char *} name           String used to describe VM. Useful for debugging
+ * @return                              0 on success, otherwise -1 for error
+ */
 int vm_init(vm_t *vm, vka_t *vka, simple_t *host_simple, vspace_t host_vspace,
             ps_io_ops_t *io_ops, seL4_CPtr host_endpoint, const char *name);
 
-/* Create a VCPU for a given VM */
+/***
+ * @function vm_create_vcpu(vm, priority)
+ * Create a VCPU for a given VM
+ * @param {vm_t *} vm       A handle to VM being configured with a new vcpu
+ * @param {int} priority    The scheduling priority assigned to the VCPU thread
+ * @return                  NULL for error, otherwise pointer to created vm_vcpu_t object
+ */
 vm_vcpu_t *vm_create_vcpu(vm_t *vm, int priority);
 
-/* Assign a vcpu with logical target cpu to run on
- * @param[in] vcpu          A handle to the VCPU
- * @param[in] target        Logical target CPU ID
- * @return                  -1 for error, otherwise 0 for success
+/***
+ * @function vm_assign_vcpu_target(vcpu, target_cpu)
+ * Assign a vcpu with logical target cpu to run on
+ * @param {vm_vcpu_t *} vcpu    A handle to the VCPU
+ * @param {int} target          Logical target CPU ID
+ * @return                      -1 for error, otherwise 0 for success
  */
 int vm_assign_vcpu_target(vm_vcpu_t *vcpu, int target_cpu);
diff --git a/libsel4vm/include/sel4vm/guest_iospace.h b/libsel4vm/include/sel4vm/guest_iospace.h
index 407eca3..60b3383 100644
--- a/libsel4vm/include/sel4vm/guest_iospace.h
+++ b/libsel4vm/include/sel4vm/guest_iospace.h
@@ -17,4 +17,18 @@
 #include <vka/vka.h>
 #include <sel4vm/guest_vm.h>
 
+/***
+ * @module guest_iospace.h
+ * The libsel4vm iospace interface enables the registration and management of a guest VM's IO Space. This
+ * being used when supporting IOMMU (x86) and SMMU (ARM) VM features.
+ */
+
+/***
+ * @function vm_guest_add_iospace(vm, loader, iospace)
+ * Attach an additional IO space to the given VM
+ * @param {vm_t *} vm           A handle to the VM
+ * @param {vspace_t *} loader   Host loader vspace to create a new iospace
+ * @param {seL4_CPtr} iospace   Capability to iospace being added
+ * @return                      0 on success, otherwise -1 for error
+ */
 int vm_guest_add_iospace(vm_t *vm, vspace_t *loader, seL4_CPtr iospace);
diff --git a/libsel4vm/include/sel4vm/guest_irq_controller.h b/libsel4vm/include/sel4vm/guest_irq_controller.h
index be2df75..101e815 100644
--- a/libsel4vm/include/sel4vm/guest_irq_controller.h
+++ b/libsel4vm/include/sel4vm/guest_irq_controller.h
@@ -14,38 +14,51 @@
 
 #include <sel4vm/guest_vm.h>
 
-/* Callback for irq acknowledgement */
-typedef void (*irq_ack_fn_t)(vm_vcpu_t *vcpu, int irq, void *cookie);
+/***
+ * @module guest_irq_controller.h
+ * The libsel4vm IRQ controller interface provides a base abstraction around initialising a guest VM irq controller
+ * and methods for injecting IRQs into a running VM instance.
+ */
 
 /**
+ * Callback for irq acknowledgement
+ */
+typedef void (*irq_ack_fn_t)(vm_vcpu_t *vcpu, int irq, void *cookie);
+
+/***
+ * @function vm_inject_irq(vcpu, irq)
  * Inject an IRQ into a VM's interrupt controller
- * @param vcpu  Handle to the VCPU
- * @param irq   IRQ number to inject
- * @return      0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu    Handle to the VCPU
+ * @param {int} irq             IRQ number to inject
+ * @return                      0 on success, otherwise -1 for error
  */
 int vm_inject_irq(vm_vcpu_t *vcpu, int irq);
 
-/**
+/***
+ * @function vm_set_irq_level(vcpu, irq, irq_level)
  * Set level of IRQ number into a VM's interrupt controller
- * @param vcpu      Handle to the VCPU
- * @param irq       IRQ number to set level on
- * @param irq_level Value of IRQ level
- * @return          0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t} vcpu      Handle to the VCPU
+ * @param {int} irq             IRQ number to set level on
+ * @param {int} irq_level       Value of IRQ level
+ * @return                      0 on success, otherwise -1 for error
  */
 int vm_set_irq_level(vm_vcpu_t *vcpu, int irq, int irq_level);
 
-/**
+/***
+ * @function vm_register_irq(vcpu, irq, ack_fn, cookie)
  * Register irq with an acknowledgment function
- * @param vcpu      Handle to the VCPU
- * @param irq       IRQ number to register acknowledgement function on
- * @param ack_fn    IRQ acknowledgement function
- * @param cookie    Cookie to pass back with IRQ acknowledgement function
- * @return          0 on success, otherwise -1 for error
+ * @param {vm_vcpu_t *} vcpu        Handle to the VCPU
+ * @param {int} irq                 IRQ number to register acknowledgement function on
+ * @param {irq_ack_fn_t} ack_fn     IRQ acknowledgement function
+ * @param {void *} cookie           Cookie to pass back with IRQ acknowledgement function
+ * @return                          0 on success, otherwise -1 for error
  */
 int vm_register_irq(vm_vcpu_t *vcpu, int irq, irq_ack_fn_t ack_fn, void *cookie);
 
-/**
+/***
+ * @function vm_create_default_irq_controller(vm)
  * Install the default interrupt controller into the VM
- * @param vm    Handle to the VM
+ * @param {vm_t *} vm   Handle to the VM
+ * @return              0 on success, otherwise -1 for error
  */
 int vm_create_default_irq_controller(vm_t *vm);
diff --git a/libsel4vm/include/sel4vm/guest_memory.h b/libsel4vm/include/sel4vm/guest_memory.h
index 04c904e..8d1aa2a 100644
--- a/libsel4vm/include/sel4vm/guest_memory.h
+++ b/libsel4vm/include/sel4vm/guest_memory.h
@@ -17,96 +17,141 @@
 
 #include <sel4vm/arch/guest_memory_arch.h>
 
+/***
+ * @module guest_memory.h
+ * The libsel4vm memory interface provides useful abstractions to manage your guest VM's address space.
+ * This interface can be leveraged for uses such as mapping device memory into your VM instance
+ * or for creating emulated device regions binded with custom handlers/callbacks.
+ * The main mechanisms this interface provides involves reserving memory regions and using those reservations
+ * to either map memory into your guest VM's address space or emulate subsequent accesses. Reservations
+ * are created through either using `vm_reserve_memory_at` or `vm_reserve_anon_memory`.
+ * The user can then further back the reservation with seL4 frames by performing `vm_map_reservation`.
+ */
+
 typedef struct vm vm_t;
 typedef struct vm_vcpu vm_vcpu_t;
 
+/***
+ * @struct vm_frame_t
+ * Structure representing a mappable memory frame
+ * @param {seL4_CPtr} cptr              Capability to frame
+ * @param {seL4_CapRights_t} rights     Mapping rights of frame
+ * @param {uintptr_t} vaddr             Virtual address of which to map the frame into
+ * @param {size_t} size_bits            Size of frame in bits
+ */
 typedef struct vm_frame {
-    seL4_CPtr cptr;
-    seL4_CapRights_t rights;
-    uintptr_t vaddr;
-    size_t size_bits;
+    seL4_CPtr cptr; /** Capability to frame */
+    seL4_CapRights_t rights; /** Mapping rights of frame */
+    uintptr_t vaddr; /** Virtual address of which to map the frame into */
+    size_t size_bits; /** Size of frame in bits */
 } vm_frame_t;
 
+/**
+ * Enumeration of results that can be returned by a memory fault callback (type 'memory_fault_callback_fn')
+ */
 typedef enum memory_fault_result {
-    FAULT_HANDLED,
-    FAULT_UNHANDLED,
-    FAULT_RESTART,
-    FAULT_IGNORE,
-    FAULT_ERROR
+    FAULT_HANDLED, /** The memory fault was handled, advance execution */
+    FAULT_UNHANDLED, /** The memory fault was left unhandled */
+    FAULT_RESTART, /** The memory fault should be restarted, restart execution */
+    FAULT_IGNORE, /** Ignore the memory fault, advance execution */
+    FAULT_ERROR /** Handling the memory fault resulted in an error */
 } memory_fault_result_t;
 
+/**
+ * Type signature of memory fault handler/callback function, provided when creating a memory reservation
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {vm_vcpu_t} vcpu          A handle to the fault vcpu
+ * @param {uintptr_t} fault addr    Faulting address
+ * @param {size_t} fault_length     Length of faulted access
+ * @param {void *} cookie           User cookie to pass onto callback
+ * @return                          Fault handling status code: HANDLED, UNHANDLED, RESTART, ERROR
+ */
 typedef memory_fault_result_t (*memory_fault_callback_fn)(vm_t *vm, vm_vcpu_t *vcpu, uintptr_t fault_addr,
                                                           size_t fault_length,
                                                           void *cookie);
+/**
+ * Type signature of memory map iterator function, provided when mapping a memory reservation
+ * @param {uintptr_t} addr      Address being mapped
+ * @param {void *} cookie       User cookie to pass onto iterator
+ * @return                      vm_frame_t describing the memory frame that corresponds with the given address
+ */
 typedef vm_frame_t (*memory_map_iterator_fn)(uintptr_t addr, void *cookie);
 
 typedef struct vm_memory_reservation vm_memory_reservation_t;
 typedef struct vm_memory_reservation_cookie vm_memory_reservation_cookie_t;
 
-/**
+/***
+ * @function vm_reserve_memory_at(vm, addr, size, fault_callback, cookie)
  * Reserve a region of the VM's memory at a given base address
- * @param[in] vm                    A handle to the VM
- * @param[in] addr                  Base address of the memory region being reserved
- * @param[in] size                  Size of the memory region being reserved
- * @param[in] fault_callback        Callback function that will be invoked if memory region is faulted on
- * @param[in] cookie                User cookie to pass onto to callback
- * @return                          NULL on failure otherwise a pointer to a reservation object representing the reserved region
+ * @param {vm_t *} vm                                       A handle to the VM
+ * @param {uintptr} addr                                    Base address of the memory region being reserved
+ * @param {size_t} size                                     Size of the memory region being reserved
+ * @param {memory_fault_callback_fn} fault_callback         Callback function that will be invoked if memory region is faulted on
+ * @param {void *} cookie                                   User cookie to pass onto to callback
+ * @return                                                  NULL on failure otherwise a pointer to a reservation object representing the reserved region
  */
 vm_memory_reservation_t *vm_reserve_memory_at(vm_t *vm, uintptr_t addr, size_t size,
                                               memory_fault_callback_fn fault_callback, void *cookie);
 
-/**
+/***
+ * @function vm_reserve_anon_memory(vm, size, fault_callback, cookie, addr)
  * Reserve an anonymous region of the VM's memory. This uses memory previously made anonymous
  * through the `vm_memory_make_anon` function.
- * @param[in] vm                    A handle to the VM
- * @param[in] size                  Size of the anoymous emory region being reserved
- * @param[in] fault_callback        Callback function that will be invoked if memory region is faulted on
- * @param[in] cookie                User cookie to pass onto to callback
- * @param[in] addr                  Pointer that will be set with the base address of the reserved anonymous region
- * @return                          NULL on failure otherwise a pointer to a reservation object representing the reserved region
+ * @param {vm_t *} vm                                       A handle to the VM
+ * @param {size_t} size                                     Size of the anoymous emory region being reserved
+ * @param {memory_fault_callback_fn} fault_callback         Callback function that will be invoked if memory region is faulted on
+ * @param {void *} cookie                                   User cookie to pass onto to callback
+ * @param {uintptr_t *} addr                                Pointer that will be set with the base address of the reserved anonymous region
+ * @return                                                  NULL on failure otherwise a pointer to a reservation object representing the reserved region
  */
 vm_memory_reservation_t *vm_reserve_anon_memory(vm_t *vm, size_t size,
                                                 memory_fault_callback_fn fault_callback, void *cookie, uintptr_t *addr);
 
-/**
+/*** vm_memory_make_anon(vm, addr, size)
+ * @function
  * Create an anoymous region of the VM's memory. This claims a region of VM memory that can be used for the creation
  * of anonymous reservations (achieved by calling 'vm_reserve_anon_memory').
- * @param[in] vm                    A handle to the VM
- * @param[in] addr                  Base address of the memory region being made into an anoymous reservation
- * @param[in] size                  Size of the memory region being reserved
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {uintptr} addr            Base address of the memory region being made into an anoymous reservation
+ * @param {size_t} size             Size of the memory region being reserved
  * @return                          -1 on failure otherwise 0 for success
  */
 int vm_memory_make_anon(vm_t *vm, uintptr_t addr, size_t size);
 
-/**
+/***
+ * @function vm_free_reserved_memory(vm, reservation)
  * Free memory reservation from the VM
- * @param[in] vm                    A handle to the VM
- * @param[in] reservation           Pointer to the reservation being free'd
- * @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 the reservation being free'd
+ * @return                                              -1 on failure otherwise 0 for success
  */
 int vm_free_reserved_memory(vm_t *vm, vm_memory_reservation_t *reservation);
 
-/**
+/***
+ * @function vm_map_reservation(vm, reservation, map_iterator, cookie)
  * Map a reservation into the VM's virtual address space
- * @param[in] vm                    A handle to the VM
- * @param[in] reservation           Pointer to reservation object being mapped
- * @param[in] map_iterator          Iterator function that returns a cap to the memory region being mapped
- * @param[in] cookie                Cookie to pass onto map_iterator function
+ * @param {vm_t *} vm                                   A handle to the VM
+ * @param {vm_memory_reservation_t *} reservation       Pointer to reservation object being mapped
+ * @param {memory_map_iterator_fn} map_iterator         Iterator function that returns a cap to the memory region being mapped
+ * @param {void *} cookie                               Cookie to pass onto map_iterator function
+ * @return                                              -1 on failure otherwise 0 for success
  */
 int vm_map_reservation(vm_t *vm, vm_memory_reservation_t *reservation, memory_map_iterator_fn map_iterator,
                        void *cookie);
 
-/**
+/***
+ * @function vm_get_reservation_memory_region(reservation, addr, size)
  * Get the memory region information (address & size) from a given reservation
- * @param[in] reservation           Pointer to reservation object
- * @param[in] addr                  Pointer that will be set with the address of reservation
- * @param[in] size                  Pointer that will be set with the size of reservation
+ * @param {vm_memory_reservation_t *} reservation           Pointer to reservation object
+ * @param {uintptr_t *} addr                                Pointer that will be set with the address of reservation
+ * @param {size_t *} size                                   Pointer that will be set with the size of reservation
  */
 void vm_get_reservation_memory_region(vm_memory_reservation_t *reservation, uintptr_t *addr, size_t *size);
 
-/**
+/***
+ * @function vm_memory_init(vm)
  * Initialise a VM's memory management interface
- * @param[in] vm                    A handle to the VM
+ * @param {vm_t *} vm               A handle to the VM
  * @return                          -1 on failure otherwise 0 for success
 */
 int vm_memory_init(vm_t *vm);
diff --git a/libsel4vm/include/sel4vm/guest_memory_helpers.h b/libsel4vm/include/sel4vm/guest_memory_helpers.h
index a4f8c89..c36027d 100644
--- a/libsel4vm/include/sel4vm/guest_memory_helpers.h
+++ b/libsel4vm/include/sel4vm/guest_memory_helpers.h
@@ -15,9 +15,21 @@
 #include <sel4vm/guest_vm.h>
 #include <sel4vm/guest_memory.h>
 
-/**
+/***
+ * @module guest_memory_helpers.h
+ * The libsel4vm guest memory helpers interface provides simple utilities for using the guest memory interface.
+ */
+
+/***
+ * @function default_error_fault_callback(vm, vcpu, fault_addr, fault_length, cookie)
  * Default fault callback that throws a fault error.
  * Useful to avoid having to re-define a fault callback on regions that should be mapped with all rights.
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {vm_vcpu_t *} vcpu        A handle to the fault vcpu
+ * @param {uintptr_t} fault addr    Faulting address
+ * @param {size_t} fault_length     Length of faulted access
+ * @param {void *} cookie           User cookie to pass onto callback
+ * @return                          Always returns FAULT_ERROR
  */
 memory_fault_result_t default_error_fault_callback(vm_t *vm, vm_vcpu_t *vcpu, uintptr_t fault_addr,
                                                    size_t fault_length, void *cookie);
diff --git a/libsel4vm/include/sel4vm/guest_ram.h b/libsel4vm/include/sel4vm/guest_ram.h
index f6bd419..f2a4c5f 100644
--- a/libsel4vm/include/sel4vm/guest_ram.h
+++ b/libsel4vm/include/sel4vm/guest_ram.h
@@ -14,67 +14,116 @@
 
 #include <sel4vm/guest_vm.h>
 
+/***
+ * @module guest_ram.h
+ * The libsel4vm RAM interface provides us with a set of methods to manage a guest VM's RAM. This involves functions
+ * to register, allocate and copy to and from RAM regions.
+ */
+
+/**
+ * Type signature of ram touch callback function, provided when invoking 'vm_ram_touch'
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {uintptr_t} guest_addr    Current guest physical address being accessed
+ * @param {void *} vmm_vaddr        Virtual address in hosts (vmm) vspace corresponding with the current 'guest_addr'
+ * @param {size_t} size             Size of region being currently accessed
+ * @param {size_t} offset           Current offset from the base guest physical address supplied to 'vm_ram_touch'
+ * @param {void *} cookie           User supplied cookie to pass onto callback
+ * @return                          0 on success, -1 on error
+ */
 typedef int (*ram_touch_callback_fn)(vm_t *vm, uintptr_t guest_addr, void *vmm_vaddr, size_t size, size_t offset,
                                      void *cookie);
+
+/***
+ * @function vm_guest_ram_read_callback(vm, guest_addr, vaddr, size, offset, buf)
+ * Common guest ram touch callback for reading from a guest address into a user supplied buffer
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {uintptr_t} guest_addr    Guest physical address to read from
+ * @param {void *} vmm_vaddr        Virtual address in hosts (vmm) vspace corresponding with the 'guest_addr'
+ * @param {size_t} size             Size of region being currently accessed
+ * @param {size_t} offset           Current offset from the base guest physical address supplied to 'vm_ram_touch'
+ * @param {void *} cookie           User supplied buffer to store read data into
+ * @return                          0 on success, -1 on error
+ */
 int vm_guest_ram_read_callback(vm_t *vm, uintptr_t guest_addr, void *vaddr, size_t size, size_t offset, void *buf);
+
+/***
+ * @function vm_guest_ram_write_callback(vm, guest_addr, vaddr, size, offset, buf)
+ * Common guest ram touch callback for writing a user supplied buffer into a guest address
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {uintptr_t} guest_addr    Guest physical address to write to
+ * @param {void *} vmm_vaddr        Virtual address in hosts (vmm) vspace corresponding with the 'guest_addr'
+ * @param {size_t} size             Size of region being currently accessed
+ * @param {size_t} offset           Current offset from the base guest physical address supplied to 'vm_ram_touch'
+ * @param {void *} cookie           User supplied buffer to write data from
+ * @return                          0 on success, -1 on error
+ */
 int vm_guest_ram_write_callback(vm_t *vm, uintptr_t guest_addr, void *vaddr, size_t size, size_t offset, void *buf);
 
-/* Touch a series of pages in the guest vm and invoke a callback for each page accessed
- * @param[in] vm        A handle to the VM
- * @param[in] addr      Address to access in the guest vm
- * @param[in] size      Size of memory region to access
- * @param[in] callback  Callback to invoke on each page access
- * @param[in] cookie    User data to pass onto callback
+/***
+ * @function vm_ram_touch(vm, addr, size, touch_callback, cookie)
+ * Touch a series of pages in the guest vm and invoke a callback for each page accessed
+ * @param {vm_t *} vm                       A handle to the VM
+ * @param {uintptr_t} addr                  Address to access in the guest vm
+ * @param {size_t} size                     Size of memory region to access
+ * @param {ram_touch_callback_fn} callback  Callback to invoke on each page access
+ * @param {void *} cookie                   User data to pass onto callback
+ * @return                                  0 on success, -1 on error
  */
 int vm_ram_touch(vm_t *vm, uintptr_t addr, size_t size, ram_touch_callback_fn touch_callback, void *cookie);
 
-/**
+/***
+ * @function vm_ram_find_largest_free_region(vm, addr, size)
  * Find the largest free ram region
- * @param[in] vm                A handle to the VM
- * @param[in] addr              Pointer to be set with largest region address
- * @param[in] size              Pointer to be set with largest region size
- * @return                     -1 on failure, otherwise 0 for success
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {uintptr_t *} addr        Pointer to be set with largest region address
+ * @param {size_t *} size           Pointer to be set with largest region size
+ * @return                          -1 on failure, otherwise 0 for success
  */
 int vm_ram_find_largest_free_region(vm_t *vm, uintptr_t *addr, size_t *size);
 
-/**
+/***
+ * @function vm_ram_register(vm, bytes)
  * Reserve a region of memory for RAM in the guest VM
- * @param[in] vm                A handle to the VM
- * @param[in] bytes             Size of RAM region to allocate
+ * @param {vm_t *} vm           A handle to the VM
+ * @param {size_t} bytes        Size of RAM region to allocate
  * @return                      Starting address of registered ram region
  */
 uintptr_t vm_ram_register(vm_t *vm, size_t bytes);
 
-/**
+/***
+ * @function vm_ram_register_at(vm, start, bytes, untyped)
  * Reserve a region of memory for RAM in the guest VM at a starting guest physical address
- * @param[in] vm            A handle to the VM that ram needs to be allocated for
- * @param[in] start         Starting guest physical address of the ram region being allocated
- * @param[in] size          The size of the RAM region to be allocated
- * @param[in] untyped       Allocate RAM frames such that it uses untyped memory
- * @return                  0 on success
+ * @param {vm_t *} vm           A handle to the VM that ram needs to be allocated for
+ * @param {uintptr_t} start     Starting guest physical address of the ram region being allocated
+ * @param {size_t} size         The size of the RAM region to be allocated
+ * @param {bool} untyped        Allocate RAM frames such that it uses untyped memory
+ * @return                      0 on success, -1 on error
  */
 int vm_ram_register_at(vm_t *vm, uintptr_t start, size_t bytes, bool untyped);
 
-/**
+/***
+ * @function vm_ram_mark_allocated(vm, start, bytes)
  * Mark a registered region of RAM as allocated
- * @param[in] vm                A handle to the VM
- * @param[in] start             Starting address of guest ram region
- * @param[in] bytes             Size of RAM region
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {uintptr_t} start         Starting address of guest ram region
+ * @param {size_t} bytes            Size of RAM region
  */
 void vm_ram_mark_allocated(vm_t *vm, uintptr_t start, size_t bytes);
 
-/**
+/***
+ * @function vm_ram_allocate(vm, bytes)
  * Allocate a region of registered ram
- * @param[in] vm                A handle to the VM
- * @param[in] bytes             Size of allocation
+ * @param {vm_t *} vm           A handle to the VM
+ * @param {size_t} bytes        Size of allocation
  * @return                      Starting address of allocated ram region
  */
 uintptr_t vm_ram_allocate(vm_t *vm, size_t bytes);
 
-/**
+/***
+ * @function vm_ram_free(vm, start, bytes)
  * Free a RAM a previously allocated RAM region
- * @param[in] vm        A handle to the VM that ram needs to be free'd for
- * @param[in] start     Starting guest physical address of the ram region being free'd
- * @param[in] size      The size of the RAM region to be free'd
+ * @param {vm_t *} vm           A handle to the VM that ram needs to be free'd for
+ * @param {uintptr_t} start     Starting guest physical address of the ram region being free'd
+ * @param {size_t} size         The size of the RAM region to be free'd
  */
 void vm_ram_free(vm_t *vm, uintptr_t start, size_t bytes);
diff --git a/libsel4vm/include/sel4vm/guest_vcpu_fault.h b/libsel4vm/include/sel4vm/guest_vcpu_fault.h
index 5ed737d..b670a79 100644
--- a/libsel4vm/include/sel4vm/guest_vcpu_fault.h
+++ b/libsel4vm/include/sel4vm/guest_vcpu_fault.h
@@ -17,72 +17,89 @@
 #include <sel4/sel4.h>
 #include <sel4vm/guest_vm.h>
 
-/*
+/***
+ * @module guest_vcpu_fault.h
+ * The libsel4vm VCPU fault interface provides a set of useful methods to query and configure vcpu objects that
+ * have faulted during execution. This interface is commonly leveraged by VMM's to process a vcpu fault and handle
+ * it accordingly.
+ */
+
+/***
+ * @function get_vcpu_fault_address(vcpu)
  * Get current fault address of vcpu
- * @param vcpu  Handle to vcpu
- * @return      Current fault address of vcpu
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @return                      Current fault address of vcpu
  */
 seL4_Word get_vcpu_fault_address(vm_vcpu_t *vcpu);
 
-/*
+/***
+ * @function get_vcpu_fault_ip(vcpu)
  * Get instruction pointer of current vcpu fault
- * @param vcpu  Handle to vcpu
- * @return      Intruction pointer of vcpu fault
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @return                      Intruction pointer of vcpu fault
  */
 seL4_Word get_vcpu_fault_ip(vm_vcpu_t *vcpu);
 
-/*
+/***
+ * @function get_vcpu_fault_data(vcpu)
  * Get the data of the current vcpu fault
- * @param vcpu  Handle to vcpu
- * @return      Data of vcpu fault
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @return                      Data of vcpu fault
  */
 seL4_Word get_vcpu_fault_data(vm_vcpu_t *vcpu);
 
-/*
+/***
+ * @function get_vcpu_fault_data_mask(vcpu)
  * Get data mask of the current vcpu fault
- * @param vcpu  Handle to vcpu
- * @return      Data mask of vcpu fault
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @return                      Data mask of vcpu fault
  */
 seL4_Word get_vcpu_fault_data_mask(vm_vcpu_t *vcpu);
 
-/*
+/***
+ * @function get_vcpu_fault_size(vcpu)
  * Get access size of the current vcpu fault
- * @param vcpu  Handle to vcpu
- * @return      Access size of vcpu fault
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @return                      Access size of vcpu fault
  */
 size_t get_vcpu_fault_size(vm_vcpu_t *vcpu);
 
-/*
+/***
+ * @function is_vcpu_read_fault(vcpu)
  * Is current vcpu fault a read fault
- * @param vcpu  Handle to vcpu
- * @return      True if read fault, False if write fault
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @return                      True if read fault, False if write fault
  */
 bool is_vcpu_read_fault(vm_vcpu_t *vcpu);
 
-/*
+/***
+ * @function set_vcpu_fault_data(vcpu, data)
  * Set the data of the current vcpu fault
- * @param vcpu  Handle to vcpu
- * @param data  Data to set for current vcpu fault
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @param {seL4_Word} data      Data to set for current vcpu fault
  * @return 0 for success, otherwise -1 for error
  */
 int set_vcpu_fault_data(vm_vcpu_t *vcpu, seL4_Word data);
 
-/*
+/***
+ * @function emulate_vcpu_fault(vcpu, data)
  * Emulate a read or write fault on a given data value
- * @param vcpu  Handle to vcpu
- * @param data  Data to perform emulate fault on
- * @return      Emulation result of vcpu fault over given data value
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
+ * @param {seL4_Word} data      Data to perform emulate fault on
+ * @return                      Emulation result of vcpu fault over given data value
  */
 seL4_Word emulate_vcpu_fault(vm_vcpu_t *vcpu, seL4_Word data);
 
-/*
+/***
+ * @function advance_vcpu_fault(vcpu)
  * Advance the current vcpu fault to the next stage/instruction
- * @param vcpu  Handle to vcpu
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
  */
 void advance_vcpu_fault(vm_vcpu_t *vcpu);
 
-/*
+/***
+ * @function restart_vcpu_fault(vcpu)
  * Restart the current vcpu fault
- * @param vcpu  Handle to vcpu
+ * @param {vm_vcpu_t *} vcpu    Handle to vcpu
  */
 void restart_vcpu_fault(vm_vcpu_t *vcpu);
diff --git a/libsel4vm/include/sel4vm/guest_vm.h b/libsel4vm/include/sel4vm/guest_vm.h
index ca0a281..bf6e2f1 100644
--- a/libsel4vm/include/sel4vm/guest_vm.h
+++ b/libsel4vm/include/sel4vm/guest_vm.h
@@ -29,20 +29,61 @@
 typedef struct vm_run vm_run_t;
 typedef struct vm_arch vm_arch_t;
 
+/***
+ * @module guest_vm.h
+ * The guest vm interface is central to libsel4vm, providing definitions of the guest vm datastructure and
+ * primitives to run the VM instance and start its vcpus.
+ */
+
+/**
+ * Type signature of unhandled memory fault function, invoked when a memory fault is unable to be handled
+ * @param {vm_t *} vm           A handle to the VM
+ * @param {vm_vcpu_t *} vcpu    A handle to the fault vcpu
+ * @param {uintptr_t} paddr     Faulting guest physical address
+ * @param {size_t} len          Length of faulted access
+ * @param {void *} cookie       User cookie to pass onto callback
+ * @return                      Fault handling status code: HANDLED, UNHANDLED, RESTART, ERROR
+ */
 typedef memory_fault_result_t (*unhandled_mem_fault_callback_fn)(vm_t *vm, vm_vcpu_t *vcpu, uintptr_t paddr,
                                                                  size_t len, void *cookie);
+
+/**
+ * Type signature of unhandled notification callback, invoked when a notification is recieved and cannot be processed
+ * by the vm runtime
+ * @param {vm_t *} vm                   A handle to the VM
+ * @param {seL4_Word} badge             Badge of inbound event
+ * @param {seL4_MessageInfo_t} tag      seL4 Message Info tag of inbound event (if IPC related)
+ * @param {void *} cookie               User cookie to pass onto callback
+ * @return                              -1 on failure otherwise 0 for success
+ */
 typedef int (*notification_callback_fn)(vm_t *vm, seL4_Word badge, seL4_MessageInfo_t tag,
                                         void *cookie);
 
+/***
+ * @struct vm_ram_region
+ * Structure representing individual RAM region. A VM can have multiple regions to represent its total RAM
+ * @param {uintptr_t} start     Guest physical start address of region
+ * @param {size_t} size         Size of region in bytes
+ * @param {int} allocated       Whether or not this region has been 'allocated'
+ */
 struct vm_ram_region {
-    /* Guest physical start address */
     uintptr_t start;
-    /* size in bytes */
     size_t size;
-    /* whether or not this region has been 'allocated' */
     int allocated;
 };
 
+/***
+ * @struct vm_mem
+ * Structure representing VM memory managment
+ * @param {vspace_t} vm_vspace                                              Guest VM's vspace
+ * @param {vka_object_t} vm_vspace_root                                     VKA allocated guest VM root vspace
+ * @param {vspace_t} vmm_vspace                                             Hosts/VMMs vspace
+ * @param {int} num_ram_regions                                             Total number of registered `vm_ram_regions`
+ * @param {struct vm_ram_region *}                                          Set of registered `vm_ram_regions`
+ * @param {vm_memory_reservation_cookie_t *}                                Initialised instance of vm memory interface
+ * @param {unhandled_mem_fault_callback_fn}  unhandled_mem_fault_handler    Registered callback for unhandled memory faults
+ * @param {void *} unhandled_mem_fault_cookie                               User data passed onto unhandled mem fault callback
+ */
 struct vm_mem {
     /* Guest vm vspace management */
     vspace_t vm_vspace;
@@ -61,15 +102,33 @@
     void *unhandled_mem_fault_cookie;
 };
 
+/***
+ * @struct vm_tcb
+ * Structure used for TCB management within a VCPU
+ * @param {vka_object_t} tcb            VKA allocated TCB object
+ * @param {vka_object_t} sc             VKA allocated scheduling context
+ * @param {int} priority                VCPU scheduling priority
+ */
 struct vm_tcb {
     /* Guest vm tcb management objects */
     vka_object_t tcb;
     vka_object_t sc;
     vka_object_t sched_ctrl;
-    /* Guest vm scheduling priority */
+    /* vcpu scheduling priority */
     int priority;
 };
 
+/***
+ * @struct vm_vcpu
+ * Structure used to represent a VCPU
+ * @param {struct vm *} vm                  Parent VM
+ * @param {vka_object_t} vcpu               VKA allocated vcpu object
+ * @param {struct vm_tcb} tcb               VCPUs TCB management structure
+ * @param {unsigned int} vcpu_id            VCPU Identifier
+ * @param {int} target_cpu                  The target core the vcpu is assigned to
+ * @param {bool} vcpu_online                Flag representing if the vcpu has been started
+ * @param {struct vm_vcpu_arch} vcpu_arch   Architecture specific vcpu properties
+ */
 struct vm_vcpu {
     /* Parent vm */
     struct vm *vm;
@@ -79,7 +138,7 @@
     struct vm_tcb tcb;
     /* Id of vcpu */
     unsigned int vcpu_id;
-    /* The identifier used by the guest to enable this vcpu */
+    /* The target core the vcpu is assigned to */
     int target_cpu;
     /* is the vcpu online */
     bool vcpu_online;
@@ -87,19 +146,47 @@
     struct vm_vcpu_arch vcpu_arch;
 };
 
+/***
+ * @struct vm_run
+ * VM Runtime management structure
+ * @param {int} exit_reason                                     Records last vm exit reason
+ * @param {notification_callback_fn} notification_callback      Callback for processing unhandled notifications
+ * @param {void *} notification_callback_cookie                 A cookie to supply to the notification callback
+ */
 struct vm_run {
-    /* Records last vm exit reason */
     int exit_reason;
     notification_callback_fn notification_callback;
     void *notification_callback_cookie;
 };
 
+/***
+ * @struct vm_cspace
+ * VM cspace management structure
+ * @param {vka_object_t} cspace_obj     VKA allocated cspace object
+ * @param {seL4_Word} cspace_root_data  cspace root data capability
+ */
 struct vm_cspace {
-    /* Kernel cspace object */
     vka_object_t cspace_obj;
     seL4_Word cspace_root_data;
 };
 
+/***
+ * @struct vm
+ * Structure representing a VM instance
+ * @param {struct vm_arch} arch         Architecture specfic vm structure
+ * @param {unsigned int} num_vcpus      Number of vcpus created for the VM
+ * @param {struct vm_vcpu*} vcpus       vcpu's belonging to the VM
+ * @param {struct vm_mem} mem           Memory management structure
+ * @param {struct vm_run} run           VM Runtime management structure
+ * @param {struct vm_cspace} cspace     VM CSpace management structure
+ * @param {seL4_CPtr} host_endpoint     Host/VMM endpoint. `vm_run` waits on this enpoint
+ * @param {vka_t *} vka                 Handle to virtual kernel allocator for seL4 kernel object allocation
+ * @param {ps_io_ops_t *} io_ops        Handle to platforms io ops
+ * @param {simple_t *} simple           Handle to hosts simple environment
+ * @param {char *} vm_name              String used to describe VM. Useful for debugging
+ * @param {unsigned int} vm_id          Identifier for VM. Useful for debugging
+ * @param {bool} vm_initialised         Boolean flagging whether VM is intialised or not
+ */
 struct vm {
     /* Architecture specfic vm structure */
     struct vm_arch arch;
@@ -124,13 +211,43 @@
     bool vm_initialised;
 };
 
-/* Run the VM */
+/***
+ * @function vm_run(vm_t *vm)
+ * Enter the VM event runtime loop.
+ * This funtion is a blocking call, returning on the event of an unhandled VM exit or error
+ * @param {vm_t *} vm   A handle to the VM to run
+ * @return              0 on success, -1 on error
+ */
 int vm_run(vm_t *vm);
-/* Start a vcpu */
+
+/***
+ * @function vcpu_start(vcpu)
+ * Start an initialised vcpu thread
+ * @param {vm_vcpu_t *} vcpu    A handle to vcpu to start
+ * @return                      0 on success, -1 on error
+ */
 int vcpu_start(vm_vcpu_t *vcpu);
 
 /* Unhandled fault callback registration functions */
+
+/***
+ * @function vm_register_unhandled_mem_fault_callback(vm, fault_handler, cookie)
+ * Register a callback for processing unhandled memory faults (memory regions not previously registered or reserved)
+ * @param {vm_t *} vm                                           A handle to the VM
+ * @param {unhandled_mem_fault_callback_fn} fault_handler       A user supplied callback to process unhandled memory faults
+ * @param {void *} cookie                                       A cookie to supply to the memory fault handler
+ * @return                                                      0 on success, -1 on error
+ */
 int vm_register_unhandled_mem_fault_callback(vm_t *vm, unhandled_mem_fault_callback_fn fault_handler,
                                              void *cookie);
+
+/***
+ * @function vm_register_notification_callback(vm, notification_callback, cookie)
+ * Register a callback for processing unhandled notifications (events unknown to libsel4vm)
+ * @param {vm_t *} vm                                           A handle to the VM
+ * @param {notification_callback_fn} notification_callback      A user supplied callback to process unhandled notifications
+ * @param {void *} cookie                                       A cookie to supply to the callback
+ * @return                                                      0 on success, -1 on error
+ */
 int vm_register_notification_callback(vm_t *vm, notification_callback_fn notification_callback,
                                       void *cookie);
diff --git a/libsel4vm/include/sel4vm/guest_vm_util.h b/libsel4vm/include/sel4vm/guest_vm_util.h
index f93effa..d302047 100644
--- a/libsel4vm/include/sel4vm/guest_vm_util.h
+++ b/libsel4vm/include/sel4vm/guest_vm_util.h
@@ -12,13 +12,31 @@
 
 #pragma once
 
+/***
+ * @module guest_vm_util.h
+ * The libsel4vm VM util interface provides a set of useful methods to query a guest vm instance.
+ */
+
 #include <sel4vm/guest_vm.h>
 
+/***
+ * @function vm_get_vcpu_tcb(vcpu)
+ * Get the TCB CPtr a given VCPU is associated with
+ * @param {vm_vcpu_t} vcpu  A handle to the vcpu
+ * @return                  seL4_CPtr of TCB object
+ */
 static inline seL4_CPtr vm_get_vcpu_tcb(vm_vcpu_t *vcpu)
 {
     return vcpu->tcb.tcb.cptr;
 }
 
+/***
+ * @function vm_get_vcpu(vm, vcpu_id)
+ * Get the VCPU CPtr associatated with a given logical ID
+ * @param {vm_t *} vm       A handle to the vm owning the vcpu
+ * @param {int} vcpu_id     Logical ID of the vcpu
+ * @return                  seL4_CapNull if no vcpu exists, otherwise the seL4_CPtr of the VCPU object
+ */
 static inline seL4_CPtr vm_get_vcpu(vm_t *vm, int vcpu_id)
 {
     if (vcpu_id >= vm->num_vcpus) {
@@ -27,6 +45,13 @@
     return vm->vcpus[vcpu_id]->vcpu.cptr;
 }
 
+/***
+ * @function vm_vcpu_for_target_cpu(vm, target_cpu)
+ * Get the VCPU object that is assigned to a given target core ID
+ * @param {vm_t *} vm           A handle to the vm owning the vcpu
+ * @param {int} target_cpu      Target core ID
+ * @return                      NULL if no vcpu is assigned to the target core, otherwise the vm_vcpu_t object
+ */
 static inline vm_vcpu_t *vm_vcpu_for_target_cpu(vm_t *vm, int target_cpu)
 {
     for (int i = 0; i < vm->num_vcpus; i++) {
@@ -37,6 +62,12 @@
     return NULL;
 }
 
+/***
+ * @function vm_find_free_unassigned_vcpu(vm)
+ * Find a VCPU object that hasn't been assigned to a target core
+ * @param {vm_t *} vm           A handle to the vm owning the vcpu
+ * @return                      NULL if no vcpu can be found, otherwise the vm_vcpu_t object
+ */
 static inline vm_vcpu_t *vm_find_free_unassigned_vcpu(vm_t *vm)
 {
     for (int i = 0; i < vm->num_vcpus; i++) {
@@ -47,16 +78,34 @@
     return NULL;
 }
 
+/***
+ * @function is_vcpu_online(vcpu)
+ * Find if a given VCPU is online
+ * @param {vm_vcpu_t *} vcpu    A handle to the vcpu
+ * @return                      True if the vcpu is online, otherwise False
+ */
 static inline bool is_vcpu_online(vm_vcpu_t *vcpu)
 {
     return vcpu->vcpu_online;
 }
 
+/***
+ * @function vm_get_vspace(vm)
+ * Get the vspace of a given VM instance
+ * @param {vm_t *} vm       A handle to the VM
+ * @return                  A vspace_t object
+ */
 static inline vspace_t *vm_get_vspace(vm_t *vm)
 {
     return &vm->mem.vm_vspace;
 }
 
+/***
+ * @function vm_get_vmm_vspace(vm)
+ * Get the vspace of the host VMM associated with a given VM instance
+ * @param {vm_t *} vm       A handle to the VM
+ * @return                  A vspace_t object
+ */
 static inline vspace_t *vm_get_vmm_vspace(vm_t *vm)
 {
     return &vm->mem.vmm_vspace;
diff --git a/libsel4vm/src/guest_memory.h b/libsel4vm/src/guest_memory.h
index ef8524f..86955d4 100644
--- a/libsel4vm/src/guest_memory.h
+++ b/libsel4vm/src/guest_memory.h
@@ -15,7 +15,23 @@
 #include <sel4vm/guest_vm.h>
 #include <sel4vm/guest_memory.h>
 
+/**
+ * Handle a vm memory fault through searching previously created reservations and invoking the appropriate fault callback
+ * @param {vm_t *} vm               A handle to the VM
+ * @param {vm_vcpu_t *} vcpu        A handle to the faulting vcpu
+ * @param {uintptr_t} addr          Faulting address
+ * @param {size_t} size             Size of the faulting region
+ * @return                          Fault handling status code: HANDLED, UNHANDLED, RESTART, ERROR
+ */
 memory_fault_result_t vm_memory_handle_fault(vm_t *vm, vm_vcpu_t *vcpu, uintptr_t addr, size_t size);
 
+/**
+ * Map a vm memory reservation - this invokation is performed immediately (mapping is not deferred)
+ * @param {vm_t *} vm                                   A handle to the VM
+ * @param {vm_memory_reservation_t *} vm_reservation    A handle to the VM reservation being mapped
+ * @param {memory_map_iterator_fn} map_iterator         Pointer to the map iterator function for retrieving reservation frames
+ * @param {void *} map_cookie                           Cookie to pass onto map iterator
+ * @return                                              0 on success, -1 on error
+ */
 int map_vm_memory_reservation(vm_t *vm, vm_memory_reservation_t *vm_reservation,
                               memory_map_iterator_fn map_iterator, void *map_cookie);