diff --git a/libsel4platsupport/include/sel4platsupport/io.h b/libsel4platsupport/include/sel4platsupport/io.h
index f6d4986..e947030 100644
--- a/libsel4platsupport/include/sel4platsupport/io.h
+++ b/libsel4platsupport/include/sel4platsupport/io.h
@@ -21,6 +21,16 @@
 #include <stdlib.h>
 #include <stdio.h>
 
+/*
+ * NOTE: All vspace, vka, simple interfaces that are passed in *MUST* remain
+ * valid for the lifetime of these interfaces.
+ *
+ * Additionally, these interfaces are not thread-safe, so care must be taken to
+ * ensure that synchronisation is controlled externally. This also includes the
+ * simple, vspace and vka interfaces that were passed in to initialise these
+ * interfaces.
+ */
+
 /**
  * Creates a new implementation of the platsupport io_mapper interface using a
  * provided simple, vspace and vka
@@ -31,7 +41,7 @@
  *
  * @return returns 0 on success
  */
-int sel4platsupport_new_io_mapper(vspace_t vspace, vka_t vka, ps_io_mapper_t *io_mapper);
+int sel4platsupport_new_io_mapper(vspace_t *vspace, vka_t *vka, ps_io_mapper_t *io_mapper);
 
 /**
  * Create a new malloc ops using stdlib malloc, calloc and free.
@@ -61,15 +71,15 @@
  *
  * @return returns 0 on success
  */
-int sel4platsupport_new_io_ops(vspace_t vspace, vka_t vka, ps_io_ops_t *io_ops);
+int sel4platsupport_new_io_ops(vspace_t *vspace, vka_t *vka, ps_io_ops_t *io_ops);
 
 /* Initialise all arch-specific io ops for this platform
  *
  * sel4platsupport_new_io_ops should have already populated relevant non-arch specific
  * io ops (memory allocation, mapping).
  *
- * @param simple a simple interface which must remain valid after this call.
- * @param vka a vka interface which must remain valid after this call.
+ * @param simple a simple interface
+ * @param vka a vka interface
  * @return 0 on success.
  */
 int sel4platsupport_new_arch_ops(ps_io_ops_t *ops, simple_t *simple, vka_t *vka);
diff --git a/libsel4platsupport/src/io.c b/libsel4platsupport/src/io.c
index 500bf16..151c5ea 100644
--- a/libsel4platsupport/src/io.c
+++ b/libsel4platsupport/src/io.c
@@ -43,8 +43,8 @@
 } io_mapping_t;
 
 typedef struct sel4platsupport_io_mapper_cookie {
-    vspace_t vspace;
-    vka_t vka;
+    vspace_t *vspace;
+    vka_t *vka;
     io_mapping_t *head;
 } sel4platsupport_io_mapper_cookie_t;
 
@@ -137,8 +137,8 @@
                                                       size_t size, size_t page_size_bits, bool cached)
 {
 
-    vka_t *vka = &io_mapper->vka;
-    vspace_t *vspace = &io_mapper->vspace;
+    vka_t *vka = io_mapper->vka;
+    vspace_t *vspace = io_mapper->vspace;
 
     /* search at start of page */
     int page_size = BIT(page_size_bits);
@@ -228,8 +228,8 @@
 {
     sel4platsupport_io_mapper_cookie_t *io_mapper = cookie;
 
-    vspace_t *vspace = &io_mapper->vspace;
-    vka_t *vka = &io_mapper->vka;
+    vspace_t *vspace = io_mapper->vspace;
+    vka_t *vka = io_mapper->vka;
     io_mapping_t *mapping = find_node(io_mapper, vaddr);
 
     if (!mapping) {
@@ -246,7 +246,7 @@
     destroy_node(vka, mapping);
 }
 
-int sel4platsupport_new_io_mapper(vspace_t vspace, vka_t vka, ps_io_mapper_t *io_mapper)
+int sel4platsupport_new_io_mapper(vspace_t *vspace, vka_t *vka, ps_io_mapper_t *io_mapper)
 {
     sel4platsupport_io_mapper_cookie_t *cookie = calloc(1, sizeof(sel4platsupport_io_mapper_cookie_t));
     if (!cookie) {
@@ -331,7 +331,7 @@
 #endif
 }
 
-int sel4platsupport_new_io_ops(vspace_t vspace, vka_t vka, ps_io_ops_t *io_ops)
+int sel4platsupport_new_io_ops(vspace_t *vspace, vka_t *vka, ps_io_ops_t *io_ops)
 {
     memset(io_ops, 0, sizeof(ps_io_ops_t));