RISC-V port

diff --git a/libsel4allocman/sel4_arch/riscv/allocman/sel4_arch/mapping.h b/libsel4allocman/sel4_arch/riscv/allocman/sel4_arch/mapping.h
new file mode 100644
index 0000000..4681ba8
--- /dev/null
+++ b/libsel4allocman/sel4_arch/riscv/allocman/sel4_arch/mapping.h

@@ -0,0 +1,23 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef __ALLOCMAN_SEL4_ARCH_MAPPING__
+#define __ALLOCMAN_SEL4_ARCH_MAPPING__
+
+#include <allocman/allocman.h>
+
+static inline seL4_Error allocman_sel4_arch_create_object_at_level(allocman_t *alloc, seL4_Word bits, cspacepath_t *path, void *vaddr, seL4_CPtr vspace_root) {
+    /* RISCV has no paging objects beyond the common page table
+     * so this function should never get called */
+    ZF_LOGF("Invalid lookup level");
+    return seL4_InvalidArgument;
+}
+
+#endif

diff --git a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h b/libsel4allocman/sel4_arch/riscv/allocman/sel4_arch/reservation.h
similarity index 60%
copy from libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
copy to libsel4allocman/sel4_arch/riscv/allocman/sel4_arch/reservation.h
index da14c1b..a0e6c05 100644
--- a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
+++ b/libsel4allocman/sel4_arch/riscv/allocman/sel4_arch/reservation.h

@@ -9,7 +9,13 @@
  *
  * @TAG(DATA61_BSD)
  */
-#pragma once
 
-/* nothing - this is here so we don't have to wrap #ifdef ARCH/IA32 around arch/io.h includes */
+#ifndef __ALLOCMAN_SEL4_ARCH_RESERVATION__
+#define __ALLOCMAN_SEL4_ARCH_RESERVATION__
 
+#include <allocman/allocman.h>
+
+static inline void allocman_sel4_arch_configure_reservations(allocman_t *alloc) {
+}
+
+#endif

diff --git a/libsel4allocman/sel4_arch/riscv32 b/libsel4allocman/sel4_arch/riscv32
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4allocman/sel4_arch/riscv32

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4allocman/sel4_arch/riscv64 b/libsel4allocman/sel4_arch/riscv64
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4allocman/sel4_arch/riscv64

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4debug/arch_include/riscv/sel4debug/arch/registers.h b/libsel4debug/arch_include/riscv/sel4debug/arch/registers.h
new file mode 100644
index 0000000..11d9062
--- /dev/null
+++ b/libsel4debug/arch_include/riscv/sel4debug/arch/registers.h

@@ -0,0 +1,31 @@
+
+#ifndef __DEBUG_ARCH_REGISTERS_H
+#define __DEBUG_ARCH_REGISTERS_H
+
+#include <sel4/sel4.h>
+#include <stddef.h>
+#include <utils/util.h>
+
+static UNUSED const char *register_names[] = {
+    /* FIXME: Add the full set of registers */
+    "ra",
+    "sp",
+    "t0",
+    "t1",
+    "t2",
+    "a0",
+    "a1",
+    "a2",
+    "a3",
+    "a4",
+    "a5",
+    "a6",
+    "a7",
+    "t3",
+    "t4",
+    "t5",
+    "t6",
+
+};
+
+#endif /* __DEBUG_ARCH_REGISTERS_H */

diff --git a/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/device.h b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/device.h
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/device.h

@@ -0,0 +1 @@
+

diff --git a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/io.h
similarity index 62%
copy from libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
copy to libsel4platsupport/arch_include/riscv/sel4platsupport/arch/io.h
index da14c1b..3d8707a 100644
--- a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
+++ b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/io.h

@@ -9,7 +9,10 @@
  *
  * @TAG(DATA61_BSD)
  */
-#pragma once
+#ifndef _RISCV_PLATSUPPORT_IO_H
+#define _RISCV_PLATSUPPORT_IO_H
 
-/* nothing - this is here so we don't have to wrap #ifdef ARCH/IA32 around arch/io.h includes */
+/* nothing - this is here so we don't have to wrap #ifdef ARCH/RISCV around arch/io.h includes */
+
+#endif /* _RISCV_PLATSUPPORT_IO_H */
 

diff --git a/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/serial.h b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/serial.h
new file mode 100644
index 0000000..f875ae0
--- /dev/null
+++ b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/serial.h

@@ -0,0 +1,22 @@
+/*
+ * Copyright 2017, 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)
+ */
+
+#pragma once
+
+#include <vka/object.h>
+
+typedef struct arch_serial_objects {
+    /* Paddr of the platsupport default serial's frame */
+    uintptr_t serial_frame_paddr;
+    /* VKA object for the platsupport default serial's frame */
+    vka_object_t serial_frame_obj;
+} arch_serial_objects_t;

diff --git a/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/timer.h b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/timer.h
new file mode 100644
index 0000000..cd9a374
--- /dev/null
+++ b/libsel4platsupport/arch_include/riscv/sel4platsupport/arch/timer.h

@@ -0,0 +1,28 @@
+/*
+ * Copyright 2017, 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)
+ */
+#pragma once
+
+#include <sel4platsupport/timer_types.h>
+#include <sel4platsupport/plat/timer.h>
+
+#include <autoconf.h>
+#include <platsupport/timer.h>
+#include <platsupport/plat/timer.h>
+#include <vspace/vspace.h>
+#include <simple/simple.h>
+#include <vka/vka.h>
+
+typedef struct arch_timer_objects {
+    plat_timer_objects_t plat_timer_objects;
+} arch_timer_objects_t;
+
+seL4_timer_t *sel4platsupport_get_generic_timer(void);

diff --git a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h b/libsel4platsupport/plat_include/spike/sel4platsupport/plat/serial.h
similarity index 75%
copy from libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
copy to libsel4platsupport/plat_include/spike/sel4platsupport/plat/serial.h
index da14c1b..6ea0202 100644
--- a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
+++ b/libsel4platsupport/plat_include/spike/sel4platsupport/plat/serial.h

@@ -9,7 +9,9 @@
  *
  * @TAG(DATA61_BSD)
  */
+
 #pragma once
+//#include <platsupport/plat/timer.h>
 
-/* nothing - this is here so we don't have to wrap #ifdef ARCH/IA32 around arch/io.h includes */
-
+#define DEFAULT_SERIAL_PADDR NULL 
+#define DEFAULT_SERIAL_INTERRUPT 0

diff --git a/libsel4platsupport/plat_include/spike/sel4platsupport/plat/timer.h b/libsel4platsupport/plat_include/spike/sel4platsupport/plat/timer.h
new file mode 100644
index 0000000..74aba45
--- /dev/null
+++ b/libsel4platsupport/plat_include/spike/sel4platsupport/plat/timer.h

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2017, 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)
+ */
+#ifndef _SEL4PLATSUPPORT_PLAT_TIMER_H
+#define _SEL4PLATSUPPORT_PLAT_TIMER_H
+
+// FIXME
+#define DEFAULT_TIMER_INTERRUPT 0
+
+typedef struct plat_timer_objects {
+} plat_timer_objects_t;
+
+#endif /* _SEL4PLATSUPPORT_PLAT_TIMER_H */

diff --git a/libsel4platsupport/src/arch/riscv/crt0.S b/libsel4platsupport/src/arch/riscv/crt0.S
new file mode 100644
index 0000000..1971cdb
--- /dev/null
+++ b/libsel4platsupport/src/arch/riscv/crt0.S

@@ -0,0 +1,61 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+/*
+ * A default crt0 for ARM. It does the bare minimum required to get into
+ * main() with a sensible C environment.
+ *
+ * This file will only be linked in if:
+ *   - no other file already provides a _start symbol, and
+ *   - _start is an undefined external symbol (force this by passing
+ *     "-u _start" to ld).
+ */
+
+#include <autoconf.h>
+
+#ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_START
+.extern __stdout_used
+.text
+
+/*
+ * Image Entry point.
+ */
+.global _start
+_start:
+    /* Dirty hack to load gp and avoid load/store exceptions, this should be
+    * defined by the linker */
+#error "you know"
+     li gp, 0x800
+     la s0, __stdout_used
+     add gp, gp, s0
+    /* Setup a stack for ourselves. */
+    la     sp, _stack_top
+
+    /* Setup bootinfo. The pointer to the bootinfo struct starts in 'a0'. */
+    #add a0, x0, a5
+    jal      seL4_InitBootInfo
+
+    la      a1, sel4_vsyscall
+    /* Call constructors and other initialisation functions. */
+    jal      _init
+
+    /* Call main. */
+    jal     main
+    j       exit
+
+/* .text Literal Pool */
+
+/* Stack for the image. */
+.bss
+.align  8
+_stack_bottom:
+.space  16384
+_stack_top:
+
+#endif /* CONFIG_LIB_SEL4_PLAT_SUPPORT_START */

diff --git a/libsel4platsupport/src/arch/riscv/device.c b/libsel4platsupport/src/arch/riscv/device.c
new file mode 100644
index 0000000..68536d2
--- /dev/null
+++ b/libsel4platsupport/src/arch/riscv/device.c

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2017, 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)
+ */
+
+#include <sel4platsupport/device.h>
+#include <utils/util.h>
+
+int sel4platsupport_arch_copy_irq_cap(UNUSED arch_simple_t *arch_simple, UNUSED ps_irq_t *irq,
+        UNUSED cspacepath_t *dest)
+{
+    ZF_LOGE("unknown irq type");
+    return -1;
+}

diff --git a/libsel4platsupport/src/arch/riscv/pmem.c b/libsel4platsupport/src/arch/riscv/pmem.c
new file mode 100644
index 0000000..da3787a
--- /dev/null
+++ b/libsel4platsupport/src/arch/riscv/pmem.c

@@ -0,0 +1,24 @@
+/*
+ * Copyright 2017, 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)
+ */
+
+#include <stdint.h>
+#include <sel4platsupport/pmem.h>
+#include <utils/util.h>
+
+int sel4platsupport_get_num_pmem_regions(simple_t *simple) {
+    return 0;
+}
+
+int sel4platsupport_get_pmem_region_list(simple_t *simple, size_t max_length, pmem_region_t *region_list) {
+    ZF_LOGW("Not implemented");
+    return -1;
+}

diff --git a/libsel4platsupport/src/arch/riscv/sel4_crt0.S b/libsel4platsupport/src/arch/riscv/sel4_crt0.S
new file mode 100644
index 0000000..a4ee476
--- /dev/null
+++ b/libsel4platsupport/src/arch/riscv/sel4_crt0.S

@@ -0,0 +1,89 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+/*
+ * A default seL4 crt0 for arm. It does the bare minimum required to emulate
+ * a typical startup environment and jump to the regular _start symbol
+ */
+
+#include <autoconf.h>
+
+#ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START
+
+    .global _sel4_start
+    .extern sel4_vsyscall
+    .extern __dso_handle 
+.text
+
+_sel4_start:
+
+    /* Dirty hack to load gp and avoid load/store exceptions, this should be
+     * defined by the linker */
+    //li gp, 0x800
+    //la s0, __dso_handle
+    //add gp, gp, s0
+    la gp, _gp
+
+    /* Setup a stack for ourselves. */
+    la     sp, _stack_top
+
+    /* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */
+    jal      seL4_InitBootInfo
+
+    /* Setup stack frame ready for jumping to _start */
+    addi sp, sp, -64
+    
+    /* argc */
+    li   a1, 1
+    sd   a1, 0(sp)
+    
+    /* prog name */
+    la   a1, prog_name
+    sd   a1, 8(sp)
+    
+    /* Null-terminate arg vector */
+    sd   x0, 16(sp)
+    
+    /* Give an environment string */
+    la   a1, environment_string
+
+    /* Null terminate envp */
+    sd   x0, 24(sp)
+
+    /* give vsyscall location */
+    li   a1, 32
+    sw   a1, 32(sp)
+    la   a1, sel4_vsyscall
+    sw   a1, 40(sp)
+    
+    /* null terminate auxv */
+    sw   x0, 48(sp)
+    sw   x0, 56(sp)
+    sw   x0, 64(sp) 
+
+    /* Now go to actual _start */
+    j       _start
+
+/* .text Literal Pool */
+    .data
+    .align 4
+
+environment_string:
+    .asciz "seL4=1"
+prog_name:
+    .asciz "rootserver"
+
+    .bss
+    .align  8
+
+_stack_bottom:
+    .space  16384
+_stack_top:
+
+#endif /* CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START */

diff --git a/libsel4platsupport/src/arch/riscv/serial.c b/libsel4platsupport/src/arch/riscv/serial.c
new file mode 100644
index 0000000..4061db4
--- /dev/null
+++ b/libsel4platsupport/src/arch/riscv/serial.c

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2017, 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)
+ */
+
+#include <sel4platsupport/serial.h>
+#include <sel4platsupport/device.h>
+
+int
+sel4platsupport_arch_init_default_serial_caps(vka_t *vka, UNUSED vspace_t *vspace, simple_t *simple, serial_objects_t *serial_objects)
+{
+    /* No serial driver */
+    return 0;
+}

diff --git a/libsel4platsupport/src/arch/riscv/timer.c b/libsel4platsupport/src/arch/riscv/timer.c
new file mode 100644
index 0000000..80e2051
--- /dev/null
+++ b/libsel4platsupport/src/arch/riscv/timer.c

@@ -0,0 +1,29 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#include <autoconf.h>
+#include <vka/vka.h>
+#include <vspace/vspace.h>
+
+#include <sel4platsupport/timer.h>
+#include <sel4platsupport/plat/timer.h>
+
+#include <stdlib.h>
+
+seL4_timer_t *
+sel4platsupport_get_generic_timer(void)
+{
+    return NULL;
+}
+
+uintptr_t
+sel4platsupport_get_default_timer_paddr(UNUSED vka_t *vka, UNUSED vspace_t *vspace)
+{
+    return NULL;
+}

diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c
index fbc9c77..dfe2aec 100644
--- a/libsel4platsupport/src/common.c
+++ b/libsel4platsupport/src/common.c

@@ -56,11 +56,16 @@
 static vka_t _vka_mem;
 
 /* Hacky constants / data structures for a failsafe mapping */
+#ifdef ARCH_RISCV
+#define DITE_HEADER_START ((seL4_Word) 0x1000 - 0x1000)
+#else
 #define DITE_HEADER_START ((seL4_Word)__executable_start - 0x1000)
+#endif
 static seL4_CPtr device_cap = 0;
 extern char __executable_start[];
 
-#if !(defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_DEBUG_BUILD))
+
+#if !(defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_PRINTING))
 static void* __map_device_page(void* cookie, uintptr_t paddr, size_t size,
                                int cached, ps_mem_flags_t flags);
 
@@ -213,7 +218,7 @@
     }
     memset(&_simple_mem, 0, sizeof(simple_t));
     memset(&_vka_mem, 0, sizeof(vka_t));
-#if defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_DEBUG_BUILD)
+#if defined(CONFIG_PRINTING)
     /* only support putchar on a debug kernel */
     setup_status = SETUP_COMPLETE;
 #else
@@ -245,7 +250,7 @@
         assert(!"You cannot recover");
         return -1;
     }
-#if defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_DEBUG_BUILD)
+#if defined(CONFIG_PRINTING)
     /* only support putchar on a debug kernel */
     setup_status = SETUP_COMPLETE;
 #else
@@ -309,7 +314,7 @@
 __arch_putchar(int c)
 {
     if (setup_status != SETUP_COMPLETE) {
-        __serial_setup();
+        //__serial_setup();
     }
     __plat_putchar(c);
 }
@@ -329,7 +334,7 @@
 __arch_getchar(void)
 {
     if (setup_status != SETUP_COMPLETE) {
-        __serial_setup();
+        //__serial_setup();
     }
     return __plat_getchar();
 }

diff --git a/libsel4platsupport/src/sel4_arch/riscv/sel4_crt0.S b/libsel4platsupport/src/sel4_arch/riscv/sel4_crt0.S
new file mode 100644
index 0000000..ccd64a8
--- /dev/null
+++ b/libsel4platsupport/src/sel4_arch/riscv/sel4_crt0.S

@@ -0,0 +1,116 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+/*
+ * A default seL4 crt0 for arm. It does the bare minimum required to emulate
+ * a typical startup environment and jump to the regular _start symbol
+ */
+
+#include <autoconf.h>
+
+#ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START
+#if __riscv_xlen == 32
+#define LW lw
+#define SW sw
+#define REGSIZE 4
+#else
+#define LW ld
+#define SW sd
+#define REGSIZE 8
+#endif
+
+    .global _sel4_start
+    .extern sel4_vsyscall
+    .extern __dso_handle
+.text
+
+_sel4_start:
+
+/* Set gp for relaxation. See
+ * https://www.sifive.com/blog/2017/08/28/all-aboard-part-3-linker-relaxation-in-riscv-toolchain/
+ */
+.option push
+.option norelax
+1:auipc gp, %pcrel_hi(__global_pointer$)
+  addi  gp, gp, %pcrel_lo(1b)
+.option pop
+
+    /* Setup a stack for ourselves. */
+    la     sp, _stack_top
+
+    /* Setup bootinfo. The pointer to the bootinfo struct starts in 'a0'. */
+    //jal      seL4_InitBootInfo
+    /* Construct bootinfo environment variable */
+    mv     a2, a0
+    la     a0, bootinfo_storage
+    la     a1, bootinfo_format
+    jal    sprintf
+
+
+    /* Setup stack frame ready for jumping to _start */
+    addi sp, sp, -(10*REGSIZE)
+
+    /* argc */
+    li   a1, 1
+    SW   a1, 0(sp)
+
+    /* prog name */
+    la   a1, prog_name
+    SW   a1, (1*REGSIZE)(sp)
+
+    /* Null-terminate arg vector */
+    SW   x0, (2*REGSIZE)(sp)
+
+    /* Give an environment string */
+    la   a1, environment_string
+    SW   a1, (3*REGSIZE)(sp)
+
+    /* Give bootinfo location */
+    la   a1, bootinfo_storage
+    SW   a1, (4*REGSIZE)(sp)
+
+    /* Null terminate envp */
+    SW   x0, (5*REGSIZE)(sp)
+
+    /* give vsyscall location */
+    li   a1, 32
+    SW   a1, (6*REGSIZE)(sp)
+    la   a1, sel4_vsyscall
+    SW   a1, (7*REGSIZE)(sp)
+
+    /* null terminate auxv */
+    SW   x0, (8*REGSIZE)(sp)
+    SW   x0, (9*REGSIZE)(sp)
+    SW   x0, (10*REGSIZE)(sp)
+
+    /* Now go to actual _start */
+    j       _start
+
+/* .text Literal Pool */
+    .data
+    .align  8
+bootinfo_format:
+    .asciz "bootinfo=%p"
+    .align  8
+bootinfo_storage:
+    .space 29
+
+environment_string:
+    .asciz "seL4=1"
+prog_name:
+    .asciz "rootserver"
+
+    .bss
+    .align  8
+
+_stack_bottom:
+    .space  16384
+_stack_top:
+
+#endif /* CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START */

diff --git a/libsel4platsupport/src/sel4_arch/riscv32 b/libsel4platsupport/src/sel4_arch/riscv32
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4platsupport/src/sel4_arch/riscv32

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4platsupport/src/sel4_arch/riscv64 b/libsel4platsupport/src/sel4_arch/riscv64
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4platsupport/src/sel4_arch/riscv64

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4platsupport/src/serial.c b/libsel4platsupport/src/serial.c
index 1904840..abc2953 100644
--- a/libsel4platsupport/src/serial.c
+++ b/libsel4platsupport/src/serial.c

@@ -51,7 +51,7 @@
     struct ps_chardevice temp_device;
     if (ps_cdev_init(PS_SERIAL_DEFAULT, io_ops, &temp_device)) {
         /* Apply the changes */
-#if defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR)
+#if defined(CONFIG_PRINTING)
         temp_device.write = &debug_write;
 #endif
         console_device = temp_device;

diff --git a/libsel4simple-default/Kbuild b/libsel4simple-default/Kbuild
index cafd108..9982c39 100644
--- a/libsel4simple-default/Kbuild
+++ b/libsel4simple-default/Kbuild

@@ -11,4 +11,4 @@
 #
 
 libs-$(CONFIG_LIB_SEL4_SIMPLE_DEFAULT) += libsel4simple-default
-libsel4simple-default: libsel4 common $(libc) libsel4simple libsel4vspace libsel4debug libutils
+libsel4simple-default: libsel4 common $(libc) libsel4simple libsel4vspace libutils

diff --git a/libsel4simple-default/src/arch/riscv/default.c b/libsel4simple-default/src/arch/riscv/default.c
new file mode 100644
index 0000000..33062f6
--- /dev/null
+++ b/libsel4simple-default/src/arch/riscv/default.c

@@ -0,0 +1,33 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#include <autoconf.h>
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+
+#include <sel4/sel4.h>
+
+#include <simple-default/simple-default.h>
+
+#include <vspace/page.h>
+
+seL4_Error simple_default_get_irq(void *data, int irq, seL4_CNode root, seL4_Word index, uint8_t depth) {
+    return seL4_IRQControl_Get(seL4_CapIRQControl, irq, root, index, depth);
+}
+
+void
+simple_default_init_arch_simple(arch_simple_t *simple, void *data) 
+{
+    simple->data = data;
+    simple->irq = simple_default_get_irq;
+}
+

diff --git a/libsel4simple-default/src/libsel4simple-default.c b/libsel4simple-default/src/libsel4simple-default.c
index 2cbf7d5..1539de8 100644
--- a/libsel4simple-default/src/libsel4simple-default.c
+++ b/libsel4simple-default/src/libsel4simple-default.c

@@ -19,7 +19,7 @@
 #include <string.h>
 
 #include <sel4/sel4.h>
-#include <sel4debug/debug.h>
+//#include <sel4debug/debug.h>
 #include <simple-default/simple-default.h>
 
 #include <vspace/page.h>
@@ -177,7 +177,7 @@
         ZF_LOGE("Data is null!");
     }
 
-    debug_print_bootinfo(data);
+    //debug_print_bootinfo(data);
 }
 
 seL4_CPtr simple_default_sched_control(void *data, int core)

diff --git a/libsel4simple/arch_include/riscv/simple/arch/simple.h b/libsel4simple/arch_include/riscv/simple/arch/simple.h
new file mode 100644
index 0000000..b48545c
--- /dev/null
+++ b/libsel4simple/arch_include/riscv/simple/arch/simple.h

@@ -0,0 +1,44 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _INTERFACE_ARCH_SIMPLE_H_
+#define _INTERFACE_ARCH_SIMPLE_H_
+
+#include <autoconf.h>
+
+#include <assert.h>
+#include <sel4/sel4.h>
+#include <stdlib.h>
+#include <utils/util.h>
+#include <vka/cspacepath_t.h>
+
+/**
+ * Request a cap to a specific IRQ number on the system
+ *
+ * @param irq the irq number to get the cap for
+ * @param data cookie for the underlying implementation
+ * @param the CNode in which to put this cap
+ * @param the index within the CNode to put cap
+ * @param Depth of index
+ */
+typedef seL4_Error (*arch_simple_get_IRQ_control_fn)(void *data, int irq, seL4_CNode cnode, seL4_Word index, uint8_t depth); 
+
+typedef struct arch_simple {
+    void *data;
+    arch_simple_get_IRQ_control_fn irq;
+} arch_simple_t;
+
+static inline seL4_CPtr 
+arch_simple_get_IOPort_cap(arch_simple_t *arch_simple, uint16_t start_port, uint16_t end_port)
+{
+    ZF_LOGE("%s not implemented", __FUNCTION__);
+    return seL4_CapNull;
+}
+#endif /* _INTERFACE_ARCH_SIMPLE_H_ */

diff --git a/libsel4utils/arch_include/riscv/sel4utils/arch/.mapping.h.swp b/libsel4utils/arch_include/riscv/sel4utils/arch/.mapping.h.swp
new file mode 100644
index 0000000..902eb51
--- /dev/null
+++ b/libsel4utils/arch_include/riscv/sel4utils/arch/.mapping.h.swp
Binary files differ

diff --git a/libsel4utils/arch_include/riscv/sel4utils/arch/cache.h b/libsel4utils/arch_include/riscv/sel4utils/arch/cache.h
new file mode 100644
index 0000000..e08481a
--- /dev/null
+++ b/libsel4utils/arch_include/riscv/sel4utils/arch/cache.h

@@ -0,0 +1,32 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#ifndef SEL4UTILS_ARCH_CACHE_H
+#define SEL4UTILS_ARCH_CACHE_H
+
+#include <sel4/sel4.h>
+
+static inline int seL4_ARCH_PageDirectory_Clean_Data(seL4_CPtr root, seL4_Word start, seL4_Word end)
+{
+    return seL4_NoError;
+}
+
+static inline int seL4_ARCH_PageDirectory_Invalidate_Data(seL4_CPtr root, seL4_Word start, seL4_Word end)
+{
+    return seL4_NoError;
+}
+
+static inline int seL4_ARCH_PageDirectory_CleanInvalidate_Data(seL4_CPtr root, seL4_Word start, seL4_Word end)
+{
+    return seL4_NoError;
+}
+
+#endif /* SEL4UTILS_ARCH_CACHE_H */
+
+

diff --git a/libsel4utils/arch_include/riscv/sel4utils/arch/mapping.h b/libsel4utils/arch_include/riscv/sel4utils/arch/mapping.h
new file mode 100644
index 0000000..c389823
--- /dev/null
+++ b/libsel4utils/arch_include/riscv/sel4utils/arch/mapping.h

@@ -0,0 +1,51 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#ifndef _SEL4UTILS_ARCH_MAPPING_H
+#define _SEL4UTILS_ARCH_MAPPING_H
+
+#include <vspace/page.h>
+#include <vka/vka.h>
+#include <vka/object.h>
+
+static inline int
+sel4utils_create_object_at_level(vka_t *vka, seL4_Word failed_bits, vka_object_t *objects, int *num_objects, void *vaddr, seL4_CPtr vspace_root)
+{
+    int error;
+    if (failed_bits == SEL4_MAPPING_LOOKUP_NO_LVL2PT) {
+        vka_object_t object;
+        error = vka_alloc_page_table(vka, &object);
+        if (error) {
+            printf("Failed to allocate page table");
+            return error;
+        }
+        error = seL4_RISCV_PageTable_Map(object.cptr, vspace_root, (seL4_Word)vaddr, seL4_RISCV_Default_VMAttributes);
+        if (error == seL4_DeleteFirst) {
+            /* through creating the object we must have ended up mapping this
+             * level as part of the metadata creation. Delete this and keep
+             * on going */
+            vka_free_object(vka, &object);
+            printf("Failed to map lvl2 page table, already exist, delete first");
+            return 0;
+        }
+        if (error) {
+            printf("Failed to map lvl2 page table");
+            vka_free_object(vka, &object);
+        } else {
+            objects[*num_objects] = object;
+            (*num_objects)++;
+        }
+        return error;
+    } else {
+        printf("Invalid lookup level %d", (int)failed_bits);
+        return seL4_InvalidArgument;
+    }
+}
+
+#endif /* _SEL4UTILS_ARCH_MAPPING_H */

diff --git a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h b/libsel4utils/arch_include/riscv/sel4utils/arch/page.h
similarity index 77%
rename from libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
rename to libsel4utils/arch_include/riscv/sel4utils/arch/page.h
index da14c1b..6ca3c06 100644
--- a/libsel4platsupport/arch_include/arm/sel4platsupport/arch/io.h
+++ b/libsel4utils/arch_include/riscv/sel4utils/arch/page.h

@@ -11,5 +11,4 @@
  */
 #pragma once
 
-/* nothing - this is here so we don't have to wrap #ifdef ARCH/IA32 around arch/io.h includes */
-
+#include <vspace/arch/page.h>

diff --git a/libsel4utils/arch_include/riscv/sel4utils/arch/util.h b/libsel4utils/arch_include/riscv/sel4utils/arch/util.h
new file mode 100644
index 0000000..81109a1
--- /dev/null
+++ b/libsel4utils/arch_include/riscv/sel4utils/arch/util.h

@@ -0,0 +1,26 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#ifndef _SEL4UTILS_ARCH_UTIL_H
+#define _SEL4UTILS_ARCH_UTIL_H
+
+#include <stdint.h>
+#include <sel4/sel4.h>
+#include <sel4/arch/pfIPC.h>
+#include <sel4/arch/exIPC.h>
+#include <sel4utils/sel4_arch/util.h>
+
+static inline int
+sel4utils_is_read_fault(void)
+{
+    seL4_Word fsr = seL4_GetMR(seL4_VMFault_FSR);
+    return (fsr == 1 || fsr == 2 || fsr == 5);
+}
+
+#endif /* _SEL4UTILS_ARCH_UTIL_H */

diff --git a/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/mapping.h b/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/mapping.h
new file mode 100644
index 0000000..359762a
--- /dev/null
+++ b/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/mapping.h

@@ -0,0 +1,23 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#ifndef _SEL4UTILS_SEL4_ARCH_MAPPING_H
+#define _SEL4UTILS_SEL4_ARCH_MAPPING_H
+
+#include <vspace/arch/page.h>
+#include <vka/vka.h>
+#include <vka/object.h>
+
+static inline int
+sel4utils_create_object_at_level(vka_t *vka, seL4_Word failed_bits, vka_object_t *objects, int *num_objects, void *vaddr, seL4_CPtr vspace_root)
+{
+    ZF_LOGE("TODO: Not implemented yet");
+}
+
+#endif /* _SEL4UTILS_SEL4_ARCH_MAPPING_H */

diff --git a/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/util.h b/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/util.h
new file mode 100644
index 0000000..d5ad27d
--- /dev/null
+++ b/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/util.h

@@ -0,0 +1,43 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#ifndef _SEL4UTILS_SEL4_ARCH_UTIL_H
+#define _SEL4UTILS_SEL4_ARCH_UTIL_H
+
+#include <stdint.h>
+#include <sel4/sel4.h>
+
+#define EXCEPT_IPC_SYS_MR_IP EXCEPT_IPC_SYS_MR_RIP
+#define ARCH_SYSCALL_INSTRUCTION_SIZE 4
+
+static inline void
+sel4utils_set_instruction_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+    regs->pc = value;
+}
+
+static inline seL4_Word
+sel4utils_get_instruction_pointer(seL4_UserContext regs)
+{
+    return regs.pc;
+}
+
+static inline seL4_Word
+sel4utils_get_sp(seL4_UserContext regs)
+{
+    return regs.sp;
+}
+
+static inline void
+sel4utils_set_stack_pointer(seL4_UserContext *regs, seL4_Word value)
+{
+    regs->sp = value;
+}
+
+#endif /* _SEL4UTILS_SEL4_ARCH_UTIL_H */

diff --git a/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/vspace.h b/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/vspace.h
new file mode 100644
index 0000000..a3e0ac5
--- /dev/null
+++ b/libsel4utils/sel4_arch_include/riscv/sel4utils/sel4_arch/vspace.h

@@ -0,0 +1,33 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef SEL4UTILS_SEL4_ARCH_VSPACE_H
+#define SEL4UTILS_SEL4_ARCH_VSPACE_H
+
+#include <autoconf.h>
+
+#if CONFIG_PT_LEVELS == 2
+#define KERNEL_RESERVED_START 0x7ffff000
+#define VSPACE_LEVEL_BITS 10
+#elif CONFIG_PT_LEVELS == 3
+#define KERNEL_RESERVED_START 0x0000002ffffff000
+#define VSPACE_LEVEL_BITS 9
+#elif CONFIG_PT_LEVELS == 4
+#define KERNEL_RESERVED_START 0x00007ffffffff000
+#define VSPACE_LEVEL_BITS 9
+#else
+#error "Unsupported PT level"
+#endif
+
+#define VSPACE_MAP_PAGING_OBJECTS 5
+
+#define VSPACE_NUM_LEVELS CONFIG_PT_LEVELS
+
+#endif /* SEL4UTILS_SEL4_ARCH_VSPACE_H */

diff --git a/libsel4utils/sel4_arch_include/riscv32 b/libsel4utils/sel4_arch_include/riscv32
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4utils/sel4_arch_include/riscv32

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4utils/sel4_arch_include/riscv64 b/libsel4utils/sel4_arch_include/riscv64
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4utils/sel4_arch_include/riscv64

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4utils/src/arch/riscv/arch.c b/libsel4utils/src/arch/riscv/arch.c
new file mode 100644
index 0000000..ccb5c2e
--- /dev/null
+++ b/libsel4utils/src/arch/riscv/arch.c

@@ -0,0 +1,41 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#include <autoconf.h>
+#include <sel4/types.h>
+#include <sel4utils/thread.h>
+#include <stdbool.h>
+
+int
+sel4utils_arch_init_context(void *entry_point, void *stack_top, seL4_UserContext *context)
+{
+    //context->ra = (seL4_Word) entry_point;
+    context->sepc = (seL4_Word) entry_point;
+    context->sp = (seL4_Word) stack_top;
+    if ((uintptr_t) stack_top % (sizeof(seL4_Word) * 2) != 0) {
+        ZF_LOGE("Stack %p not aligned on double word boundary", stack_top);
+        return -1;
+    }
+    return 0;
+}
+
+int
+sel4utils_arch_init_context_with_args(void *entry_point, void *arg0, void *arg1, void *arg2,
+                            bool local_stack, void *stack_top, seL4_UserContext *context,
+                            vka_t *vka, vspace_t *local_vspace, vspace_t *remote_vspace)
+{
+    extern char __global_pointer$[];
+
+    context->a0 = (seL4_Word) arg0;
+    context->a1 = (seL4_Word) arg1;
+    context->a2 = (seL4_Word) arg2;
+    context->x3 = (seL4_Word) __global_pointer$;
+
+    return sel4utils_arch_init_context(entry_point, stack_top, context);
+}

diff --git a/libsel4utils/src/arch/riscv32 b/libsel4utils/src/arch/riscv32
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4utils/src/arch/riscv32

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4utils/src/arch/riscv64 b/libsel4utils/src/arch/riscv64
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4utils/src/arch/riscv64

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4utils/src/mapping.c b/libsel4utils/src/mapping.c
index 722d04f..ebc79e8 100644
--- a/libsel4utils/src/mapping.c
+++ b/libsel4utils/src/mapping.c

@@ -57,11 +57,24 @@
                 }
             }
         } else {
-            error = sel4utils_create_object_at_level(vka, failed_bits, objects, num_objects, vaddr, vspace_root);
+            error = sel4utils_create_object_at_level(vka, failed_bits, objects, num_objects, (seL4_Word) vaddr, vspace_root);
             if (error) {
                 /* log message printed out by sel4utils_create_object_at_level */
                 return error;
             }
+
+            error = vka_alloc_page_table(vka, &objects[*num_objects]);
+            if (error) {
+                ZF_LOGE("Page table allocation failed");
+                return error;
+            }
+            error = seL4_ARCH_PageTable_Map(objects[*num_objects].cptr, vspace_root, (seL4_Word)vaddr, seL4_ARCH_Default_VMAttributes);
+            (*num_objects)++;
+            if (error) {
+                ZF_LOGE("Failed to map page table %d", error);
+                return error;
+            }
+
         }
         error = seL4_ARCH_Page_Map(frame, vspace_root, (seL4_Word) vaddr, rights, attr);
     }

diff --git a/libsel4utils/src/sel4_arch/riscv/arch.c b/libsel4utils/src/sel4_arch/riscv/arch.c
new file mode 100644
index 0000000..de8c3c2
--- /dev/null
+++ b/libsel4utils/src/sel4_arch/riscv/arch.c

@@ -0,0 +1,40 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#include <autoconf.h>
+#include <sel4/types.h>
+#include <sel4utils/thread.h>
+#include <stdbool.h>
+
+int
+sel4utils_arch_init_context(void *entry_point, void *stack_top, seL4_UserContext *context)
+{
+    context->pc = (seL4_Word) entry_point;
+    context->sp = (seL4_Word) stack_top;
+    if ((uintptr_t) stack_top % (sizeof(seL4_Word) * 2) != 0) {
+        ZF_LOGE("Stack %p not aligned on double word boundary", stack_top);
+        return -1;
+    }
+    return 0;
+}
+
+int
+sel4utils_arch_init_context_with_args(void *entry_point, void *arg0, void *arg1, void *arg2,
+                            bool local_stack, void *stack_top, seL4_UserContext *context,
+                            vka_t *vka, vspace_t *local_vspace, vspace_t *remote_vspace)
+{
+    extern char __global_pointer$[];
+
+    context->a0 = (seL4_Word) arg0;
+    context->a1 = (seL4_Word) arg1;
+    context->a2 = (seL4_Word) arg2;
+    context->x3 = (seL4_Word) __global_pointer$;
+
+    return sel4utils_arch_init_context(entry_point, stack_top, context);
+}

diff --git a/libsel4utils/src/sel4_arch/riscv32 b/libsel4utils/src/sel4_arch/riscv32
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4utils/src/sel4_arch/riscv32

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4utils/src/sel4_arch/riscv64 b/libsel4utils/src/sel4_arch/riscv64
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4utils/src/sel4_arch/riscv64

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4utils/src/thread.c b/libsel4utils/src/thread.c
index 2b66821..e7aef3d 100644
--- a/libsel4utils/src/thread.c
+++ b/libsel4utils/src/thread.c

@@ -227,10 +227,10 @@
                COLOR_ERROR,
                thread_name,
                sel4utils_is_read_fault() ? "read" : "write",
-               seL4_Fault_VMFault_get_PrefetchFault(fault) ? "prefetch fault" : "fault",
+               "fault",
+               //seL4_Fault_VMFault_get_PrefetchFault(fault) ? "prefetch fault" : "fault",
                (void*)seL4_Fault_VMFault_get_IP(fault),
                (void*)seL4_Fault_VMFault_get_Addr(fault),
-               (void *)seL4_Fault_VMFault_get_FSR(fault),
                COLOR_NORMAL);
         break;
 

diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c
index 336e234..264c777 100644
--- a/libsel4utils/src/vspace/bootstrap.c
+++ b/libsel4utils/src/vspace/bootstrap.c

@@ -222,10 +222,10 @@
 void
 sel4utils_get_image_region(uintptr_t *va_start, uintptr_t *va_end)
 {
-    extern char __executable_start[];
+    extern char _start[];
     extern char _end[];
 
-    *va_start = (uintptr_t) __executable_start;
+    *va_start = (uintptr_t) _start;
     *va_end = (uintptr_t) _end;
     *va_end = (uintptr_t) ROUND_UP(*va_end, PAGE_SIZE_4K);
 }

diff --git a/libsel4vka/arch_include/riscv/vka/arch/kobject_t.h b/libsel4vka/arch_include/riscv/vka/arch/kobject_t.h
new file mode 100644
index 0000000..2e4a5f2
--- /dev/null
+++ b/libsel4vka/arch_include/riscv/vka/arch/kobject_t.h

@@ -0,0 +1,71 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _ARCH_KOBJECT_T_H_
+#define _ARCH_KOBJECT_T_H_
+
+#include <sel4/types.h>
+#include <assert.h>
+#include <autoconf.h>
+#include <utils/util.h>
+#include <vka/sel4_arch/kobject_t.h>
+
+enum _riscv_kobject_type {
+    KOBJECT_IO_PAGETABLE = KOBJECT_MODE_NUM_TYPES,
+    KOBJECT_PAGE_DIRECTORY,
+    KOBJECT_PAGE_TABLE,
+    KOBJECT_ARCH_NUM_TYPES,
+};
+
+/*
+ * Get the size (in bits) of the untyped memory required to
+ * create an object of the given size.
+ */
+static inline seL4_Word
+arch_kobject_get_size(kobject_t type, seL4_Word objectSize)
+{
+    switch (type) {
+    case KOBJECT_FRAME:
+        switch (objectSize) {
+        case seL4_PageBits:
+        case seL4_LargePageBits:
+            return objectSize;
+        }
+        /* If frame size was unknown fall through to default case as it
+         * might be a mode specific frame size */
+    default:
+        return riscv_mode_kobject_get_size(type, objectSize);
+    }
+}
+
+
+static inline seL4_Word
+arch_kobject_get_type(int type, seL4_Word objectSize)
+{
+    switch (type) {
+    case KOBJECT_PAGE_DIRECTORY:
+    case KOBJECT_PAGE_TABLE:
+        return seL4_RISCV_PageTableObject;
+    case KOBJECT_FRAME:
+        switch (objectSize) {
+        case seL4_PageBits:
+            return seL4_RISCV_4K_Page;
+        case seL4_LargePageBits:
+            return seL4_RISCV_Mega_Page;
+        default:
+            return riscv_mode_kobject_get_type(type, objectSize);
+        }
+    default:
+        return riscv_mode_kobject_get_type(type, objectSize);
+    }
+}
+
+
+#endif /* _ARCH_KOBJECT_T_H_ */

diff --git a/libsel4vka/arch_include/riscv/vka/arch/object.h b/libsel4vka/arch_include/riscv/vka/arch/object.h
new file mode 100644
index 0000000..e8ae0b3
--- /dev/null
+++ b/libsel4vka/arch_include/riscv/vka/arch/object.h

@@ -0,0 +1,50 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _VKA_ARCH_OBJECT_H__
+#define _VKA_ARCH_OBJECT_H__
+
+#include <vka/vka.h>
+#include <vka/kobject_t.h>
+#include <utils/util.h>
+#include <vka/sel4_arch/object.h>
+
+static inline int vka_alloc_io_page_table(vka_t *vka, vka_object_t *result)
+{
+    return 0; /* Not supported */
+}
+
+LEAKY(io_page_table)
+
+static inline unsigned long
+vka_arch_get_object_size(seL4_Word objectType)
+{
+    switch (objectType) {
+    case seL4_RISCV_4K_Page:
+        return seL4_PageBits;
+    case seL4_RISCV_Mega_Page:
+        return seL4_LargePageBits;
+#if CONFIG_PT_LEVELS > 2
+    case seL4_RISCV_Giga_Page:
+        return seL4_HugePageBits;
+#endif
+#if CONFIG_PT_LEVELS > 3
+    case seL4_RISCV_Tera_Page:
+        return seL4_TeraPageBits;
+#endif
+    case seL4_RISCV_PageTableObject:
+        return seL4_PageTableBits;
+
+    default:
+        return vka_riscv_mode_get_object_size(objectType);
+    }
+}
+
+#endif /* _VKA_ARCH_OBJECT_H__ */

diff --git a/libsel4vka/arch_include/riscv32/vka/arch/kobject_t.h b/libsel4vka/arch_include/riscv32/vka/arch/kobject_t.h
new file mode 100644
index 0000000..2e4a5f2
--- /dev/null
+++ b/libsel4vka/arch_include/riscv32/vka/arch/kobject_t.h

@@ -0,0 +1,71 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _ARCH_KOBJECT_T_H_
+#define _ARCH_KOBJECT_T_H_
+
+#include <sel4/types.h>
+#include <assert.h>
+#include <autoconf.h>
+#include <utils/util.h>
+#include <vka/sel4_arch/kobject_t.h>
+
+enum _riscv_kobject_type {
+    KOBJECT_IO_PAGETABLE = KOBJECT_MODE_NUM_TYPES,
+    KOBJECT_PAGE_DIRECTORY,
+    KOBJECT_PAGE_TABLE,
+    KOBJECT_ARCH_NUM_TYPES,
+};
+
+/*
+ * Get the size (in bits) of the untyped memory required to
+ * create an object of the given size.
+ */
+static inline seL4_Word
+arch_kobject_get_size(kobject_t type, seL4_Word objectSize)
+{
+    switch (type) {
+    case KOBJECT_FRAME:
+        switch (objectSize) {
+        case seL4_PageBits:
+        case seL4_LargePageBits:
+            return objectSize;
+        }
+        /* If frame size was unknown fall through to default case as it
+         * might be a mode specific frame size */
+    default:
+        return riscv_mode_kobject_get_size(type, objectSize);
+    }
+}
+
+
+static inline seL4_Word
+arch_kobject_get_type(int type, seL4_Word objectSize)
+{
+    switch (type) {
+    case KOBJECT_PAGE_DIRECTORY:
+    case KOBJECT_PAGE_TABLE:
+        return seL4_RISCV_PageTableObject;
+    case KOBJECT_FRAME:
+        switch (objectSize) {
+        case seL4_PageBits:
+            return seL4_RISCV_4K_Page;
+        case seL4_LargePageBits:
+            return seL4_RISCV_Mega_Page;
+        default:
+            return riscv_mode_kobject_get_type(type, objectSize);
+        }
+    default:
+        return riscv_mode_kobject_get_type(type, objectSize);
+    }
+}
+
+
+#endif /* _ARCH_KOBJECT_T_H_ */

diff --git a/libsel4vka/arch_include/riscv32/vka/arch/object.h b/libsel4vka/arch_include/riscv32/vka/arch/object.h
new file mode 100644
index 0000000..e8ae0b3
--- /dev/null
+++ b/libsel4vka/arch_include/riscv32/vka/arch/object.h

@@ -0,0 +1,50 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _VKA_ARCH_OBJECT_H__
+#define _VKA_ARCH_OBJECT_H__
+
+#include <vka/vka.h>
+#include <vka/kobject_t.h>
+#include <utils/util.h>
+#include <vka/sel4_arch/object.h>
+
+static inline int vka_alloc_io_page_table(vka_t *vka, vka_object_t *result)
+{
+    return 0; /* Not supported */
+}
+
+LEAKY(io_page_table)
+
+static inline unsigned long
+vka_arch_get_object_size(seL4_Word objectType)
+{
+    switch (objectType) {
+    case seL4_RISCV_4K_Page:
+        return seL4_PageBits;
+    case seL4_RISCV_Mega_Page:
+        return seL4_LargePageBits;
+#if CONFIG_PT_LEVELS > 2
+    case seL4_RISCV_Giga_Page:
+        return seL4_HugePageBits;
+#endif
+#if CONFIG_PT_LEVELS > 3
+    case seL4_RISCV_Tera_Page:
+        return seL4_TeraPageBits;
+#endif
+    case seL4_RISCV_PageTableObject:
+        return seL4_PageTableBits;
+
+    default:
+        return vka_riscv_mode_get_object_size(objectType);
+    }
+}
+
+#endif /* _VKA_ARCH_OBJECT_H__ */

diff --git a/libsel4vka/arch_include/riscv64/vka/arch/kobject_t.h b/libsel4vka/arch_include/riscv64/vka/arch/kobject_t.h
new file mode 100644
index 0000000..2e4a5f2
--- /dev/null
+++ b/libsel4vka/arch_include/riscv64/vka/arch/kobject_t.h

@@ -0,0 +1,71 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _ARCH_KOBJECT_T_H_
+#define _ARCH_KOBJECT_T_H_
+
+#include <sel4/types.h>
+#include <assert.h>
+#include <autoconf.h>
+#include <utils/util.h>
+#include <vka/sel4_arch/kobject_t.h>
+
+enum _riscv_kobject_type {
+    KOBJECT_IO_PAGETABLE = KOBJECT_MODE_NUM_TYPES,
+    KOBJECT_PAGE_DIRECTORY,
+    KOBJECT_PAGE_TABLE,
+    KOBJECT_ARCH_NUM_TYPES,
+};
+
+/*
+ * Get the size (in bits) of the untyped memory required to
+ * create an object of the given size.
+ */
+static inline seL4_Word
+arch_kobject_get_size(kobject_t type, seL4_Word objectSize)
+{
+    switch (type) {
+    case KOBJECT_FRAME:
+        switch (objectSize) {
+        case seL4_PageBits:
+        case seL4_LargePageBits:
+            return objectSize;
+        }
+        /* If frame size was unknown fall through to default case as it
+         * might be a mode specific frame size */
+    default:
+        return riscv_mode_kobject_get_size(type, objectSize);
+    }
+}
+
+
+static inline seL4_Word
+arch_kobject_get_type(int type, seL4_Word objectSize)
+{
+    switch (type) {
+    case KOBJECT_PAGE_DIRECTORY:
+    case KOBJECT_PAGE_TABLE:
+        return seL4_RISCV_PageTableObject;
+    case KOBJECT_FRAME:
+        switch (objectSize) {
+        case seL4_PageBits:
+            return seL4_RISCV_4K_Page;
+        case seL4_LargePageBits:
+            return seL4_RISCV_Mega_Page;
+        default:
+            return riscv_mode_kobject_get_type(type, objectSize);
+        }
+    default:
+        return riscv_mode_kobject_get_type(type, objectSize);
+    }
+}
+
+
+#endif /* _ARCH_KOBJECT_T_H_ */

diff --git a/libsel4vka/arch_include/riscv64/vka/arch/object.h b/libsel4vka/arch_include/riscv64/vka/arch/object.h
new file mode 100644
index 0000000..e8ae0b3
--- /dev/null
+++ b/libsel4vka/arch_include/riscv64/vka/arch/object.h

@@ -0,0 +1,50 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _VKA_ARCH_OBJECT_H__
+#define _VKA_ARCH_OBJECT_H__
+
+#include <vka/vka.h>
+#include <vka/kobject_t.h>
+#include <utils/util.h>
+#include <vka/sel4_arch/object.h>
+
+static inline int vka_alloc_io_page_table(vka_t *vka, vka_object_t *result)
+{
+    return 0; /* Not supported */
+}
+
+LEAKY(io_page_table)
+
+static inline unsigned long
+vka_arch_get_object_size(seL4_Word objectType)
+{
+    switch (objectType) {
+    case seL4_RISCV_4K_Page:
+        return seL4_PageBits;
+    case seL4_RISCV_Mega_Page:
+        return seL4_LargePageBits;
+#if CONFIG_PT_LEVELS > 2
+    case seL4_RISCV_Giga_Page:
+        return seL4_HugePageBits;
+#endif
+#if CONFIG_PT_LEVELS > 3
+    case seL4_RISCV_Tera_Page:
+        return seL4_TeraPageBits;
+#endif
+    case seL4_RISCV_PageTableObject:
+        return seL4_PageTableBits;
+
+    default:
+        return vka_riscv_mode_get_object_size(objectType);
+    }
+}
+
+#endif /* _VKA_ARCH_OBJECT_H__ */

diff --git a/libsel4vka/include/vka/kobject_t.h b/libsel4vka/include/vka/kobject_t.h
index e01d2b7..4199d2b 100644
--- a/libsel4vka/include/vka/kobject_t.h
+++ b/libsel4vka/include/vka/kobject_t.h

@@ -61,7 +61,7 @@
     case KOBJECT_NOTIFICATION:
         return seL4_EndpointBits;
     case KOBJECT_PAGE_DIRECTORY:
-        return seL4_PageDirBits;
+        return seL4_PageTableBits;
     case KOBJECT_PAGE_TABLE:
         return seL4_PageTableBits;
 #ifdef CONFIG_KERNEL_RT

diff --git a/libsel4vka/include/vka/object.h b/libsel4vka/include/vka/object.h
index 8635c7c..73bf300 100644
--- a/libsel4vka/include/vka/object.h
+++ b/libsel4vka/include/vka/object.h

@@ -222,7 +222,7 @@
 
 static inline int vka_alloc_page_directory(vka_t *vka, vka_object_t *result)
 {
-    return vka_alloc_object(vka, kobject_get_type(KOBJECT_PAGE_DIRECTORY, 0), seL4_PageDirBits, result);
+    return vka_alloc_object(vka, kobject_get_type(KOBJECT_PAGE_DIRECTORY, 0), seL4_PageTableBits, result);
 }
 
 static inline int vka_alloc_page_table(vka_t *vka, vka_object_t *result)

diff --git a/libsel4vka/sel4_arch_include/riscv/vka/sel4_arch/kobject_t.h b/libsel4vka/sel4_arch_include/riscv/vka/sel4_arch/kobject_t.h
new file mode 100644
index 0000000..6432ab7
--- /dev/null
+++ b/libsel4vka/sel4_arch_include/riscv/vka/sel4_arch/kobject_t.h

@@ -0,0 +1,66 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _SEL4_ARCH_KOBJECT_T_H_
+#define _SEL4_ARCH_KOBJECT_T_H_
+
+#include <sel4/types.h>
+#include <assert.h>
+#include <autoconf.h>
+#include <utils/util.h>
+
+enum _riscv_mode_kobject_type {
+    KOBJECT_FRAME,
+    KOBJECT_MODE_NUM_TYPES,
+};
+
+typedef int kobject_t;
+
+/*
+ * Get the size (in bits) of the untyped memory required to
+ * create an object of the given size.
+ */
+static inline seL4_Word
+riscv_mode_kobject_get_size(kobject_t type, seL4_Word objectSize)
+{
+    switch (type) {
+    default:
+        ZF_LOGE("Uknown object type");
+        return 0;
+    }
+}
+
+
+static inline seL4_Word
+riscv_mode_kobject_get_type(kobject_t type, seL4_Word objectSize)
+{
+    switch (type) {
+    case KOBJECT_FRAME:
+        switch (objectSize) {
+#if CONFIG_PT_LEVELS > 2
+        case seL4_HugePageBits:
+            return seL4_RISCV_Giga_Page;
+#endif
+#if CONFIG_PT_LEVEL > 3
+        case seL4_TeraPageBits:
+            return seL4_RISCV_Tera_Page;
+#endif
+        default:
+            return -1;
+        }
+    default:
+        /* Unknown object type. */
+        ZF_LOGE("Unknown object type %d", type);
+        return -1;
+    }
+}
+
+
+#endif /* _SEL4_ARCH_KOBJECT_T_H_ */

diff --git a/libsel4vka/sel4_arch_include/riscv/vka/sel4_arch/object.h b/libsel4vka/sel4_arch_include/riscv/vka/sel4_arch/object.h
new file mode 100644
index 0000000..f8610be
--- /dev/null
+++ b/libsel4vka/sel4_arch_include/riscv/vka/sel4_arch/object.h

@@ -0,0 +1,45 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+
+#ifndef _VKA_SEL4_ARCH_OBJECT_H__
+#define _VKA_SEL4_ARCH_OBJECT_H__
+
+#include <vka/vka.h>
+#include <vka/kobject_t.h>
+#include <utils/util.h>
+
+/*
+static inline int vka_alloc_pd(vka_t *vka, vka_object_t *result)
+{
+    return vka_alloc_object(vka, kobject_get_type(KOBJECT_PAGE_DIRECTORY, 0), seL4_PageTableBits, result);
+}
+*/
+static inline int vka_alloc_pd(vka_t *vka, vka_object_t *result)
+{
+    return vka_alloc_object(vka, kobject_get_type(KOBJECT_PAGE_TABLE, 0), seL4_PageTableBits, result);
+}
+
+static inline int vka_alloc_vspace_root(vka_t *vka, vka_object_t *result)
+{
+    return vka_alloc_pd(vka, result);
+}
+
+static inline unsigned long
+vka_riscv_mode_get_object_size(seL4_Word objectType)
+{
+    switch (objectType) {
+    default:
+        /* Unknown object type. */
+        ZF_LOGF("Unknown object type %ld", (long)objectType);
+        return -1;
+    }
+}
+
+#endif /* _VKA_SEL4_ARCH_OBJECT_H__ */

diff --git a/libsel4vka/sel4_arch_include/riscv32 b/libsel4vka/sel4_arch_include/riscv32
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4vka/sel4_arch_include/riscv32

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4vka/sel4_arch_include/riscv64 b/libsel4vka/sel4_arch_include/riscv64
new file mode 120000
index 0000000..4847a64
--- /dev/null
+++ b/libsel4vka/sel4_arch_include/riscv64

@@ -0,0 +1 @@
+riscv
\ No newline at end of file

diff --git a/libsel4vspace/arch_include/riscv/vspace/arch/page.h b/libsel4vspace/arch_include/riscv/vspace/arch/page.h
new file mode 100644
index 0000000..19915fa
--- /dev/null
+++ b/libsel4vspace/arch_include/riscv/vspace/arch/page.h

@@ -0,0 +1,47 @@
+/*
+ * Copyright 2016, NICTA
+ *
+ * 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(NICTA_BSD)
+ */
+#ifndef _VSPACE_ARCH_PAGE_H
+#define _VSPACE_ARCH_PAGE_H
+
+#include <autoconf.h>
+#include <stddef.h>
+#include <utils/attribute.h>
+#include <sel4/sel4_arch/constants.h>
+
+/* ordered list of page sizes for this architecture */
+static const UNUSED size_t sel4_page_sizes[] = {
+    seL4_PageBits,
+    seL4_LargePageBits,
+#if CONFIG_PT_LEVEL > 2
+    seL4_HugePageBits,
+#endif
+#if CONFIG_PT_LEVEL > 3
+    seL4_TeraPageBits,
+#endif
+};
+
+#define seL4_ARCH_Page_Map             seL4_RISCV_Page_Map
+#define seL4_ARCH_Page_Unmap           seL4_RISCV_Page_Unmap
+#define seL4_ARCH_PageTable_Map        seL4_RISCV_PageTable_Map
+#define seL4_ARCH_PageTable_Unmap      seL4_RISCV_PageTable_Unmap
+#define seL4_ARCH_ASIDPool_Assign      seL4_RISCV_ASIDPool_Assign
+#define seL4_ARCH_ASIDControl_MakePool seL4_RISCV_ASIDControl_MakePool
+#define seL4_ARCH_PageTableObject      seL4_RISCV_PageTableObject
+#define seL4_ARCH_PageDirectoryObject  seL4_RISCV_PageTableObject
+#define seL4_ARCH_Default_VMAttributes seL4_RISCV_Default_VMAttributes
+#define seL4_ARCH_VMAttributes         seL4_RISCV_VMAttributes
+#define seL4_ARCH_4KPage               seL4_RISCV_4K_Page
+#define seL4_ARCH_Uncached_VMAttributes 0
+#define seL4_ARCH_LargePageObject      seL4_RISCV_Mega_Page
+/* for size of a large page object use seL4_LargePageBits */
+/* Remap does not exist on all kernels */
+#define seL4_ARCH_Page_Remap           seL4_RISCV_Page_Remap
+
+#endif /* _VSPACE_ARCH_PAGE_H */