libsel4vmmplatsupport: Markdown docs

This commit introduces a series of markdown files documenting the
libsel4vmmplatsupport interface. These are generated out of the
interface comments, offering an alternative method to navigate and
read the libsel4vmmplatsupport documentation.

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_ac_device.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_ac_device.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_ac_device.md
new file mode 100644
index 0000000..5fb11df
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_ac_device.md
@@ -0,0 +1,60 @@
+<!--
+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 `ac_device.h`
+
+The ARM access control device interface facilitates the creation of generic virtual devices in a VM instance with
+access control permissions over the devices addressable memory. An access controlled device is often used to abstract
+the memory of a specific platform hardware device e.g a clock device. This allows the user to present hardware devices
+to a VM instance but limit their permissions with regards to modifying its register state.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_install_generic_ac_device(vm, d, mask, size, action)`](#function-vm_install_generic_ac_devicevm-d-mask-size-action)
+
+
+## Functions
+
+The interface `ac_device.h` defines the following functions.
+
+### Function `vm_install_generic_ac_device(vm, d, mask, size, action)`
+
+Installs a generic access controlled device
+are modifiable by the guest.
+'1' represents bits that the guest can read and write
+                                            '0' represents bits that can only be read by the guest
+Underlying memory for the mask should remain accessible for
+the life of this device. The mask may be updated at run time
+on demand.
+cases where the underlying device does not occupy a full
+page. If an access lies outside of the range of the mask,
+guest access.
+
+**Parameters:**
+
+- `vm {vm_t *}`: The VM to install the device into
+- `d {const struct device *}`: A description of the device to install
+- `mask {void *}`: An access mask. The mask provides a map of device bits that
+- `size {size_t}`: The size of the mask. This is useful for conserving memory in
+- `action {enum vacdev_action}`: Action to take when access is violated.
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-ac_deviceh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_generic_forward_device.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_generic_forward_device.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_generic_forward_device.md
new file mode 100644
index 0000000..01686c1
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_generic_forward_device.md
@@ -0,0 +1,72 @@
+<!--
+     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 `generic_forward_device.h`
+
+This interface facilitates the creation of a virtual device used for
+dispatching faults to external handlers. For example when using CAmkES,
+a device frame for a real device can be given to a different CAmkES component
+and this virtual device will forward read and write faults over a CAmkES
+interface so the component can perform or emulate the actions.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_install_generic_forward_device(vm, d, cfg)`](#function-vm_install_generic_forward_devicevm-d-cfg)
+
+
+
+**Structs**:
+
+> [`generic_forward_cfg`](#struct-generic_forward_cfg)
+
+
+## Functions
+
+The interface `generic_forward_device.h` defines the following functions.
+
+### Function `vm_install_generic_forward_device(vm, d, cfg)`
+
+Install the virtual forwarding device into a VM instance
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `Virtual {const struct device *}`: device being forwarded
+- `Interface {struct generic_forward_cfg}`: for forwarding the devices read and write faults
+
+**Returns:**
+
+- -1 for error, otherwise 0 for success
+
+Back to [interface description](#module-generic_forward_deviceh).
+
+
+## Structs
+
+The interface `generic_forward_device.h` defines the following structs.
+
+### Struct `generic_forward_cfg`
+
+Interface for forwarding read and write faults
+
+**Elements:**
+
+- `write_fn {forward_write_fn}`: A callback for forwarding write faults
+- `read_fn {forward_read_fn}`: A callback for forwarding read faults
+
+Back to [interface description](#module-generic_forward_deviceh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_boot_init.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_boot_init.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_boot_init.md
new file mode 100644
index 0000000..8b5db05
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_boot_init.md
@@ -0,0 +1,52 @@
+<!--
+     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_boot_init.h`
+
+The libsel4vmmplatsupport arm guest boot init interface provides helpers to initialise the booting state of
+a VM instance. This currently only targets booting a Linux guest OS.
+
+### Brief content:
+
+**Functions**:
+
+> [`vcpu_set_bootargs(vcpu, pc, mach_type, atags)`](#function-vcpu_set_bootargsvcpu-pc-mach_type-atags)
+
+
+## Functions
+
+The interface `guest_boot_init.h` defines the following functions.
+
+### Function `vcpu_set_bootargs(vcpu, pc, mach_type, atags)`
+
+Set the boot args and pc for the VM.
+For linux:
+r0 -> 0
+r1 -> MACH_TYPE  (e.g #4151 for EXYNOS5410 eval. platform smdk5410)
+r2 -> atags/dtb address
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to the boot VCPU
+- `pc {seL4_Word}`: The initial PC for the VM
+- `mach_type {seL4_Word}`: Linux specific machine ID see http://www.arm.linux.org.uk/developer/machines/
+- `atags {seL4_Word}`: Linux specific IPA of atags. Can also be substituted with dtb address
+
+**Returns:**
+
+- 0 on success, otherwise -1 for failure
+
+Back to [interface description](#module-guest_boot_inith).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_reboot.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_reboot.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_reboot.md
new file mode 100644
index 0000000..4d6cc04
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_reboot.md
@@ -0,0 +1,116 @@
+<!--
+     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_reboot.h`
+
+The guest reboot interface provides a series of helpers for registering callbacks when rebooting the VMM.
+This interface giving various VMM components and drivers the ability to reset necessary state on a reboot.
+
+### Brief content:
+
+**Functions**:
+
+> [`vmm_init_reboot_hooks_list(rb_hooks_list)`](#function-vmm_init_reboot_hooks_listrb_hooks_list)
+
+> [`vmm_register_reboot_callback(rb_hooks_list, hook, token)`](#function-vmm_register_reboot_callbackrb_hooks_list-hook-token)
+
+> [`vmm_process_reboot_callbacks(vm, rb_hooks_list)`](#function-vmm_process_reboot_callbacksvm-rb_hooks_list)
+
+
+
+**Structs**:
+
+> [`reboot_hook`](#struct-reboot_hook)
+
+> [`reboot_hooks_list`](#struct-reboot_hooks_list)
+
+
+## Functions
+
+The interface `guest_reboot.h` defines the following functions.
+
+### Function `vmm_init_reboot_hooks_list(rb_hooks_list)`
+
+Initialise state of a given reboot hooks list
+
+**Parameters:**
+
+- `rb_hooks_list {reboot_hooks_list_t *}`: Handle to reboot hooks list
+
+**Returns:**
+
+- 0 for success, otherwise -1 for error
+
+Back to [interface description](#module-guest_rebooth).
+
+### Function `vmm_register_reboot_callback(rb_hooks_list, hook, token)`
+
+Register a reboot callback within a given reboot hooks list
+
+**Parameters:**
+
+- `rb_hooks_list {reboot_hooks_list_t *}`: Handle to reboot hooks list
+- `hook {rb_hook_fn}`: Reboot callback to be invoked when list is processed
+- `token {void *}`: Cookie passed to reboot callback when invoked
+
+**Returns:**
+
+- 0 for success, otherwise -1 for error
+
+Back to [interface description](#module-guest_rebooth).
+
+### Function `vmm_process_reboot_callbacks(vm, rb_hooks_list)`
+
+Process the reboot hooks registered in a reboot hooks list
+
+**Parameters:**
+
+- `vm {vm_t *}`: Handle to vm - passed onto reboot callback
+- `rb_hooks_list {reboot_hooks_list_t *}`: Handle to reboot hooks list
+
+**Returns:**
+
+- 0 for success, otherwise -1 for error
+
+Back to [interface description](#module-guest_rebooth).
+
+
+## Structs
+
+The interface `guest_reboot.h` defines the following structs.
+
+### Struct `reboot_hook`
+
+Datastructure representing a reboot hook, containing a callback function to invoke when processing the
+hook
+
+**Elements:**
+
+- `fn {reboot_hook_fn}`: Function pointer to reboot callback
+- `token {void *}`: Cookie passed to reboot callback when invoked
+
+Back to [interface description](#module-guest_rebooth).
+
+### Struct `reboot_hooks_list`
+
+Reboot hooks management datastructure. Contains a list of reboot hooks that a VMM registers
+
+**Elements:**
+
+- `rb_hooks {reboot_hook_t *}`: List of reboot hooks
+- `nhooks {size_t}`: Number of reboot hooks in `rb_hooks` member
+
+Back to [interface description](#module-guest_rebooth).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_fault.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_fault.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_fault.md
new file mode 100644
index 0000000..dac885d
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_fault.md
@@ -0,0 +1,66 @@
+<!--
+     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 arm guest vcpu fault interface provides a module for registering
+and processing vcpu faults. The module can be used such that it directly hooks
+into an ARM VMMs unhandled vcpu callback interface or wrapped over by another driver. This
+module particularly provides useful handlers to vcpu faults relating to SMC and MSR/MRS instructions.
+
+### Brief content:
+
+**Functions**:
+
+> [`vmm_handle_arm_vcpu_exception(vcpu, hsr, cookie)`](#function-vmm_handle_arm_vcpu_exceptionvcpu-hsr-cookie)
+
+> [`register_arm_vcpu_exception_handler(ec_class, exception_handler)`](#function-register_arm_vcpu_exception_handlerec_class-exception_handler)
+
+
+## Functions
+
+The interface `guest_vcpu_fault.h` defines the following functions.
+
+### Function `vmm_handle_arm_vcpu_exception(vcpu, hsr, cookie)`
+
+Handle a vcpu exception given the HSR value - Syndrome information
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to the faulting VCPU
+- `hsr {uint32_t }`: Syndrome information value describing the exception/fault
+- `cookie {void *}`: User supplied cookie to pass onto exception
+
+**Returns:**
+
+- -1 on error, otherwise 0 for success
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+### Function `register_arm_vcpu_exception_handler(ec_class, exception_handler)`
+
+Register a handler to a vcpu exception class
+
+**Parameters:**
+
+- `ec_class {uint32_t}`: The exception class the handler will be called on
+- `exception_handler {vcpu_exception_handler_fn}`: Function pointer to the exception handler
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-guest_vcpu_faulth).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_util.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_util.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_util.md
new file mode 100644
index 0000000..2a103d1
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_guest_vcpu_util.md
@@ -0,0 +1,46 @@
+<!--
+     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_util.h`
+
+The ARM guest vcpu util interface provides abstractions and helpers for managing libsel4vm vcpus on an ARM platform.
+
+### Brief content:
+
+**Functions**:
+
+> [`fdt_generate_plat_vcpu_node(vm, fdt)`](#function-fdt_generate_plat_vcpu_nodevm-fdt)
+
+
+## Functions
+
+The interface `guest_vcpu_util.h` defines the following functions.
+
+### Function `fdt_generate_plat_vcpu_node(vm, fdt)`
+
+Generate a CPU device node for a given fdt. This taking into account
+the vcpus created for the VM.
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `fdt {void *}`: FDT blob to append generated device node
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-guest_vcpu_utilh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vpci.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vpci.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vpci.md
new file mode 100644
index 0000000..6330b1d
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vpci.md
@@ -0,0 +1,69 @@
+<!--
+     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 `vpci.h`
+
+The libsel4vmmplatsupport vpci interface presents a Virtual PCI driver for ARM-based VM's.
+Using the `vmm_pci_space_t` management interface, the vpci driver establishes the configuration
+space in the guest VM. The driver also handles and processes all subsequent memory and ioport accesses to the
+virtual pci device.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_install_vpci(vm, io_port, pci)`](#function-vm_install_vpcivm-io_port-pci)
+
+> [`fdt_generate_vpci_node(vm, pci, fdt, gic_phandle)`](#function-fdt_generate_vpci_nodevm-pci-fdt-gic_phandle)
+
+
+## Functions
+
+The interface `vpci.h` defines the following functions.
+
+### Function `vm_install_vpci(vm, io_port, pci)`
+
+
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `io_port {vmm_io_port_list_t *}`: IOPort library instance to emulate io accesses with
+- `pci {vmm_pci_space_t }`: PCI library instance to emulate PCI device accesses with
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-vpcih).
+
+### Function `fdt_generate_vpci_node(vm, pci, fdt, gic_phandle)`
+
+Generate a PCI device node for a given fdt. This taking into account
+the virtual PCI device configuration space.
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `PCI {vmm_pci_space_t *}`: library instance to generate fdt node
+- `fdt {void *}`: FDT blob to append generated device node
+- `gic_phandle {int}`: Phandle of IRQ controller to generate a correct interrupt map property
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-vpcih).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vusb.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vusb.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vusb.md
new file mode 100644
index 0000000..09a6f58
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_arm_vusb.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 `vusb.h`
+
+The libsel4vmmplatsupport vusb interface presents a Virtual USB driver for ARM-based VM's.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_install_vusb(vm, hcd, pbase, virq, vmm_ncap, vm_ncap, badge)`](#function-vm_install_vusbvm-hcd-pbase-virq-vmm_ncap-vm_ncap-badge)
+
+> [`vm_vusb_notify(vusb)`](#function-vm_vusb_notifyvusb)
+
+
+## Functions
+
+The interface `vusb.h` defines the following functions.
+
+### Function `vm_install_vusb(vm, hcd, pbase, virq, vmm_ncap, vm_ncap, badge)`
+
+Install a virtual usb device
+Calls made to this hcd may be redirected for filtering.
+
+**Parameters:**
+
+- `vm {vm_t *}`: The VM in which to install the device
+- `hcd {usb_host_t *}`: The USB host controller that should be used for USB transactions.
+- `pbase {uintptr_t}`: The guest physical address of the device (2 pages)
+- `virq {int}`: The virtual IRQ number for this device
+- `vmm_ncap {seL4_CPtr}`: The capability to the endpoint at which the VMM waits for notifications.
+- `vm_ncap {seL4_CPtr}`: The index at which to install a notification capability into the VM
+- `badge {int}`: The seL4 badge which should be applied to the notification capability.
+
+**Returns:**
+
+- A handle to the virtual usb device, or NULL on failure
+
+Back to [interface description](#module-vusbh).
+
+### Function `vm_vusb_notify(vusb)`
+
+This function should be called when a notification is received from the
+VM. The notification is identifyable by a message on the fault endpoint
+of the VM which has a badge that matches that which was passed into the
+vm_install_vusb function.
+
+**Parameters:**
+
+- `vusb {vusb_device_t *}`: A handle to a virtual usb device
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-vusbh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_cross_vm_connection.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_cross_vm_connection.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_cross_vm_connection.md
new file mode 100644
index 0000000..a4befd9
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_cross_vm_connection.md
@@ -0,0 +1,110 @@
+<!--
+     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 `cross_vm_connection.h`
+
+The crossvm connection module facilitates the creation of communication channels between VM's and other
+components on a seL4-based system. The module exports registered cross vm connections to a Linux VM such that
+processes can access them from userlevel. This being facilitated over a virtual PCI device.
+
+### Brief content:
+
+**Functions**:
+
+> [`cross_vm_connections_init_common(vm, connection_base_addr, connections, num_connections, pci, alloc_irq)`](#function-cross_vm_connections_init_commonvm-connection_base_addr-connections-num_connections-pci-alloc_irq)
+
+> [`consume_connection_event(vm, event_id, inject_irq)`](#function-consume_connection_eventvm-event_id-inject_irq)
+
+
+
+**Structs**:
+
+> [`crossvm_dataport_handle`](#struct-crossvm_dataport_handle)
+
+> [`crossvm_handle`](#struct-crossvm_handle)
+
+
+## Functions
+
+The interface `cross_vm_connection.h` defines the following functions.
+
+### Function `cross_vm_connections_init_common(vm, connection_base_addr, connections, num_connections, pci, alloc_irq)`
+
+Install a set of cross vm connections into a guest VM (for either x86 or ARM VM platforms)
+for the crossvm connectors
+PCI device
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `connection_base_addr {uintptr_t}`: The base guest physical address that can be used to reserve memory
+- `connections {crossvm_handle_t *}`: The set of crossvm connections to be initialised and installed in the guest
+- `num_connection {int}`: The number of connections passed in through the 'connections' parameter
+- `pci {vmm_pci_space_t *}`: A handle to the VM's host PCI device. The connections are advertised through the
+- `alloc_irq {alloc_free_interrupt_fn}`: A function that is used to allocated an irq number for the crossvm connections
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-cross_vm_connectionh).
+
+### Function `consume_connection_event(vm, event_id, inject_irq)`
+
+Handler to consume a cross vm connection event. This being called by the VMM when it recieves a notification from an
+external process. The event is then relayed onto the VM.
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `event_id {seL4_Word}`: The id that corresponds to the occuring event
+- `inject_irq {bool}`: Whether to inject an interrupt into the VM
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-cross_vm_connectionh).
+
+
+## Structs
+
+The interface `cross_vm_connection.h` defines the following structs.
+
+### Struct `crossvm_dataport_handle`
+
+Datastructure representing a dataport of a crossvm connection
+
+**Elements:**
+
+- `size {size_t}`: The size of the crossvm dataport
+- `num_frames {int}`: Total number of frames in the `frames` member
+- `frames {seL4_CPtr *}`: The set of frames backing the dataport
+
+Back to [interface description](#module-cross_vm_connectionh).
+
+### Struct `crossvm_handle`
+
+Datastructure representing a single crossvm connection
+This is matched on when invoking `consume_connection_event`
+
+**Elements:**
+
+- `dataport {crossvm_dataport_handle_t *}`: The dataport associated with the crossvm connection
+- `emit_fn {emit_fn}`: The function pointer to the crossvm emit method
+- `consume_id {seL4_Word}`: The identifier used for the crossvm connection when receiving incoming notifications
+
+Back to [interface description](#module-cross_vm_connectionh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device.md
new file mode 100644
index 0000000..f36acc1
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device.md
@@ -0,0 +1,117 @@
+<!--
+     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 `device.h`
+
+The device.h interface provides a series of datastructures and helpers to manage VMM devices.
+
+### Brief content:
+
+**Functions**:
+
+> [`device_list_init(list)`](#function-device_list_initlist)
+
+> [`add_device(dev_list, d)`](#function-add_devicedev_list-d)
+
+> [`find_device_by_pa(dev_list, addr)`](#function-find_device_by_padev_list-addr)
+
+
+
+**Structs**:
+
+> [`device`](#struct-device)
+
+> [`device_list`](#struct-device_list)
+
+
+## Functions
+
+The interface `device.h` defines the following functions.
+
+### Function `device_list_init(list)`
+
+Initialise an empty device list
+
+**Parameters:**
+
+- `list {device_list_t *}`: device list to initialise
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-deviceh).
+
+### Function `add_device(dev_list, d)`
+
+Add a generic device to a given device list without performing any initialisation of the device
+
+**Parameters:**
+
+- `dev_list {device_list_t *}`: A handle to the device list that the device should be installed into
+- `device {const struct device *}`: A description of the device
+
+**Returns:**
+
+- 0 on success, otherwise -1 for error
+
+Back to [interface description](#module-deviceh).
+
+### Function `find_device_by_pa(dev_list, addr)`
+
+Find a device by a given addr within a device list
+
+**Parameters:**
+
+- `dev_list {device_list_t *}`: Device list to search within
+- `addr {uintptr_t}`: Add to search with
+
+**Returns:**
+
+- Pointer to device if found, otherwise NULL if not found
+
+Back to [interface description](#module-deviceh).
+
+
+## Structs
+
+The interface `device.h` defines the following structs.
+
+### Struct `device`
+
+Device Management Object
+
+
+**Elements:**
+
+- `name {const char *}`: A string representation of the device. Useful for debugging
+- `pstart {seL4_Word}`: The physical address of the device
+- `size {seL4_Word}`: Device mapping size
+- `handle_device_fault {int *(vm_t, vm_vcpu_t, dev, addr, len)}`: Fault handler
+- `priv {void *}`: Device emulation private data
+
+Back to [interface description](#module-deviceh).
+
+### Struct `device_list`
+
+Management for a list of devices
+
+**Elements:**
+
+- `devices {struct device *}`: List of registered devices
+- `num_devices {int}`: Total number of registered devices
+
+Back to [interface description](#module-deviceh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device_utils.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device_utils.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device_utils.md
new file mode 100644
index 0000000..cb406ab
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_device_utils.md
@@ -0,0 +1,80 @@
+<!--
+     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 `device_utils.h`
+
+The device utils interface provides various helpers to establish different types devices for a given VM
+instance.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_install_passthrough_device(vm, device)`](#function-vm_install_passthrough_devicevm-device)
+
+> [`vm_install_ram_only_device(vm, device)`](#function-vm_install_ram_only_devicevm-device)
+
+> [`vm_install_listening_device(vm, device)`](#function-vm_install_listening_devicevm-device)
+
+
+## Functions
+
+The interface `device_utils.h` defines the following functions.
+
+### Function `vm_install_passthrough_device(vm, device)`
+
+Install a passthrough device into a VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM that the device should be install to
+- `device {const struct device *}`: A description of the device
+
+**Returns:**
+
+- 0 on success, -1 for error
+
+Back to [interface description](#module-device_utilsh).
+
+### Function `vm_install_ram_only_device(vm, device)`
+
+Install a device backed by ram into a VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM that the device should be install to
+- `device {const struct device *}`: A description of the device
+
+**Returns:**
+
+- 0 on success, -1 for error
+
+Back to [interface description](#module-device_utilsh).
+
+### Function `vm_install_listening_device(vm, device)`
+
+Install a passthrough device into a VM, but trap and print all access
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM that the device should be install to
+- `device {const struct device *}`: A description of the device
+
+**Returns:**
+
+- 0 on success, -1 for error
+
+Back to [interface description](#module-device_utilsh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_image.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_image.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_image.md
new file mode 100644
index 0000000..2caea09
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_image.md
@@ -0,0 +1,105 @@
+<!--
+     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_image.h`
+
+The guest image interface provides general utilites to load guest vm images (e.g. kernel, initrd, modules).
+This interface probably stops being relevant/useful after we start running a VM instance.
+
+### Brief content:
+
+**Functions**:
+
+> [`vm_load_guest_kernel(vm, kernel_name, load_address, alignment, guest_kernel_image)`](#function-vm_load_guest_kernelvm-kernel_name-load_address-alignment-guest_kernel_image)
+
+> [`vm_load_guest_module(vm, module_name, load_address, alignment, guest_image)`](#function-vm_load_guest_modulevm-module_name-load_address-alignment-guest_image)
+
+
+
+**Structs**:
+
+> [`guest_image`](#struct-guest_image)
+
+> [`guest_kernel_image`](#struct-guest_kernel_image)
+
+
+## Functions
+
+The interface `guest_image.h` defines the following functions.
+
+### Function `vm_load_guest_kernel(vm, kernel_name, load_address, alignment, guest_kernel_image)`
+
+Load guest kernel image
+
+**Parameters:**
+
+- `vm {vm_t *}`: Handle to the VM
+- `kernel_name {const char *}`: Name of the kernel image
+- `load_address {uintptr_t}`: Address to load guest kernel image at
+- `alignment {size_t}`: Alignment for loading kernel image
+- `guest_kernel_image {guest_kernel_image_t *}`: Handle to information regarding the resulted loading of the guest kernel image
+
+**Returns:**
+
+- 0 on success, otherwise -1 on error
+
+Back to [interface description](#module-guest_imageh).
+
+### Function `vm_load_guest_module(vm, module_name, load_address, alignment, guest_image)`
+
+Load guest kernel module e.g. initrd
+
+**Parameters:**
+
+- `vm {vm_t *}`: Handle to the VM
+- `module_name {const char *}`: Name of the module image
+- `load_address {uintptr_t}`: Address to load guest kernel image at
+- `alignment {size_t}`: Alignment for loading module image
+- `guest_image {guest_image_t *}`: Handle to information regarding the resulted loading of the guest module image
+
+**Returns:**
+
+- 0 on success, otherwise -1 on error
+
+Back to [interface description](#module-guest_imageh).
+
+
+## Structs
+
+The interface `guest_image.h` defines the following structs.
+
+### Struct `guest_image`
+
+General datastructure for managing a guest image
+
+**Elements:**
+
+- `load_paddr {uintptr_t}`: Base address (in guest physical) where the image was loaded
+- `alignment {size_t}`: Alignment we used when loading the image
+- `size {size_t}`: Size of guest image
+
+Back to [interface description](#module-guest_imageh).
+
+### Struct `guest_kernel_image`
+
+Stores information about the guest kernel image we are loading.
+
+**Elements:**
+
+- `kernel_image {guest_image_t}`: Datastructure referring to guest kernel image
+- `kernel_image_arch {guest_kernel_image_arch_t}`: Architecture specific information for loaded guest image
+
+Back to [interface description](#module-guest_imageh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_memory_util.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_memory_util.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_memory_util.md
new file mode 100644
index 0000000..44d5d72
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_memory_util.md
@@ -0,0 +1,138 @@
+<!--
+     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_util.h`
+
+The guest memory util interface provides various utilities and helpers for using the libsel4vm guest memory
+interface. The methods in the interface cover common usage patterns when managing memory for a VM instance.
+
+### Brief content:
+
+**Functions**:
+
+> [`create_allocated_reservation_frame(vm, addr, rights, alloc_fault_callback, alloc_fault_cookie)`](#function-create_allocated_reservation_framevm-addr-rights-alloc_fault_callback-alloc_fault_cookie)
+
+> [`create_device_reservation_frame(vm, addr, rights, fault_callback, fault_cookie)`](#function-create_device_reservation_framevm-addr-rights-fault_callback-fault_cookie)
+
+> [`map_ut_alloc_reservation_with_base_paddr(vm, paddr, reservation)`](#function-map_ut_alloc_reservation_with_base_paddrvm-paddr-reservation)
+
+> [`map_ut_alloc_reservation(vm, reservation)`](#function-map_ut_alloc_reservationvm-reservation)
+
+> [`map_frame_alloc_reservation(vm, reservation)`](#function-map_frame_alloc_reservationvm-reservation)
+
+> [`map_maybe_device_reservation(vm, reservation)`](#function-map_maybe_device_reservationvm-reservation)
+
+
+## Functions
+
+The interface `guest_memory_util.h` defines the following functions.
+
+### Function `create_allocated_reservation_frame(vm, addr, rights, alloc_fault_callback, alloc_fault_cookie)`
+
+Create and map a reservation for a vka allocated frame. The allocated frame is mapped in both the vm and vmm vspace
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `addr {uintptr_t}`: Address of emulated frame
+- `rights {seL4_CapRights_t}`: Rights for mapping the allocated frame into the vm's vspace
+- `alloc_fault_callback {memory_fault_callback_fn}`: Fault callback for allocated frame
+- `alloc_fault_cookie {void *}`: Cookie for fault callback
+
+**Returns:**
+
+- Address of allocated frame in vmm vspace
+
+Back to [interface description](#module-guest_memory_utilh).
+
+### Function `create_device_reservation_frame(vm, addr, rights, fault_callback, fault_cookie)`
+
+Create and map a reservation for a device frame. The device frame is mapped in both the vm and vmm vspace
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `addr {uintptr_t}`: Address of emulated frame
+- `rights {seL4_CapRights_t}`: Rights for mapping the device frame into the vm's vspace
+- `fault_callback {memory_fault_callback_fn}`: Fault callback for the frame
+- `fault_cookie {void *}`: Cookie for fault callback
+
+**Returns:**
+
+- Address of device frame in vmm vspace
+
+Back to [interface description](#module-guest_memory_utilh).
+
+### Function `map_ut_alloc_reservation_with_base_paddr(vm, paddr, reservation)`
+
+Map a guest reservation backed with untyped frames allocated from a base paddr
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `paddr {uintptr_t}`: Base paddr to allocate from
+- `reservation {vm_memory_reservation_t *}`: Pointer to reservation object being mapped
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-guest_memory_utilh).
+
+### Function `map_ut_alloc_reservation(vm, reservation)`
+
+Map a guest reservation backed with untyped frames
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `reservation {vm_memory_reservation_t *}`: Pointer to reservation object being mapped
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-guest_memory_utilh).
+
+### Function `map_frame_alloc_reservation(vm, reservation)`
+
+Map a guest reservation backed with free vka frames
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `reservation {vm_memory_reservation_t *}`: Pointer to reservation object being mapped
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-guest_memory_utilh).
+
+### Function `map_maybe_device_reservation(vm, reservation)`
+
+Map a guest reservation backed with device frames
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `reservation {vm_memory_reservation_t *}`: Pointer to reservation object being mapped
+
+**Returns:**
+
+- -1 on failure otherwise 0 for success
+
+Back to [interface description](#module-guest_memory_utilh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_vcpu_util.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_vcpu_util.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_vcpu_util.md
new file mode 100644
index 0000000..681c1cc
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_guest_vcpu_util.md
@@ -0,0 +1,46 @@
+<!--
+     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_util.h`
+
+The guest vcpu util interface provides abstractions and helpers for managing libsel4vm vcpus.
+
+### Brief content:
+
+**Functions**:
+
+> [`create_vmm_plat_vcpu(vm, priority)`](#function-create_vmm_plat_vcpuvm-priority)
+
+
+## Functions
+
+The interface `guest_vcpu_util.h` defines the following functions.
+
+### Function `create_vmm_plat_vcpu(vm, priority)`
+
+Create a new platform vcpu. This is a wrapper around the libsel4vm function `vm_create_vcpu` however
+further intialises and configures the vcpu with platform specific attributes
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `priority {int}`: Priority of the new vcpu thread
+
+**Returns:**
+
+- NULL for error, otherwise pointer to created vm_vcpu_t object
+
+Back to [interface description](#module-guest_vcpu_utilh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_ioports.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_ioports.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_ioports.md
new file mode 100644
index 0000000..dcef455
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_ioports.md
@@ -0,0 +1,153 @@
+<!--
+     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 ioports interface provides a useful abstraction for initialising, registering and handling ioport events
+for a guest VM instance. This is independent from the x86 libsel4vm ioports interface. This interface is intended
+to be more generic and architecture independent, useful for usecases that require ioports without architecture
+support (virtio PCI).
+
+### Brief content:
+
+**Functions**:
+
+> [`vmm_io_port_init(io_list, ioport_alloc_addr)`](#function-vmm_io_port_initio_list-ioport_alloc_addr)
+
+> [`vmm_io_port_add_handler(io_list, ioport_range, ioport_interface, port_type)`](#function-vmm_io_port_add_handlerio_list-ioport_range-ioport_interface-port_type)
+
+> [`emulate_io_handler(io_port, port_no, is_in, size, data)`](#function-emulate_io_handlerio_port-port_no-is_in-size-data)
+
+
+
+**Structs**:
+
+> [`ioport_range`](#struct-ioport_range)
+
+> [`ioport_interface`](#struct-ioport_interface)
+
+> [`ioport_entry`](#struct-ioport_entry)
+
+> [`vmm_io_list`](#struct-vmm_io_list)
+
+
+## Functions
+
+The interface `ioports.h` defines the following functions.
+
+### Function `vmm_io_port_init(io_list, ioport_alloc_addr)`
+
+Initialize the io port list manager.
+This is used when registering ioport handlers of type 'IOPORT_FREE'
+
+**Parameters:**
+
+- `io_list {vmm_io_port_list_t **}`: Pointer to io_port list handle. This will be allocated and initialised
+- `ioport_alloc_addr {uint16_t}`: Base ioport address we can safely bump allocate from (doesn't conflict with other ioports).
+
+**Returns:**
+
+- 0 for success, otherwise -1 for error
+
+Back to [interface description](#module-ioportsh).
+
+### Function `vmm_io_port_add_handler(io_list, ioport_range, ioport_interface, port_type)`
+
+Add an io port range for emulation
+
+**Parameters:**
+
+- `io_list {vmm_io_port_list_t *}`: Handle to ioport list. This is where the new ioport handler will be appended to
+- `ioport_range {ioport_range_t}`: Range the ioport handler will emulate
+- `ioport_interface {ioport_interface_t}`: IOPort emulation interface
+- `port_type {ioport_type_t}`: The type of ioport being registered - IOPORT_FREE, IOPORT_ADDR
+
+**Returns:**
+
+- NULL for error, otherwise pointer to newly created ioport entry
+
+Back to [interface description](#module-ioportsh).
+
+### Function `emulate_io_handler(io_port, port_no, is_in, size, data)`
+
+From a set of registered ioports, emulate an io instruction given a current ioport access.
+
+**Parameters:**
+
+- `io_port {vmm_io_port_list_t *}`: List of registered ioports with in/out handlers
+- `port_no {unsigned int}`: IOPort address being accessed
+- `is_in {bool}`: True if we are performing an io in operation, otherwise False
+- `size {size_t}`: Size of io access
+- `data {unsigned int *}`: Pointer with the data being written if io-out op, otherwise will be populated with data from an io-in op
+
+**Returns:**
+
+- 0 if handled, 1 if unhandled, otherwise -1 for error
+
+Back to [interface description](#module-ioportsh).
+
+
+## Structs
+
+The interface `ioports.h` defines the following structs.
+
+### Struct `ioport_range`
+
+Range of ioport handler
+
+**Elements:**
+
+- `start {uint16_t}`: Start address of ioport range
+- `end {uint16_t}`: End address of ioport range
+- `size {uint16_t}`: Size of ioport range
+
+Back to [interface description](#module-ioportsh).
+
+### Struct `ioport_interface`
+
+Datastructure used for ioport emulation, containing handlers for the ioport range
+
+**Elements:**
+
+- `cookie {void *}`: User supplied cookie to pass onto handlers
+- `port_in {ioport_in_fn}`: IO in operation handler
+- `port_out {ioport_out_fn}`: IO out operation handler
+- `desc {const char *}`: IOPort description, useful for debugging
+
+Back to [interface description](#module-ioportsh).
+
+### Struct `ioport_entry`
+
+Datastructure used to present a registered ioport range
+
+**Elements:**
+
+- `range {ioport_range_t}`: IO address range of ioport entry
+- `interface {ioport_interface_t}`: Emulation interface for ioport range
+
+Back to [interface description](#module-ioportsh).
+
+### Struct `vmm_io_list`
+
+Parent datastructure used to maintain a list of registered ioports
+
+**Elements:**
+
+- `num_ioports {int}`: Total number of registered ioports
+- `List {ioport_entry_t **}`: of registered ioport objects
+- `alloc_addr {uint16_t}`: Base ioport address we can safely bump allocate from, used when registering ioport handlers of type 'IOPORT_FREE'
+
+Back to [interface description](#module-ioportsh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci.md
new file mode 100644
index 0000000..b9881a8
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci.md
@@ -0,0 +1,149 @@
+<!--
+     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 `pci.h`
+
+This interface presents a VMM PCI Driver. This manages the host's PCI devices, and handles guest OS PCI config space
+read & writes.
+
+### Brief content:
+
+**Functions**:
+
+> [`vmm_pci_init(space)`](#function-vmm_pci_initspace)
+
+> [`vmm_pci_add_entry(space, entry, addr)`](#function-vmm_pci_add_entryspace-entry-addr)
+
+> [`make_addr_reg_from_config(conf, addr, reg)`](#function-make_addr_reg_from_configconf-addr-reg)
+
+> [`find_device(self, addr)`](#function-find_deviceself-addr)
+
+
+
+**Structs**:
+
+> [`vmm_pci_address`](#struct-vmm_pci_address)
+
+> [`vmm_pci_entry`](#struct-vmm_pci_entry)
+
+> [`vmm_pci_sapce`](#struct-vmm_pci_sapce)
+
+
+## Functions
+
+The interface `pci.h` defines the following functions.
+
+### Function `vmm_pci_init(space)`
+
+Initialize PCI space
+
+**Parameters:**
+
+- `space {vmm_pci_space_t **}`: Pointer to PCI space being initialised
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_add_entry(space, entry, addr)`
+
+Add a PCI entry. Optionally reports where it is located
+
+**Parameters:**
+
+- `space {vmm_pci_space_t *}`: PCI space handle
+- `entry {vmm_pci_entry_t}`: PCI entry being addr
+- `addr {vmm_pci_addr_t *}`: Resulting PCI address where entry gets located
+
+**Returns:**
+
+- 0 on success, -1 on error
+
+Back to [interface description](#module-pcih).
+
+### Function `make_addr_reg_from_config(conf, addr, reg)`
+
+Convert config to pci address
+
+**Parameters:**
+
+- `conf {uint32_t}`: Configuration value to convert to pci address
+- `addr {vmm_pci_address_t *}`: Resulting PCI address
+- `reg {uint8_t *}`: Resulting register value
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-pcih).
+
+### Function `find_device(self, addr)`
+
+Find PCI device given a PCI address (Bus/Dev/Func)
+
+**Parameters:**
+
+- `self {vmm_pci_space_t *}`: PCI space handle
+- `addr {vmm_pci_address_t}`: PCI address of device
+
+**Returns:**
+
+- NULL on error, otherwise pointer to registered pci entry
+
+Back to [interface description](#module-pcih).
+
+
+## Structs
+
+The interface `pci.h` defines the following structs.
+
+### Struct `vmm_pci_address`
+
+Represents a PCI address by Bus/Device/Function
+
+**Elements:**
+
+- `bus {uint8_t}`: Bus value
+- `dev {uint8_t}`: Device value
+- `fun {uint8_t}`: Function value
+
+Back to [interface description](#module-pcih).
+
+### Struct `vmm_pci_entry`
+
+Abstracts the virtual PCI device. This is is inserted into the virtual PCI configuration space
+
+**Elements:**
+
+- `cookie {void *}`: User supplied cookie to pass onto callback functions
+- `ioread {int *(void *cookie, int offset, int size, uint32_t *result)}`: Configuration space read callback
+- `iowrite {int *(void *cookie, int offset, int size, uint32_t value)}`: Configuration space write callback
+
+Back to [interface description](#module-pcih).
+
+### Struct `vmm_pci_sapce`
+
+Represents a single host virtual PCI space
+                                        This only supports one bus at the moment.
+
+**Elements:**
+
+- `bus {vmm_pci_entry_t *}`: The PCI bus, representing 32 devices, each of which has 8 functions
+- `conf_port_addr {uint32_t}`: The current config address for IO port emulation
+
+Back to [interface description](#module-pcih).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci_helper.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci_helper.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci_helper.md
new file mode 100644
index 0000000..63bdf37
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_pci_helper.md
@@ -0,0 +1,326 @@
+<!--
+     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 `pci.h`
+
+This interface presents a series of helpers when using the VMM PCI Driver. These helpers assisting with
+the creation of pci device entries and accessors the their configuration spaces.
+
+### Brief content:
+
+**Functions**:
+
+> [`vmm_pci_entry_ignore_write(cookie, offset, size, value)`](#function-vmm_pci_entry_ignore_writecookie-offset-size-value)
+
+> [`vmm_pci_mem_device_read(cookie, offset, size, result)`](#function-vmm_pci_mem_device_readcookie-offset-size-result)
+
+> [`vmm_pci_mem_device_write(cookie, offset, size, value)`](#function-vmm_pci_mem_device_writecookie-offset-size-value)
+
+> [`define_pci_host_bridge(bridge)`](#function-define_pci_host_bridgebridge)
+
+> [`vmm_pci_create_passthrough(addr, config)`](#function-vmm_pci_create_passthroughaddr-config)
+
+> [`vmm_pci_create_bar_emulation(existing, num_bars, bars)`](#function-vmm_pci_create_bar_emulationexisting-num_bars-bars)
+
+> [`vmm_pci_create_passthrough_bar_emulation(existing, num_bars, bars)`](#function-vmm_pci_create_passthrough_bar_emulationexisting-num_bars-bars)
+
+> [`vmm_pci_create_irq_emulation(existing, irq)`](#function-vmm_pci_create_irq_emulationexisting-irq)
+
+> [`vmm_pci_create_cap_emulation(existing, num_caps, cap, num_ranges, range_starts, range_ends)`](#function-vmm_pci_create_cap_emulationexisting-num_caps-cap-num_ranges-range_starts-range_ends)
+
+
+
+**Structs**:
+
+> [`vmm_pci_device_def`](#struct-vmm_pci_device_def)
+
+> [`vmm_pci_bar`](#struct-vmm_pci_bar)
+
+> [`pci_bar_emulation`](#struct-pci_bar_emulation)
+
+> [`pci_irq_emulation`](#struct-pci_irq_emulation)
+
+> [`pci_passthrough_device`](#struct-pci_passthrough_device)
+
+> [`pci_cap_emulation`](#struct-pci_cap_emulation)
+
+
+## Functions
+
+The interface `pci.h` defines the following functions.
+
+### Function `vmm_pci_entry_ignore_write(cookie, offset, size, value)`
+
+Helper write function that just ignores any writes
+
+**Parameters:**
+
+- `cookie {void *}`: User supplied PCI entry cookie
+- `offset {int}`: Offset into PCI device header
+- `size {int}`: Size of data to be written
+- `value {uint32_t}`: value to write to PCI device header offset
+
+**Returns:**
+
+- Returns 0
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_mem_device_read(cookie, offset, size, result)`
+
+Read method for a PCI devices memory
+@result {uint32_t *} result  Resulting value read back from PCI device header
+
+**Parameters:**
+
+- `cookie {void *}`: PCI device header
+- `offset {int}`: Offset into PCI device header
+- `size {int}`: Size of data to be read
+
+**Returns:**
+
+- 0 if success, -1 if error
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_mem_device_write(cookie, offset, size, value)`
+
+Write method for a PCI devices memory
+@value {uint32_t} value      Value to write to PCI device header offset
+
+**Parameters:**
+
+- `cookie {void *}`: PCI device header
+- `offset {int}`: Offset into PCI device header
+- `size {int}`: Size of data to be read
+
+**Returns:**
+
+- 0 if success, -1 if error
+
+Back to [interface description](#module-pcih).
+
+### Function `define_pci_host_bridge(bridge)`
+
+Defines the configuration space values of the PCI host bridge
+
+**Parameters:**
+
+- `bridge {vmm_pci_device_def_t *}`: PCI bridge device definition
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_create_passthrough(addr, config)`
+
+Construct a pure passthrough device based on the real PCI. This is almost always useless as
+you will almost certainly want to rebase io memory
+
+**Parameters:**
+
+- `addr {vmm_pci_address_t}`: Address of passthrough PCI device
+- `config {vmm_pci_config_t}`: Ops for accessing the passthrough config space
+
+**Returns:**
+
+- `vmm_pci_entry_t` for passthrough device
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_create_bar_emulation(existing, num_bars, bars)`
+
+Construct a pci entry that emulates configuration space bar read/write's. The rest of the configuration space is passed on
+
+**Parameters:**
+
+- `existing {vmm_pci_entry_t}`: Existing PCI entry to wrap over and emulate its bar accesses
+- `num_bars {int}`: Number of emulated bars in PCI entry
+- `bars {vmm_pci_bar_t *}`: Set of bars to emulate access to
+
+**Returns:**
+
+- `vmm_pci_entry_t` for emulated bar device
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_create_passthrough_bar_emulation(existing, num_bars, bars)`
+
+Construct a pci entry that passes through all bar read/writes through to emulated io(read/write) handlers. This is the
+inverse of `vmm_pci_create_bar_emulation`
+
+**Parameters:**
+
+- `existing {vmm_pci_entry_t}`: Existing PCI entry to wrap over and passthrough bar read/writes
+- `num_bars {int}`: Number of emulated bars in PCI entry
+- `bars {vmm_pci_bar_t *}`: Set of bars to passthrough access to
+
+**Returns:**
+
+- `vmm_pci_entry_t` for passthrough bar device
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_create_irq_emulation(existing, irq)`
+
+Construct a pci entry the emulates configuration space interrupt read/write's. The rest of the configuration space is passed on
+
+**Parameters:**
+
+- `existing {vmm_pci_entry_t}`: Existing PCI entry to wrap over and emulate its IRQ accesses
+- `irq {int}`: IRQ line value in PCI entry
+
+**Returns:**
+
+- `vmm_pci_entry_t` for emulated irq device
+
+Back to [interface description](#module-pcih).
+
+### Function `vmm_pci_create_cap_emulation(existing, num_caps, cap, num_ranges, range_starts, range_ends)`
+
+Capability space emulation. Takes list of addresses to use to form a capability linked list, as well as a
+ranges of the capability space that should be directly disallowed. Assumes a type 0 device.
+
+**Parameters:**
+
+- `existing {vmm_pci_entry_t}`: Existing PCI entry to wrap over and emulated it capability space accesses
+- `num_caps {int}`: Number of caps in capability space
+- `caps {uint8_t *}`: Capability list
+- `num_ranges {int}`: Number of disallowed/ignored capability ranges e.g. MSI capabilities
+- `range_starts {uint8_t *}`: Array of starting indexes of ignored capability ranges
+- `range_end {uint8_t *}`: Array of ending idexes of ignored capabilities range
+
+**Returns:**
+
+- `vmm_pci_entry_t` with an emulated capability space
+
+Back to [interface description](#module-pcih).
+
+
+## Structs
+
+The interface `pci.h` defines the following structs.
+
+### Struct `vmm_pci_device_def`
+
+Struct definition of a PCI device. This is used for emulating a device from
+purely memory reads. This is not generally useful on its own, but provides
+a nice skeleton
+
+**Elements:**
+
+- `vendor_id {uint16_t}`
+- `device_id {uint16_t}`
+- `command {uint16_t}`
+- `status {uint16_t}`
+- `revision_id {uint8_t}`
+- `prog_if {uint8_t}`
+- `subclass {uint8_t}`
+- `class_code {uint8_t}`
+- `cache_line_size {uint8_t}`
+- `latency_timer {uint8_t}`
+- `header_type {uint8_t}`
+- `bist {uint8_t}`
+- `bar0 {uint32_t}`
+- `bar1 {uint32_t}`
+- `bar2 {uint32_t}`
+- `bar3 {uint32_t}`
+- `bar4 {uint32_t}`
+- `bar5 {uint32_t}`
+- `cardbus {uint32_t}`
+- `subsystem_vendor_id {uint16_t}`
+- `subsystem_id {uint16_t}`
+- `expansion_rom {uint32_t}`
+- `caps_pointer {uint8_t}`
+- `reserved1 {uint8_t}`
+- `reserved2 {uint16_t}`
+- `reserved3 {uint32_t}`
+- `interrupt_line {uint8_t}`
+- `interrupt_pin {uint8_t}`
+- `min_grant {uint8_t}`
+- `max_latency {uint8_t}`
+- `caps_len {int}`
+- `caps {void *}`
+
+Back to [interface description](#module-pcih).
+
+### Struct `vmm_pci_bar`
+
+Represents a PCI bar within a device
+
+**Elements:**
+
+- `mem_type {pci_mem_type_t}`: Type of memory supporting PCI bar
+- `address {uintptr_t}`: Address of PCI bar
+- `size_bits {size_t}`: Size of PCI bar in bits
+
+Back to [interface description](#module-pcih).
+
+### Struct `pci_bar_emulation`
+
+Wrapper datastructure over a pci entry and its configuration space. This is leveraged to emulate
+BAR accesses in an entries configuration space
+the guest OS over-writing elements in the configuration space
+
+**Elements:**
+
+- `passthrough {vmm_pci_entry_t}`: PCI entry being emulated
+- `num_bars {int}`: Number of PCI bars
+- `bars {vmm_pci_bar_t}`: Set of PCI bars being emulated in the PCI entry
+- `bar_writes {uint32_t}`: Most recent write to each PCI bar in the configuration space. This avoids
+
+Back to [interface description](#module-pcih).
+
+### Struct `pci_irq_emulation`
+
+Wrapper datastructure over a pci entry and its configuration space. This is leveraged to emulate
+IRQ line accesses in an entries configuration space
+
+**Elements:**
+
+- `passthrough {vmm_pci_entry_t}`: PCI entry being emulated
+- `irq {int}`: IRQ line value in PCI entry
+
+Back to [interface description](#module-pcih).
+
+### Struct `pci_passthrough_device`
+
+Datastructure providing direct passthrough access to a pci entry configuration space
+
+**Elements:**
+
+- `addr {vmm_pci_address_t}`: Address of PCI device
+- `config {vmm_pci_config_t}`: Ops for accessing config space
+
+Back to [interface description](#module-pcih).
+
+### Struct `pci_cap_emulation`
+
+Wrappper datastructure over a pci entry and its configuration space. This is leveraged to emulate
+capabilities in an entries configuration space.
+
+**Elements:**
+
+- `passthrough {vmm_pci_entry_t}`: PCI entry being emulation
+- `num_caps {int}`: Number of caps in capability space
+- `caps {uint8_t *}`: Capability list
+- `num_ignore {int}`: Number of disallowed/ignored capability ranges e.g. MSI capabilities
+- `ignore_start {uint8_t *}`: Array of starting indexes of ignored capability ranges
+- `ignore_end {uint8_t *}`: Array of ending idexes of ignored capabilities range
+
+Back to [interface description](#module-pcih).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_con.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_con.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_con.md
new file mode 100644
index 0000000..4c72608
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_con.md
@@ -0,0 +1,78 @@
+<!--
+     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 `virtio_con.h`
+
+This interface provides the ability to initalise a VMM virtio console driver. This creating a virtio
+PCI device in the VM's virtual pci. This can subsequently be accessed through '/dev/hvc0' in the guest.
+
+### Brief content:
+
+**Functions**:
+
+> [`common_make_virtio_con(vm, pci, ioport, ioport_range, port_type, interrupt_pin, interrupt_lin, backend)`](#function-common_make_virtio_convm-pci-ioport-ioport_range-port_type-interrupt_pin-interrupt_lin-backend)
+
+
+
+**Structs**:
+
+> [`virtio_con`](#struct-virtio_con)
+
+
+## Functions
+
+The interface `virtio_con.h` defines the following functions.
+
+### Function `common_make_virtio_con(vm, pci, ioport, ioport_range, port_type, interrupt_pin, interrupt_lin, backend)`
+
+Initialise a new virtio_con device with Base Address Registers (BARs) starting at iobase and backend functions
+specified by the console_passthrough struct.
+virtio_con_default_backend for default methods.
+
+**Parameters:**
+
+- `vm {vm_t *}`: Handle to the VM
+- `pci {vmm_pci_space_t *}`: PCI library instance to register virtio con device
+- `ioport {vmm_io_port_list_t *}`: IOPort library instance to register virtio con ioport
+- `ioport_range {ioport_range_t}`: BAR port for front end emulation
+- `iotype {ioport_type_t}`: Type of ioport i.e. whether to alloc or use given range
+- `interrupt_pin {unsigned int}`: PCI interrupt pin e.g. INTA = 1, INTB = 2 ,...
+- `interrupt_line {unsigned int}`: PCI interrupt line for virtio con IRQS
+- `backend {struct console_passthrough}`: Function pointers to backend implementation. Can be initialised by
+
+**Returns:**
+
+- Pointer to an initialised virtio_con_t, NULL if error.
+
+Back to [interface description](#module-virtio_conh).
+
+
+## Structs
+
+The interface `virtio_con.h` defines the following structs.
+
+### Struct `virtio_con`
+
+Virtio Console Driver Interface
+
+**Elements:**
+
+- `iobase {unsigned int}`: IO Port base for virtio con device
+- `emul {virtio_emul_t *}`: Virtio console emulation interface: VMM <-> Guest
+- `emul_driver_funcs {struct console_passthrough}`: Virtio console emulation functions: VMM <-> Guest
+- `ioops {ps_io_ops_t}`: Platform support io ops datastructure
+
+Back to [interface description](#module-virtio_conh).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_net.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_net.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_net.md
new file mode 100644
index 0000000..6e02150
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_virtio_net.md
@@ -0,0 +1,97 @@
+<!--
+     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 `virtio_net.h`
+
+This interface provides the ability to initalise a VMM virtio net driver. This creating a virtio
+PCI device in the VM's virtual pci. This can subsequently be accessed as an ethernet interface in the
+guest.
+
+### Brief content:
+
+**Functions**:
+
+> [`common_make_virtio_net(vm, pci, ioport, ioport_range, port_type, interrupt_pin, interrupt_line, backend, emulate_bar_access)`](#function-common_make_virtio_netvm-pci-ioport-ioport_range-port_type-interrupt_pin-interrupt_line-backend-emulate_bar_access)
+
+> [`virtio_net_default_backend()`](#function-virtio_net_default_backend)
+
+
+
+**Structs**:
+
+> [`virtio_net`](#struct-virtio_net)
+
+
+## Functions
+
+The interface `virtio_net.h` defines the following functions.
+
+### Function `common_make_virtio_net(vm, pci, ioport, ioport_range, port_type, interrupt_pin, interrupt_line, backend, emulate_bar_access)`
+
+Initialise a new virtio_net device with Base Address Registers (BARs) starting at iobase and backend functions
+specified by the raw_iface_funcs struct.
+virtio_net_default_backend for default methods.
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `pci {vmm_pci_space_t *}`: PCI library instance to register virtio net device
+- `ioport {vmm_io_port_list_t *}`: IOPort library instance to register virtio net ioport
+- `ioport_range {ioport_range_t}`: BAR port for front end emulation
+- `port_type {ioport_type_t}`: Type of ioport i.e. whether to alloc or use given range
+- `interrupt_pin {unsigned int}`: PCI interrupt pin e.g. INTA = 1, INTB = 2 ,...
+- `interrupt_line {unsigned int}`: PCI interrupt line for virtio net IRQS
+- `backend {struct raw_iface_funcs}`: Function pointers to backend implementation. Can be initialised by
+- `emulate_bar {bool}`: Emulate read and writes accesses to the PCI device Base Address Registers.
+
+**Returns:**
+
+- Pointer to an initialised virtio_net_t, NULL if error.
+
+Back to [interface description](#module-virtio_neth).
+
+### Function `virtio_net_default_backend()`
+
+update these function pointers with its own custom backend.
+
+**Parameters:**
+
+No parameters
+
+**Returns:**
+
+- A struct with a default virtio_net backend. It is the responsibility of the caller to
+
+Back to [interface description](#module-virtio_neth).
+
+
+## Structs
+
+The interface `virtio_net.h` defines the following structs.
+
+### Struct `virtio_net`
+
+Virtio Net Driver Interface
+
+**Elements:**
+
+- `iobase {unsigned int}`: IO Port base for Virtio Net device
+- `emul {virtio_emul_t *}`: Virtio Ethernet emulation interface: VMM <-> Guest
+- `emul_driver {struct eth_driver *}`: Backend Ethernet driver interface: VMM <-> Ethernet driver
+- `emul_driver_funcs {struct raw_iface_funcs}`: Virtio Ethernet emulation functions: VMM <-> Guest
+- `ioops {ps_io_ops_t}`: Platform support ioops for dma management
+
+Back to [interface description](#module-virtio_neth).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_acpi.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_acpi.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_acpi.md
new file mode 100644
index 0000000..aa94df4
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_acpi.md
@@ -0,0 +1,45 @@
+<!--
+     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 `acpi.h`
+
+The ACPI module provides support for generating ACPI table in a guest x86 VM. This being particularly leveraged
+for booting a guest Linux VM.
+
+### Brief content:
+
+**Functions**:
+
+> [`make_guest_acpi_tables(vm)`](#function-make_guest_acpi_tablesvm)
+
+
+## Functions
+
+The interface `acpi.h` defines the following functions.
+
+### Function `make_guest_acpi_tables(vm)`
+
+Creates ACPI table for the guest VM
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the guest VM instance
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-acpih).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_guest_boot_init.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_guest_boot_init.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_guest_boot_init.md
new file mode 100644
index 0000000..95f4fcc
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_guest_boot_init.md
@@ -0,0 +1,69 @@
+<!--
+     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_boot_init.h`
+
+The libsel4vmmplatsupport x86 guest boot init interface provides helpers to initialise the booting state of
+a VM instance. This currently only targets booting a Linux guest OS.
+
+### Brief content:
+
+**Functions**:
+
+> [`vmm_plat_init_guest_boot_structure(vm, cmdline, guest_kernel_image, guest_ramdisk_image, guest_boot_info_addr)`](#function-vmm_plat_init_guest_boot_structurevm-cmdline-guest_kernel_image-guest_ramdisk_image-guest_boot_info_addr)
+
+> [`vmm_plat_init_guest_thread_state(vcpu, guest_entry_addr, guest_boot_info_addr)`](#function-vmm_plat_init_guest_thread_statevcpu-guest_entry_addr-guest_boot_info_addr)
+
+
+## Functions
+
+The interface `guest_boot_init.h` defines the following functions.
+
+### Function `vmm_plat_init_guest_boot_structure(vm, cmdline, guest_kernel_image, guest_ramdisk_image, guest_boot_info_addr)`
+
+Establish the necessary BIOS boot structures to initialise and boot a guest Linux OS. This includes the creation of a BIOS
+boot info structure, an e820 map and ACPI tables.
+(in guest physical address space)
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the guest VM
+- `cmdline {const char *}`: The guest Linux boot commandline
+- `guest_kernel_image {guest_kernel_image_t}`: Guest kernel image (preloaded into the VM's memory)
+- `guest_ramdisk_image {guest_image_t}`: Guest ramdisk image (preloaded into the VM's memory)
+- `guest_boot_info_addr {uintptr_t *}`: Resulting address of loaded generated guest boot info structure
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-guest_boot_inith).
+
+### Function `vmm_plat_init_guest_thread_state(vcpu, guest_entry_addr, guest_boot_info_addr)`
+
+Initialise the booting state of a guest VM, establishing the necessary thread state to launch a guest Linux OS
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: A handle to the boot vcpu
+- `guest_entry_addr {uintptr_t}`: Address of VM entry point (often entry point defined in kernel elf image)
+- `guest_boot_info_addr {uintptr_t}`: Address of loaded guest boot info structure
+
+**Returns:**
+
+- 0 for success, -1 for error
+
+Back to [interface description](#module-guest_boot_inith).
+
+
+Back to [top](#).
+

libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_vmm_pci_helper.md

diff --git a/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_vmm_pci_helper.md b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_vmm_pci_helper.md
new file mode 100644
index 0000000..3f5e551
--- /dev/null
+++ b/libsel4vmmplatsupport/docs/libsel4vmmplatsupport_x86_vmm_pci_helper.md
@@ -0,0 +1,85 @@
+<!--
+     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 `vmm_pci_helper.h`
+
+The interface presents a series of helpers for establishing VMM PCI support on x86 platforms.
+
+### Brief content:
+
+**Functions**:
+
+> [`vmm_pci_helper_map_bars(vm, cfg, bars)`](#function-vmm_pci_helper_map_barsvm-cfg-bars)
+
+> [`vmm_pci_io_port_in(vcpu, cookie, port_no, size, result)`](#function-vmm_pci_io_port_invcpu-cookie-port_no-size-result)
+
+> [`vmm_pci_io_port_out(vcpu, cookie, port_no, size, value)`](#function-vmm_pci_io_port_outvcpu-cookie-port_no-size-value)
+
+
+## Functions
+
+The interface `vmm_pci_helper.h` defines the following functions.
+
+### Function `vmm_pci_helper_map_bars(vm, cfg, bars)`
+
+Given a PCI device config, map the PCI device bars into the VM, effectively passing-through the
+PCI device. This will map MMIO and IO-based bars.
+
+**Parameters:**
+
+- `vm {vm_t *}`: A handle to the VM
+- `cfg {libpci_device_iocfg_t *}`: PCI device config
+- `bars {vmm_pci_bar_t *}`: Resulting PCI bars mapped into the VM
+
+**Returns:**
+
+- -1 for error, otherwise the number of bars mapped into the VM (>=0)
+
+Back to [interface description](#module-vmm_pci_helperh).
+
+### Function `vmm_pci_io_port_in(vcpu, cookie, port_no, size, result)`
+
+Emulates IOPort in access on the VMM Virtual PCI device
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Faulting vcpu performing ioport access
+- `port_no {unsigned int}`: Port address being accessed
+- `size {unsigned int}`: Size of ioport access
+- `result {unsigned int *}`: Pointer that will be populated with resulting data of io-in op
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-vmm_pci_helperh).
+
+### Function `vmm_pci_io_port_out(vcpu, cookie, port_no, size, value)`
+
+Emulates IOPort out access on the VMM Virtual PCI device
+
+**Parameters:**
+
+- `vcpu {vm_vcpu_t *}`: Faulting vcpu performing ioport access
+- `port_no {unsigned int}`: Port address being accessed
+- `size {unsigned int}`: Size of ioport access
+- `value {unsigned int}`: Value being written in io-out op
+
+**Returns:**
+
+No return
+
+Back to [interface description](#module-vmm_pci_helperh).
+
+
+Back to [top](#).
+