diff --git a/Kconfig b/Kconfig
index 84863f4ea..f5233749b 100644
--- a/Kconfig
+++ b/Kconfig
@@ -359,7 +359,7 @@ menu "Build Options"
         help
             Do not enable branch prediction (also called program flow control)
             on startup. This makes execution time more deterministic at the
-            expense of drammatically decreasing performance. Primary use is for
+            expense of dramatically decreasing performance. Primary use is for
             debugging.
 
 endmenu
diff --git a/README b/README
index b6c9cb054..d793f687b 100644
--- a/README
+++ b/README
@@ -19,8 +19,8 @@ build using make, follow these instructions:
 
  * Ensure that the appropriate cross-compiler is installed.
 
- * Set the TOOLPREFIX environment variable.  eg. arm-none-eabi- if the ERTOS
-   compilers are in your PATH.
+ * Set the TOOLPREFIX environment variable to your cross-compiler's prefix. E.g.
+   arm-none-eabi-.
 
  * Set the ARCH, PLAT, ARMV and CPU variables for the intended target
    architecture and platform, chosen from the following lists:
@@ -32,4 +32,4 @@ build using make, follow these instructions:
     arm    am335x  armv7-a   cortex-a8
     ia32   pc99
 
- * For a debug build, append -DDEBUG.
+ * For a debug build, append "DEBUG=y".
diff --git a/include/arch/arm/arch/kernel/vspace.h b/include/arch/arm/arch/kernel/vspace.h
index 59525b6de..2e6e703e4 100644
--- a/include/arch/arm/arch/kernel/vspace.h
+++ b/include/arch/arm/arch/kernel/vspace.h
@@ -87,12 +87,12 @@ exception_t decodeARMMMUInvocation(word_t label, unsigned int length, cptr_t cpt
 exception_t performPageTableInvocationMap(cap_t cap, cte_t *ctSlot,
                                           pde_t pde, pde_t *pdSlot);
 exception_t performPageTableInvocationUnmap(cap_t cap, cte_t *ctSlot);
-exception_t performPageInvocationMapPTE(cap_t cap, cte_t *ctSlot,
+exception_t performPageInvocationMapPTE(asid_t asid, cap_t cap, cte_t *ctSlot,
                                         pte_t pte, pte_range_t pte_entries);
-exception_t performPageInvocationMapPDE(cap_t cap, cte_t *ctSlot,
+exception_t performPageInvocationMapPDE(asid_t asid, cap_t cap, cte_t *ctSlot,
                                         pde_t pde, pde_range_t pde_entries);
-exception_t performPageInvocationRemapPTE(pte_t pte, pte_range_t pte_entries);
-exception_t performPageInvocationRemapPDE(pde_t pde, pde_range_t pde_entries);
+exception_t performPageInvocationRemapPTE(asid_t asid, pte_t pte, pte_range_t pte_entries);
+exception_t performPageInvocationRemapPDE(asid_t asid, pde_t pde, pde_range_t pde_entries);
 exception_t performPageInvocationUnmap(cap_t cap, cte_t *ctSlot);
 exception_t performASIDControlInvocation(void *frame, cte_t *slot,
                                          cte_t *parent, asid_t base);
diff --git a/src/arch/arm/kernel/vspace.c b/src/arch/arm/kernel/vspace.c
index aa5095e81..b1a2f4b2e 100644
--- a/src/arch/arm/kernel/vspace.c
+++ b/src/arch/arm/kernel/vspace.c
@@ -65,6 +65,9 @@ static exception_t decodeARMPageDirectoryInvocation(word_t label,
                                                     extra_caps_t extraCaps, word_t *buffer);
 static pde_t PURE loadHWASID(asid_t asid);
 
+static bool_t PURE pteCheckIfMapped(pte_t *pte);
+static bool_t PURE pdeCheckIfMapped(pde_t *pde);
+
 static word_t CONST
 APFromVMRights(vm_rights_t vm_rights)
 {
@@ -1456,7 +1459,7 @@ decodeARMFrameInvocation(word_t label, unsigned int length,
             }
 
             setThreadState(ksCurThread, ThreadState_Restart);
-            return performPageInvocationMapPTE(cap, cte,
+            return performPageInvocationMapPTE(asid, cap, cte,
                                                map_ret.pte,
                                                map_ret.pte_entries);
         } else {
@@ -1469,7 +1472,7 @@ decodeARMFrameInvocation(word_t label, unsigned int length,
             }
 
             setThreadState(ksCurThread, ThreadState_Restart);
-            return performPageInvocationMapPDE(cap, cte,
+            return performPageInvocationMapPDE(asid, cap, cte,
                                                map_ret.pde,
                                                map_ret.pde_entries);
         }
@@ -1480,6 +1483,7 @@ decodeARMFrameInvocation(word_t label, unsigned int length,
         paddr_t capFBasePtr;
         cap_t pdCap;
         pde_t *pd;
+        asid_t mappedASID;
         vm_rights_t capVMRights, vmRights;
         vm_page_size_t frameSize;
         vm_attributes_t attr;
@@ -1517,7 +1521,6 @@ decodeARMFrameInvocation(word_t label, unsigned int length,
 
         {
             findPDForASID_ret_t find_ret;
-            asid_t mappedASID;
 
             mappedASID = generic_frame_cap_get_capFMappedASID(cap);
 
@@ -1566,7 +1569,7 @@ decodeARMFrameInvocation(word_t label, unsigned int length,
             }
 
             setThreadState(ksCurThread, ThreadState_Restart);
-            return performPageInvocationRemapPTE(map_ret.pte,
+            return performPageInvocationRemapPTE(mappedASID, map_ret.pte,
                                                  map_ret.pte_entries);
         } else {
             create_mappings_pde_return_t map_ret;
@@ -1578,7 +1581,7 @@ decodeARMFrameInvocation(word_t label, unsigned int length,
             }
 
             setThreadState(ksCurThread, ThreadState_Restart);
-            return performPageInvocationRemapPDE(map_ret.pde,
+            return performPageInvocationRemapPDE(mappedASID, map_ret.pde,
                                                  map_ret.pde_entries);
         }
     }
@@ -2005,46 +2008,79 @@ performPageTableInvocationUnmap(cap_t cap, cte_t *ctSlot)
     return EXCEPTION_NONE;
 }
 
+static bool_t PURE
+pteCheckIfMapped(pte_t *pte)
+{
+    return pte_ptr_get_pteType(pte) != pte_pte_invalid;
+}
+
+static bool_t PURE
+pdeCheckIfMapped(pde_t *pde)
+{
+    return pde_ptr_get_pdeType(pde) != pde_pde_invalid;
+}
+
 exception_t
-performPageInvocationMapPTE(cap_t cap, cte_t *ctSlot, pte_t pte,
+performPageInvocationMapPTE(asid_t asid, cap_t cap, cte_t *ctSlot, pte_t pte,
                             pte_range_t pte_entries)
 {
     unsigned int i;
+    bool_t tlbflush_required;
 
     ctSlot->cap = cap;
 
+    /* we only need to check the first entries because of how createSafeMappingEntries
+     * works to preserve the consistency of tables */
+    tlbflush_required = pteCheckIfMapped(pte_entries.base);
+
     for (i = 0; i < pte_entries.length; i++) {
         pte_entries.base[i] = pte;
     }
     cleanCacheRange_PoU((word_t)pte_entries.base,
                         LAST_BYTE_PTE(pte_entries.base, pte_entries.length),
                         addrFromPPtr(pte_entries.base));
+    if (unlikely(tlbflush_required)) {
+        invalidateTLBByASID(asid);
+    }
 
     return EXCEPTION_NONE;
 }
 
 exception_t
-performPageInvocationMapPDE(cap_t cap, cte_t *ctSlot, pde_t pde,
+performPageInvocationMapPDE(asid_t asid, cap_t cap, cte_t *ctSlot, pde_t pde,
                             pde_range_t pde_entries)
 {
     unsigned int i;
+    bool_t tlbflush_required;
 
     ctSlot->cap = cap;
 
+    /* we only need to check the first entries because of how createSafeMappingEntries
+     * works to preserve the consistency of tables */
+    tlbflush_required = pdeCheckIfMapped(pde_entries.base);
+
     for (i = 0; i < pde_entries.length; i++) {
         pde_entries.base[i] = pde;
     }
     cleanCacheRange_PoU((word_t)pde_entries.base,
                         LAST_BYTE_PDE(pde_entries.base, pde_entries.length),
                         addrFromPPtr(pde_entries.base));
+    if (unlikely(tlbflush_required)) {
+        invalidateTLBByASID(asid);
+    }
 
     return EXCEPTION_NONE;
 }
 
 exception_t
-performPageInvocationRemapPTE(pte_t pte, pte_range_t pte_entries)
+performPageInvocationRemapPTE(asid_t asid, pte_t pte, pte_range_t pte_entries)
 {
     unsigned int i;
+    bool_t tlbflush_required;
+
+    /* we only need to check the first entries because of how createSafeMappingEntries
+     * works to preserve the consistency of tables */
+    tlbflush_required = pteCheckIfMapped(pte_entries.base);
 
     for (i = 0; i < pte_entries.length; i++) {
         pte_entries.base[i] = pte;
@@ -2052,14 +2088,22 @@ performPageInvocationRemapPTE(pte_t pte, pte_range_t pte_entries)
     cleanCacheRange_PoU((word_t)pte_entries.base,
                         LAST_BYTE_PTE(pte_entries.base, pte_entries.length),
                         addrFromPPtr(pte_entries.base));
+    if (unlikely(tlbflush_required)) {
+        invalidateTLBByASID(asid);
+    }
 
     return EXCEPTION_NONE;
 }
 
 exception_t
-performPageInvocationRemapPDE(pde_t pde, pde_range_t pde_entries)
+performPageInvocationRemapPDE(asid_t asid, pde_t pde, pde_range_t pde_entries)
 {
     unsigned int i;
+    bool_t tlbflush_required;
+
+    /* we only need to check the first entries because of how createSafeMappingEntries
+     * works to preserve the consistency of tables */
+    tlbflush_required = pdeCheckIfMapped(pde_entries.base);
 
     for (i = 0; i < pde_entries.length; i++) {
         pde_entries.base[i] = pde;
@@ -2067,6 +2111,9 @@ performPageInvocationRemapPDE(pde_t pde, pde_range_t pde_entries)
     cleanCacheRange_PoU((word_t)pde_entries.base,
                         LAST_BYTE_PDE(pde_entries.base, pde_entries.length),
                         addrFromPPtr(pde_entries.base));
+    if (unlikely(tlbflush_required)) {
+        invalidateTLBByASID(asid);
+    }
 
     return EXCEPTION_NONE;
 }
diff --git a/src/arch/ia32/kernel/vspace.c b/src/arch/ia32/kernel/vspace.c
index ed42f22d7..65e3344b2 100644
--- a/src/arch/ia32/kernel/vspace.c
+++ b/src/arch/ia32/kernel/vspace.c
@@ -1634,7 +1634,6 @@ decodeIA32FrameInvocation(
 
             lu_ret = lookupPTSlot(pd, vaddr);
             if (lu_ret.status != EXCEPTION_NONE) {
-                userError("IA32FrameMap: Need a page table first.");
                 current_syscall_error.type = seL4_FailedLookup;
                 current_syscall_error.failedLookupWasSource = false;
                 /* current_lookup_fault will have been set by lookupPTSlot */
diff --git a/src/object/interrupt.c b/src/object/interrupt.c
index 8a95e57aa..b04a079ec 100644
--- a/src/object/interrupt.c
+++ b/src/object/interrupt.c
@@ -112,6 +112,11 @@ decodeIRQHandlerInvocation(word_t label, irq_t irq,
 
         if (cap_get_capType(aepCap) != cap_async_endpoint_cap ||
                 !cap_async_endpoint_cap_get_capAEPCanSend(aepCap)) {
+            if (cap_get_capType(aepCap) != cap_async_endpoint_cap) {
+                userError("IRQSetHandler: provided cap is not an async endpoint capablity.");
+            } else {
+                userError("IRQSetHandler: caller does not have send rights on the endpoint.");
+            }
             current_syscall_error.type = seL4_InvalidCapability;
             current_syscall_error.invalidCapNumber = 0;
             return EXCEPTION_SYSCALL_ERROR;
diff --git a/src/plat/exynos_common/mct.c b/src/plat/exynos_common/mct.c
index ead338a5b..e00d2c36c 100644
--- a/src/plat/exynos_common/mct.c
+++ b/src/plat/exynos_common/mct.c
@@ -75,8 +75,9 @@ struct mct_global_map {
     uint32_t reserved0[64];
     uint32_t cntl;           /* 0x100 Low word of count */
     uint32_t cnth;           /* 0x104 High word of count */
+    uint32_t reserved1[1];
     uint32_t cnt_wstat;      /* 0x110 Write status for cnt */
-    uint32_t reserved1[61];
+    uint32_t reserved2[60];
 
     uint32_t comp0l;         /* 0x200 Low word of Compare value */
     uint32_t comp0h;         /* 0x204 High word of Compare value*/