diff --git a/libsel4vm/docs/libsel4vm_arm_guest_vm.md b/libsel4vm/docs/libsel4vm_arm_guest_vm.md
new file mode 100644
index 0000000..57b846b
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_arm_guest_vm.md
@@ -0,0 +1,70 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_register_unhandled_vcpu_fault_callback(vcpu, vcpu_fault_callback, cookie)`](#function-vm_register_unhandled_vcpu_fault_callbackvcpu-vcpu_fault_callback-cookie)
+
+
+
+**Structs**:
+
+> [`vm_vcpu_arch`](#struct-vm_vcpu_arch)
+
+
+## Functions
+
+The interface `guest_vm_arch.h` defines the following functions.
+
+### Function `vm_register_unhandled_vcpu_fault_callback(vcpu, vcpu_fault_callback, cookie)`
+
+Register a callback for processing unhandled vcpu faults
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to the VCPU
+- `A {unhandled_vcpu_fault_callback_fn}`: user supplied callback to process unhandled vcpu faults
+- `A {void *}`: cookie to supply to the vcpu fault handler
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_vm_archh).
+
+
+## Structs
+
+The interface `guest_vm_arch.h` defines the following structs.
+
+### Struct `vm_vcpu_arch`
+
+Structure representing ARM specific vcpu properties
+
+**Elements:**
+
+- `fault {fault_t *}`: Current VCPU fault
+- `unhandled_vcpu_callback {unhandled_vcpu_fault_callback_fn}`: A callback for processing unhandled vcpu faults
+- `unhandled_vcpu_callback_cookie {void *}`: A cookie to supply to the vcpu fault handler
+
+Back to [interface description](#module-guest_vm_archh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_boot.md b/libsel4vm/docs/libsel4vm_boot.md
new file mode 100644
index 0000000..7863500
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_boot.md
@@ -0,0 +1,84 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `boot.h`
+
+The libsel4vm boot interface provides us with base abstractions to create, initialise and configure VM and VCPU instances.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_init(vm, vka, host_simple, host_vspace, io_ops, host_endpoint, name)`](#function-vm_initvm-vka-host_simple-host_vspace-io_ops-host_endpoint-name)
+
+> [`vm_create_vcpu(vm, priority)`](#function-vm_create_vcpuvm-priority)
+
+> [`vm_assign_vcpu_target(vcpu, target_cpu)`](#function-vm_assign_vcpu_targetvcpu-target_cpu)
+
+
+## Functions
+
+The interface `boot.h` defines the following functions.
+
+### Function `vm_init(vm, vka, host_simple, host_vspace, io_ops, host_endpoint, name)`
+
+Initialise/Create VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: Handle to the VM being initialised
+- `vka {vka_t *}`: Initialised handle to virtual kernel allocator for seL4 kernel object allocation
+- `host_simple {simple_t *}`: Initialised handle to hosts simple environment
+- `host_vspace {vspace_t}`: Initialised handle to hosts vspace
+- `ps_io_ops {ps_io_ops_t *}`: Initialised handle to platforms io ops
+- `host_enpoint {seL4_CPtr}`: Host's endpoint. The library will wait and manage the endpoint when running a VM instance
+- `name {const char *}`: String used to describe VM. Useful for debugging
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-booth).
+
+### Function `vm_create_vcpu(vm, priority)`
+
+Create a VCPU for a given VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to VM being configured with a new vcpu
+- `priority {int}`: The scheduling priority assigned to the VCPU thread
+
+**Returns:**
+
+- NULL for error, otherwise pointer to created vm_vcpu_t object
+
+Back to [interface description](#module-booth).
+
+### Function `vm_assign_vcpu_target(vcpu, target_cpu)`
+
+Assign a vcpu with logical target cpu to run on
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to the VCPU
+- `target {int}`: Logical target CPU ID
+
+**Returns:**
+
+- -1 for error, otherwise 0 for success
+
+Back to [interface description](#module-booth).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_arm_context.md b/libsel4vm/docs/libsel4vm_guest_arm_context.md
new file mode 100644
index 0000000..63b9871
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_arm_context.md
@@ -0,0 +1,136 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_set_thread_context(vcpu, context)`](#function-vm_set_thread_contextvcpu-context)
+
+> [`vm_set_thread_context_reg(vcpu, reg, value)`](#function-vm_set_thread_context_regvcpu-reg-value)
+
+> [`vm_get_thread_context(vcpu, context)`](#function-vm_get_thread_contextvcpu-context)
+
+> [`vm_get_thread_context_reg(vcpu, reg, value)`](#function-vm_get_thread_context_regvcpu-reg-value)
+
+> [`vm_set_arm_vcpu_reg(vcpu, reg, value)`](#function-vm_set_arm_vcpu_regvcpu-reg-value)
+
+> [`vm_get_arm_vcpu_reg(vcpu, reg, value)`](#function-vm_get_arm_vcpu_regvcpu-reg-value)
+
+
+## Functions
+
+The interface `guest_arm_context.h` defines the following functions.
+
+### Function `vm_set_thread_context(vcpu, context)`
+
+Set a VCPU's thread registers given a TCB user context
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `context {seL4_UserContext}`: seL4_UserContext applied to VCPU's TCB
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_arm_contexth).
+
+### Function `vm_set_thread_context_reg(vcpu, reg, value)`
+
+Set a single VCPU's TCB register
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {unsigned int}`: Index offset of register in seL4_UserContext e.g pc (seL4_UserContext.pc) => 0
+- `value {uintptr_t}`: Value to set TCB register with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_arm_contexth).
+
+### Function `vm_get_thread_context(vcpu, context)`
+
+Get a VCPU's TCB user context
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t}`: Handle to the vcpu
+- `context {seL4_UserContext}`: Pointer to user supplied seL4_UserContext to populate with VCPU's TCB user context
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_arm_contexth).
+
+### Function `vm_get_thread_context_reg(vcpu, reg, value)`
+
+Get a single VCPU's TCB register
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {unsigned int}`: Index offset of register in seL4_UserContext e.g pc (seL4_UserContext.pc) => 0
+- `value {uintptr_t *}`: Pointer to user supplied variable to populate TCB register value with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_arm_contexth).
+
+### Function `vm_set_arm_vcpu_reg(vcpu, reg, value)`
+
+Set an ARM VCPU register
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {seL4_Word}`: VCPU Register field defined in seL4_VCPUReg
+- `value {uintptr_t *}`: Value to set VCPU register with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_arm_contexth).
+
+### Function `vm_get_arm_vcpu_reg(vcpu, reg, value)`
+
+Get an ARM VCPU register
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {seL4_Word}`: VCPU Register field defined in seL4_VCPUReg
+- `value {uintptr_t *}`: Pointer to user supplied variable to populate VCPU register value with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_arm_contexth).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_iospace.md b/libsel4vm/docs/libsel4vm_guest_iospace.md
new file mode 100644
index 0000000..b9236bb
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_iospace.md
@@ -0,0 +1,47 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_guest_add_iospace(vm, loader, iospace)`](#function-vm_guest_add_iospacevm-loader-iospace)
+
+
+## Functions
+
+The interface `guest_iospace.h` defines the following functions.
+
+### Function `vm_guest_add_iospace(vm, loader, iospace)`
+
+Attach an additional IO space to the given VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `loader {vspace_t *}`: Host loader vspace to create a new iospace
+- `iospace {seL4_CPtr}`: Capability to iospace being added
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_iospaceh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_irq_controller.md b/libsel4vm/docs/libsel4vm_guest_irq_controller.md
new file mode 100644
index 0000000..9e9b23f
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_irq_controller.md
@@ -0,0 +1,99 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_inject_irq(vcpu, irq)`](#function-vm_inject_irqvcpu-irq)
+
+> [`vm_set_irq_level(vcpu, irq, irq_level)`](#function-vm_set_irq_levelvcpu-irq-irq_level)
+
+> [`vm_register_irq(vcpu, irq, ack_fn, cookie)`](#function-vm_register_irqvcpu-irq-ack_fn-cookie)
+
+> [`vm_create_default_irq_controller(vm)`](#function-vm_create_default_irq_controllervm)
+
+
+## Functions
+
+The interface `guest_irq_controller.h` defines the following functions.
+
+### Function `vm_inject_irq(vcpu, irq)`
+
+Inject an IRQ into a VM's interrupt controller
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the VCPU
+- `irq {int}`: IRQ number to inject
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_irq_controllerh).
+
+### Function `vm_set_irq_level(vcpu, irq, irq_level)`
+
+Set level of IRQ number into a VM's interrupt controller
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t}`: Handle to the VCPU
+- `irq {int}`: IRQ number to set level on
+- `irq_level {int}`: Value of IRQ level
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_irq_controllerh).
+
+### Function `vm_register_irq(vcpu, irq, ack_fn, cookie)`
+
+Register irq with an acknowledgment function
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the VCPU
+- `irq {int}`: IRQ number to register acknowledgement function on
+- `ack_fn {irq_ack_fn_t}`: IRQ acknowledgement function
+- `cookie {void *}`: Cookie to pass back with IRQ acknowledgement function
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_irq_controllerh).
+
+### Function `vm_create_default_irq_controller(vm)`
+
+Install the default interrupt controller into the VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: Handle to the VM
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_irq_controllerh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_memory.md b/libsel4vm/docs/libsel4vm_guest_memory.md
new file mode 100644
index 0000000..46a9e3d
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_memory.md
@@ -0,0 +1,169 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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`.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_reserve_memory_at(vm, addr, size, fault_callback, cookie)`](#function-vm_reserve_memory_atvm-addr-size-fault_callback-cookie)
+
+> [`vm_reserve_anon_memory(vm, size, fault_callback, cookie, addr)`](#function-vm_reserve_anon_memoryvm-size-fault_callback-cookie-addr)
+
+> [`vm_free_reserved_memory(vm, reservation)`](#function-vm_free_reserved_memoryvm-reservation)
+
+> [`vm_map_reservation(vm, reservation, map_iterator, cookie)`](#function-vm_map_reservationvm-reservation-map_iterator-cookie)
+
+> [`vm_get_reservation_memory_region(reservation, addr, size)`](#function-vm_get_reservation_memory_regionreservation-addr-size)
+
+> [`vm_memory_init(vm)`](#function-vm_memory_initvm)
+
+
+
+**Structs**:
+
+> [`vm_frame_t`](#struct-vm_frame_t)
+
+
+## Functions
+
+The interface `guest_memory.h` defines the following functions.
+
+### Function `vm_reserve_memory_at(vm, addr, size, fault_callback, cookie)`
+
+Reserve a region of the VM's memory at a given base address
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `addr {uintptr}`: Base address of the memory region being reserved
+- `size {size_t}`: Size of the memory region being reserved
+- `fault_callback {memory_fault_callback_fn}`: Callback function that will be invoked if memory region is faulted on
+- `cookie {void *}`: User cookie to pass onto to callback
+
+**Returns:**
+
+- NULL on failure otherwise a pointer to a reservation object representing the reserved region
+
+Back to [interface description](#module-guest_memoryh).
+
+### 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.
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `size {size_t}`: Size of the anoymous emory region being reserved
+- `fault_callback {memory_fault_callback_fn}`: Callback function that will be invoked if memory region is faulted on
+- `cookie {void *}`: User cookie to pass onto to callback
+- `addr {uintptr_t *}`: Pointer that will be set with the base address of the reserved anonymous region
+
+**Returns:**
+
+- NULL on failure otherwise a pointer to a reservation object representing the reserved region
+
+Back to [interface description](#module-guest_memoryh).
+
+### Function `vm_free_reserved_memory(vm, reservation)`
+
+Free memory reservation from the VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `reservation {vm_memory_reservation_t *}`: Pointer to the reservation being free'd
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-guest_memoryh).
+
+### Function `vm_map_reservation(vm, reservation, map_iterator, cookie)`
+
+Map a reservation into the VM's virtual address space
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `reservation {vm_memory_reservation_t *}`: Pointer to reservation object being mapped
+- `map_iterator {memory_map_iterator_fn}`: Iterator function that returns a cap to the memory region being mapped
+- `cookie {void *}`: Cookie to pass onto map_iterator function
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-guest_memoryh).
+
+### Function `vm_get_reservation_memory_region(reservation, addr, size)`
+
+Get the memory region information (address & size) from a given reservation
+
+**Parameters:**
+
+- `reservation {vm_memory_reservation_t *}`: Pointer to reservation object
+- `addr {uintptr_t *}`: Pointer that will be set with the address of reservation
+- `size {size_t *}`: Pointer that will be set with the size of reservation
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-guest_memoryh).
+
+### Function `vm_memory_init(vm)`
+
+Initialise a VM's memory management interface
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-guest_memoryh).
+
+
+## Structs
+
+The interface `guest_memory.h` defines the following structs.
+
+### Struct `vm_frame_t`
+
+Structure representing a mappable memory frame
+
+**Elements:**
+
+- `cptr {seL4_CPtr}`: Capability to frame
+- `rights {seL4_CapRights_t}`: Mapping rights of frame
+- `vaddr {uintptr_t}`: Virtual address of which to map the frame into
+- `size_bits {size_t}`: Size of frame in bits
+
+Back to [interface description](#module-guest_memoryh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_memory_helpers.md b/libsel4vm/docs/libsel4vm_guest_memory_helpers.md
new file mode 100644
index 0000000..80f0f3c
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_memory_helpers.md
@@ -0,0 +1,49 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `guest_memory_helpers.h`
+
+The libsel4vm guest memory helpers interface provides simple utilities for using the guest memory interface.
+
+### Brief content:
+
+**Functions**:
+
+> [`default_error_fault_callback(vm, vcpu, fault_addr, fault_length, cookie)`](#function-default_error_fault_callbackvm-vcpu-fault_addr-fault_length-cookie)
+
+
+## Functions
+
+The interface `guest_memory_helpers.h` defines the following functions.
+
+### 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.
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `vcpu {vm_vcpu_t *}`: A handle to the fault vcpu
+- `fault {uintptr_t}`: addr    Faulting address
+- `fault_length {size_t}`: Length of faulted access
+- `cookie {void *}`: User cookie to pass onto callback
+
+**Returns:**
+
+- Always returns FAULT_ERROR
+
+Back to [interface description](#module-guest_memory_helpersh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_ram.md b/libsel4vm/docs/libsel4vm_guest_ram.md
new file mode 100644
index 0000000..25d4bd0
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_ram.md
@@ -0,0 +1,198 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_guest_ram_read_callback(vm, guest_addr, vaddr, size, offset, buf)`](#function-vm_guest_ram_read_callbackvm-guest_addr-vaddr-size-offset-buf)
+
+> [`vm_guest_ram_write_callback(vm, guest_addr, vaddr, size, offset, buf)`](#function-vm_guest_ram_write_callbackvm-guest_addr-vaddr-size-offset-buf)
+
+> [`vm_ram_touch(vm, addr, size, touch_callback, cookie)`](#function-vm_ram_touchvm-addr-size-touch_callback-cookie)
+
+> [`vm_ram_find_largest_free_region(vm, addr, size)`](#function-vm_ram_find_largest_free_regionvm-addr-size)
+
+> [`vm_ram_register(vm, bytes)`](#function-vm_ram_registervm-bytes)
+
+> [`vm_ram_register_at(vm, start, bytes, untyped)`](#function-vm_ram_register_atvm-start-bytes-untyped)
+
+> [`vm_ram_mark_allocated(vm, start, bytes)`](#function-vm_ram_mark_allocatedvm-start-bytes)
+
+> [`vm_ram_allocate(vm, bytes)`](#function-vm_ram_allocatevm-bytes)
+
+> [`vm_ram_free(vm, start, bytes)`](#function-vm_ram_freevm-start-bytes)
+
+
+## Functions
+
+The interface `guest_ram.h` defines the following functions.
+
+### 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
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `guest_addr {uintptr_t}`: Guest physical address to read from
+- `vmm_vaddr {void *}`: Virtual address in hosts (vmm) vspace corresponding with the 'guest_addr'
+- `size {size_t}`: Size of region being currently accessed
+- `offset {size_t}`: Current offset from the base guest physical address supplied to 'vm_ram_touch'
+- `cookie {void *}`: User supplied buffer to store read data into
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_ramh).
+
+### 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
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `guest_addr {uintptr_t}`: Guest physical address to write to
+- `vmm_vaddr {void *}`: Virtual address in hosts (vmm) vspace corresponding with the 'guest_addr'
+- `size {size_t}`: Size of region being currently accessed
+- `offset {size_t}`: Current offset from the base guest physical address supplied to 'vm_ram_touch'
+- `cookie {void *}`: User supplied buffer to write data from
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_ramh).
+
+### 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
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `addr {uintptr_t}`: Address to access in the guest vm
+- `size {size_t}`: Size of memory region to access
+- `callback {ram_touch_callback_fn}`: Callback to invoke on each page access
+- `cookie {void *}`: User data to pass onto callback
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_ramh).
+
+### Function `vm_ram_find_largest_free_region(vm, addr, size)`
+
+Find the largest free ram region
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `addr {uintptr_t *}`: Pointer to be set with largest region address
+- `size {size_t *}`: Pointer to be set with largest region size
+
+**Returns:**
+
+- -1 on failure, otherwise 0 for success
+
+Back to [interface description](#module-guest_ramh).
+
+### Function `vm_ram_register(vm, bytes)`
+
+Reserve a region of memory for RAM in the guest VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `bytes {size_t}`: Size of RAM region to allocate
+
+**Returns:**
+
+- Starting address of registered ram region
+
+Back to [interface description](#module-guest_ramh).
+
+### 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
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM that ram needs to be allocated for
+- `start {uintptr_t}`: Starting guest physical address of the ram region being allocated
+- `size {size_t}`: The size of the RAM region to be allocated
+- `untyped {bool}`: Allocate RAM frames such that it uses untyped memory
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_ramh).
+
+### Function `vm_ram_mark_allocated(vm, start, bytes)`
+
+Mark a registered region of RAM as allocated
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `start {uintptr_t}`: Starting address of guest ram region
+- `bytes {size_t}`: Size of RAM region
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-guest_ramh).
+
+### Function `vm_ram_allocate(vm, bytes)`
+
+Allocate a region of registered ram
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `bytes {size_t}`: Size of allocation
+
+**Returns:**
+
+- Starting address of allocated ram region
+
+Back to [interface description](#module-guest_ramh).
+
+### Function `vm_ram_free(vm, start, bytes)`
+
+Free a RAM a previously allocated RAM region
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM that ram needs to be free'd for
+- `start {uintptr_t}`: Starting guest physical address of the ram region being free'd
+- `size {size_t}`: The size of the RAM region to be free'd
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-guest_ramh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_vcpu_fault.md b/libsel4vm/docs/libsel4vm_guest_vcpu_fault.md
new file mode 100644
index 0000000..05130f0
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_vcpu_fault.md
@@ -0,0 +1,192 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`get_vcpu_fault_address(vcpu)`](#function-get_vcpu_fault_addressvcpu)
+
+> [`get_vcpu_fault_ip(vcpu)`](#function-get_vcpu_fault_ipvcpu)
+
+> [`get_vcpu_fault_data(vcpu)`](#function-get_vcpu_fault_datavcpu)
+
+> [`get_vcpu_fault_data_mask(vcpu)`](#function-get_vcpu_fault_data_maskvcpu)
+
+> [`get_vcpu_fault_size(vcpu)`](#function-get_vcpu_fault_sizevcpu)
+
+> [`is_vcpu_read_fault(vcpu)`](#function-is_vcpu_read_faultvcpu)
+
+> [`set_vcpu_fault_data(vcpu, data)`](#function-set_vcpu_fault_datavcpu-data)
+
+> [`emulate_vcpu_fault(vcpu, data)`](#function-emulate_vcpu_faultvcpu-data)
+
+> [`advance_vcpu_fault(vcpu)`](#function-advance_vcpu_faultvcpu)
+
+> [`restart_vcpu_fault(vcpu)`](#function-restart_vcpu_faultvcpu)
+
+
+## Functions
+
+The interface `guest_vcpu_fault.h` defines the following functions.
+
+### Function `get_vcpu_fault_address(vcpu)`
+
+Get current fault address of vcpu
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+- Current fault address of vcpu
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `get_vcpu_fault_ip(vcpu)`
+
+Get instruction pointer of current vcpu fault
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+- Intruction pointer of vcpu fault
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `get_vcpu_fault_data(vcpu)`
+
+Get the data of the current vcpu fault
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+- Data of vcpu fault
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `get_vcpu_fault_data_mask(vcpu)`
+
+Get data mask of the current vcpu fault
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+- Data mask of vcpu fault
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `get_vcpu_fault_size(vcpu)`
+
+Get access size of the current vcpu fault
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+- Access size of vcpu fault
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `is_vcpu_read_fault(vcpu)`
+
+Is current vcpu fault a read fault
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+- True if read fault, False if write fault
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `set_vcpu_fault_data(vcpu, data)`
+
+Set the data of the current vcpu fault
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+- `data {seL4_Word}`: Data to set for current vcpu fault
+
+**Returns:**
+
+- 0 for success, otherwise -1 for error
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `emulate_vcpu_fault(vcpu, data)`
+
+Emulate a read or write fault on a given data value
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+- `data {seL4_Word}`: Data to perform emulate fault on
+
+**Returns:**
+
+- Emulation result of vcpu fault over given data value
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `advance_vcpu_fault(vcpu)`
+
+Advance the current vcpu fault to the next stage/instruction
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `restart_vcpu_fault(vcpu)`
+
+Restart the current vcpu fault
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to vcpu
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_vm.md b/libsel4vm/docs/libsel4vm_guest_vm.md
new file mode 100644
index 0000000..b0375d3
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_vm.md
@@ -0,0 +1,223 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_run(vm_t *vm)`](#function-vm_runvm_t-vm)
+
+> [`vcpu_start(vcpu)`](#function-vcpu_startvcpu)
+
+> [`vm_register_unhandled_mem_fault_callback(vm, fault_handler, cookie)`](#function-vm_register_unhandled_mem_fault_callbackvm-fault_handler-cookie)
+
+> [`vm_register_notification_callback(vm, notification_callback, cookie)`](#function-vm_register_notification_callbackvm-notification_callback-cookie)
+
+
+
+**Structs**:
+
+> [`vm_ram_region`](#struct-vm_ram_region)
+
+> [`vm_mem`](#struct-vm_mem)
+
+> [`vm_tcb`](#struct-vm_tcb)
+
+> [`vm_vcpu`](#struct-vm_vcpu)
+
+> [`vm_run`](#struct-vm_run)
+
+> [`vm_cspace`](#struct-vm_cspace)
+
+> [`vm`](#struct-vm)
+
+
+## Functions
+
+The interface `guest_vm.h` defines the following functions.
+
+### 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
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM to run
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_vmh).
+
+### Function `vcpu_start(vcpu)`
+
+Start an initialised vcpu thread
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to vcpu to start
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_vmh).
+
+### 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)
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `fault_handler {unhandled_mem_fault_callback_fn}`: A user supplied callback to process unhandled memory faults
+- `cookie {void *}`: A cookie to supply to the memory fault handler
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_vmh).
+
+### Function `vm_register_notification_callback(vm, notification_callback, cookie)`
+
+Register a callback for processing unhandled notifications (events unknown to libsel4vm)
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `notification_callback {notification_callback_fn}`: A user supplied callback to process unhandled notifications
+- `cookie {void *}`: A cookie to supply to the callback
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-guest_vmh).
+
+
+## Structs
+
+The interface `guest_vm.h` defines the following structs.
+
+### Struct `vm_ram_region`
+
+Structure representing individual RAM region. A VM can have multiple regions to represent its total RAM
+
+**Elements:**
+
+- `start {uintptr_t}`: Guest physical start address of region
+- `size {size_t}`: Size of region in bytes
+- `allocated {int}`: Whether or not this region has been 'allocated'
+
+Back to [interface description](#module-guest_vmh).
+
+### Struct `vm_mem`
+
+Structure representing VM memory managment
+
+**Elements:**
+
+- `vm_vspace {vspace_t}`: Guest VM's vspace
+- `vm_vspace_root {vka_object_t}`: VKA allocated guest VM root vspace
+- `vmm_vspace {vspace_t}`: Hosts/VMMs vspace
+- `num_ram_regions {int}`: Total number of registered `vm_ram_regions`
+- `Set {struct vm_ram_region *}`: of registered `vm_ram_regions`
+- `Initialised {vm_memory_reservation_cookie_t *}`: instance of vm memory interface
+- `unhandled_mem_fault_handler {unhandled_mem_fault_callback_fn}`: Registered callback for unhandled memory faults
+- `unhandled_mem_fault_cookie {void *}`: User data passed onto unhandled mem fault callback
+
+Back to [interface description](#module-guest_vmh).
+
+### Struct `vm_tcb`
+
+Structure used for TCB management within a VCPU
+
+**Elements:**
+
+- `tcb {vka_object_t}`: VKA allocated TCB object
+- `sc {vka_object_t}`: VKA allocated scheduling context
+- `priority {int}`: VCPU scheduling priority
+
+Back to [interface description](#module-guest_vmh).
+
+### Struct `vm_vcpu`
+
+Structure used to represent a VCPU
+
+**Elements:**
+
+- `vm {struct vm *}`: Parent VM
+- `vcpu {vka_object_t}`: VKA allocated vcpu object
+- `tcb {struct vm_tcb}`: VCPUs TCB management structure
+- `vcpu_id {unsigned int}`: VCPU Identifier
+- `target_cpu {int}`: The target core the vcpu is assigned to
+- `vcpu_online {bool}`: Flag representing if the vcpu has been started
+- `vcpu_arch {struct vm_vcpu_arch}`: Architecture specific vcpu properties
+
+Back to [interface description](#module-guest_vmh).
+
+### Struct `vm_run`
+
+VM Runtime management structure
+
+**Elements:**
+
+- `exit_reason {int}`: Records last vm exit reason
+- `notification_callback {notification_callback_fn}`: Callback for processing unhandled notifications
+- `notification_callback_cookie {void *}`: A cookie to supply to the notification callback
+
+Back to [interface description](#module-guest_vmh).
+
+### Struct `vm_cspace`
+
+VM cspace management structure
+
+**Elements:**
+
+- `cspace_obj {vka_object_t}`: VKA allocated cspace object
+- `cspace_root_data {seL4_Word}`: cspace root data capability
+
+Back to [interface description](#module-guest_vmh).
+
+### Struct `vm`
+
+Structure representing a VM instance
+
+**Elements:**
+
+- `arch {struct vm_arch}`: Architecture specfic vm structure
+- `num_vcpus {unsigned int}`: Number of vcpus created for the VM
+- `vcpus {struct vm_vcpu*}`: vcpu's belonging to the VM
+- `mem {struct vm_mem}`: Memory management structure
+- `run {struct vm_run}`: VM Runtime management structure
+- `cspace {struct vm_cspace}`: VM CSpace management structure
+- `host_endpoint {seL4_CPtr}`: Host/VMM endpoint. `vm_run` waits on this enpoint
+- `vka {vka_t *}`: Handle to virtual kernel allocator for seL4 kernel object allocation
+- `io_ops {ps_io_ops_t *}`: Handle to platforms io ops
+- `simple {simple_t *}`: Handle to hosts simple environment
+- `vm_name {char *}`: String used to describe VM. Useful for debugging
+- `vm_id {unsigned int}`: Identifier for VM. Useful for debugging
+- `vm_initialised {bool}`: Boolean flagging whether VM is intialised or not
+
+Back to [interface description](#module-guest_vmh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_vm_util.md b/libsel4vm/docs/libsel4vm_guest_vm_util.md
new file mode 100644
index 0000000..ce10e09
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_vm_util.md
@@ -0,0 +1,142 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `guest_vm_util.h`
+
+The libsel4vm VM util interface provides a set of useful methods to query a guest vm instance.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_get_vcpu_tcb(vcpu)`](#function-vm_get_vcpu_tcbvcpu)
+
+> [`vm_get_vcpu(vm, vcpu_id)`](#function-vm_get_vcpuvm-vcpu_id)
+
+> [`vm_vcpu_for_target_cpu(vm, target_cpu)`](#function-vm_vcpu_for_target_cpuvm-target_cpu)
+
+> [`vm_find_free_unassigned_vcpu(vm)`](#function-vm_find_free_unassigned_vcpuvm)
+
+> [`is_vcpu_online(vcpu)`](#function-is_vcpu_onlinevcpu)
+
+> [`vm_get_vspace(vm)`](#function-vm_get_vspacevm)
+
+> [`vm_get_vmm_vspace(vm)`](#function-vm_get_vmm_vspacevm)
+
+
+## Functions
+
+The interface `guest_vm_util.h` defines the following functions.
+
+### Function `vm_get_vcpu_tcb(vcpu)`
+
+Get the TCB CPtr a given VCPU is associated with
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t}`: A handle to the vcpu
+
+**Returns:**
+
+- seL4_CPtr of TCB object
+
+Back to [interface description](#module-guest_vm_utilh).
+
+### Function `vm_get_vcpu(vm, vcpu_id)`
+
+Get the VCPU CPtr associatated with a given logical ID
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the vm owning the vcpu
+- `vcpu_id {int}`: Logical ID of the vcpu
+
+**Returns:**
+
+- seL4_CapNull if no vcpu exists, otherwise the seL4_CPtr of the VCPU object
+
+Back to [interface description](#module-guest_vm_utilh).
+
+### Function `vm_vcpu_for_target_cpu(vm, target_cpu)`
+
+Get the VCPU object that is assigned to a given target core ID
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the vm owning the vcpu
+- `target_cpu {int}`: Target core ID
+
+**Returns:**
+
+- NULL if no vcpu is assigned to the target core, otherwise the vm_vcpu_t object
+
+Back to [interface description](#module-guest_vm_utilh).
+
+### Function `vm_find_free_unassigned_vcpu(vm)`
+
+Find a VCPU object that hasn't been assigned to a target core
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the vm owning the vcpu
+
+**Returns:**
+
+- NULL if no vcpu can be found, otherwise the vm_vcpu_t object
+
+Back to [interface description](#module-guest_vm_utilh).
+
+### Function `is_vcpu_online(vcpu)`
+
+Find if a given VCPU is online
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to the vcpu
+
+**Returns:**
+
+- True if the vcpu is online, otherwise False
+
+Back to [interface description](#module-guest_vm_utilh).
+
+### Function `vm_get_vspace(vm)`
+
+Get the vspace of a given VM instance
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+
+**Returns:**
+
+- A vspace_t object
+
+Back to [interface description](#module-guest_vm_utilh).
+
+### Function `vm_get_vmm_vspace(vm)`
+
+Get the vspace of the host VMM associated with a given VM instance
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+
+**Returns:**
+
+- A vspace_t object
+
+Back to [interface description](#module-guest_vm_utilh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_guest_x86_context.md b/libsel4vm/docs/libsel4vm_guest_x86_context.md
new file mode 100644
index 0000000..93abefc
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_guest_x86_context.md
@@ -0,0 +1,136 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_set_thread_context(vcpu, context)`](#function-vm_set_thread_contextvcpu-context)
+
+> [`vm_set_thread_context_reg(vcpu, reg, value)`](#function-vm_set_thread_context_regvcpu-reg-value)
+
+> [`vm_get_thread_context(vcpu, context)`](#function-vm_get_thread_contextvcpu-context)
+
+> [`vm_get_thread_context_reg(vcpu, reg, value)`](#function-vm_get_thread_context_regvcpu-reg-value)
+
+> [`vm_set_vmcs_field(vcpu, field, value)`](#function-vm_set_vmcs_fieldvcpu-field-value)
+
+> [`vm_get_vmcs_field(vcpu, field, value)`](#function-vm_get_vmcs_fieldvcpu-field-value)
+
+
+## Functions
+
+The interface `guest_x86_context.h` defines the following functions.
+
+### Function `vm_set_thread_context(vcpu, context)`
+
+Set a VCPU's thread registers given a seL4_VCPUContext
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `context {seL4_VCPUContext}`: seL4_VCPUContext applied to VCPU Registers
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_x86_contexth).
+
+### Function `vm_set_thread_context_reg(vcpu, reg, value)`
+
+Set a single VCPU's thread register in a seL4_VCPUContext
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {vcpu_context_reg_t}`: Register enumerated by vcpu_context_reg
+- `value {uint32_t}`: Value to set register with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_x86_contexth).
+
+### Function `vm_get_thread_context(vcpu, context)`
+
+Get a VCPU's thread context
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `context {seL4_VCPUContext *}`: Pointer to user supplied seL4_VCPUContext to populate with VCPU's current context
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_x86_contexth).
+
+### Function `vm_get_thread_context_reg(vcpu, reg, value)`
+
+Get a single VCPU's thread register
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {vcpu_context_reg_t}`: Register enumerated by vcpu_context_reg
+- `value {uint32_t *}`: Pointer to user supplied variable to populate register value with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_x86_contexth).
+
+### Function `vm_set_vmcs_field(vcpu, field, value)`
+
+Set a VMCS field
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {seL4_Word}`: VMCS field
+- `value {uint32_t}`: Value to set VMCS field with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_x86_contexth).
+
+### Function `vm_get_vmcs_field(vcpu, field, value)`
+
+Get a VMCS register
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Handle to the vcpu
+- `reg {seL4_Word}`: VMCS field
+- `value {uint32_t *}`: Pointer to user supplied variable to populate VMCS field value with
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-guest_x86_contexth).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_x86_guest_vm.md b/libsel4vm/docs/libsel4vm_x86_guest_vm.md
new file mode 100644
index 0000000..6108666
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_x86_guest_vm.md
@@ -0,0 +1,63 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+
+
+**Structs**:
+
+> [`vm_vcpu`](#struct-vm_vcpu)
+
+> [`vm_vcpu_arch`](#struct-vm_vcpu_arch)
+
+
+## Structs
+
+The interface `guest_vm_arch.h` defines the following structs.
+
+### Struct `vm_vcpu`
+
+Structure representing x86 specific vm properties
+
+**Elements:**
+
+- `vmexit_handler {vmexit_handler_ptr}`: Set of exit handler hooks
+- `vmcall_handlers {vmcall_handler_t *}`: Set of registered vmcall handlers
+- `vmcall_num_handler {unsigned int}`: Total number of registered vmcall handlers
+- `guest_pd {uintptr_t}`: Guest physical address of where we built the vm's page directory
+- `unhandled_ioport_callback {unhandled_ioport_callback_fn}`: A callback for processing unhandled ioport faults
+- `unhandled_ioport_callback_cookie {void *}`: A cookie to supply to the ioport callback
+- `ioport_list {vm_io_port_list_t}`: List of registered ioport handlers
+- `i8259_gs {i8259_t *}`: PIC machine state
+
+Back to [interface description](#module-guest_vm_archh).
+
+### Struct `vm_vcpu_arch`
+
+Structure representing x86 specific vcpu properties
+
+**Elements:**
+
+- `guest_state {guest_state_t *}`: Current VCPU State
+- `lapic {vm_lapic_t *}`: VM local apic
+
+Back to [interface description](#module-guest_vm_archh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_x86_ioports.md b/libsel4vm/docs/libsel4vm_x86_ioports.md
new file mode 100644
index 0000000..44939ba
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_x86_ioports.md
@@ -0,0 +1,83 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_io_port_add_handler(vm, ioport_range, ioport_interface)`](#function-vm_io_port_add_handlervm-ioport_range-ioport_interface)
+
+> [`vm_register_unhandled_ioport_callback(vm, ioport_callback, cookie)`](#function-vm_register_unhandled_ioport_callbackvm-ioport_callback-cookie)
+
+> [`vm_enable_passthrough_ioport(vcpu, port_start, port_end)`](#function-vm_enable_passthrough_ioportvcpu-port_start-port_end)
+
+
+## Functions
+
+The interface `ioports.h` defines the following functions.
+
+### Function `vm_io_port_add_handler(vm, ioport_range, ioport_interface)`
+
+Add an io port range for emulation
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `ioport_range {vm_ioport_range_t}`: Range of ioport being emulated with the given handler
+- `ioport_interface {vm_ioport_interface_t}`: Interface for ioport range, containing io_in and io_out handler functions
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-ioportsh).
+
+### Function `vm_register_unhandled_ioport_callback(vm, ioport_callback, cookie)`
+
+Register a callback for processing unhandled ioport faults (faults unknown to libsel4vm)
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `ioport_callback {unhandled_ioport_callback_fn}`: A user supplied callback to process unhandled ioport faults
+- `cookie {void *}`: A cookie to supply to the callback
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-ioportsh).
+
+### Function `vm_enable_passthrough_ioport(vcpu, port_start, port_end)`
+
+Enable the passing-through of specific ioport ranges to the VM
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to the VCPU being given ioport passthrough access
+- `port_start {uint16_t}`: Base address of ioport
+- `port_end {uint16_t}`: End address of ioport
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-ioportsh).
+
+
+Back to [top](#).
+
diff --git a/libsel4vm/docs/libsel4vm_x86_vmcall.md b/libsel4vm/docs/libsel4vm_x86_vmcall.md
new file mode 100644
index 0000000..16861e3
--- /dev/null
+++ b/libsel4vm/docs/libsel4vm_x86_vmcall.md
@@ -0,0 +1,49 @@
+<!--
+     Copyright 2020, Data61
+     Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+     ABN 41 687 119 230.
+
+     This software may be distributed and modified according to the terms of
+     the BSD 2-Clause license. Note that NO WARRANTY is provided.
+     See "LICENSE_BSD2.txt" for details.
+
+     @TAG(DATA61_BSD)
+-->
+
+## Interface `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.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_reg_new_vmcall_handler(vm, func, token)`](#function-vm_reg_new_vmcall_handlervm-func-token)
+
+
+## Functions
+
+The interface `vmcall.h` defines the following functions.
+
+### 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.
+This being matched with the value found in the vcpu EAX register on a vmcall exception
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `func {vmcall_handler}`: A handler function for the given vmcall being registered
+- `token {int}`: A token to associate with a vmcall handler.
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-vmcallh).
+
+
+Back to [top](#).
+