diff --git a/include/arch/arm/arch/machine/gic_common.h b/include/arch/arm/arch/machine/gic_common.h
index f58cac35a8..d3fd24e0b7 100644
--- a/include/arch/arm/arch/machine/gic_common.h
+++ b/include/arch/arm/arch/machine/gic_common.h
@@ -72,8 +72,52 @@ irq_t irqInvalid = (uint16_t) -1;
  */
 extern word_t active_irq[CONFIG_MAX_NUM_NODES];
 
+static inline irq_t getActiveIRQ(void)
+{
+    word_t cur_core = CURRENT_CPU_INDEX();
+    word_t *active_irq_slot = &active_irq[cur_core];
+
+    irq_t irq = *active_irq_slot;
+    if (!IS_IRQ_VALID(irq)) {
+        /* Our slot is empty, check hardware if a new interrupt is pending. */
+        irq = get_gic_pending_interrupt();
+        if (!IS_IRQ_VALID(irq)) {
+            /* There is no interrupt pending, */
+            return irqInvalid;
+        }
+        /* Put the new interrupt into our slot. */
+        *active_irq_slot = irq;
+    }
+    return CORE_IRQ_TO_IRQT(cur_core, irq & IRQ_MASK);
+}
+
+static inline void ackInterrupt(irq_t irq)
+{
+    word_t cur_core = CURRENT_CPU_INDEX();
+    word_t *active_irq_slot = &active_irq[cur_core];
+
+    irq_t irq = *active_irq_slot;
+    if (!IS_IRQ_VALID(irq)) {
+        /* This is not supposed to happen. */
+        printf("WARNING: can't ack invalid IRQ %d\n", irq);
+        return;
+    }
+
+    word_t hw_irq = IRQT_TO_IRQ(irq);
+    if ((irq & IRQ_MASK) != hw_irq) {
+        /* The ack does not match the interrupt currently pending. */
+        printf("WARNING: ack IRQ %d differs from pending IRQ %d\n", irq, hw_irq);
+        hw_irq = irq;
+        return;
+    }
+
+    gic_ack_interrupt(hw_irq);
+    *active_irq_slot = IRQ_NONE;
+}
+
 static inline void handleSpuriousIRQ(void)
 {
+    /* Nothing to do here */
 }
 
 void initIRQController(void);
diff --git a/include/arch/arm/arch/machine/gic_v2.h b/include/arch/arm/arch/machine/gic_v2.h
index 8114629bfe..083371da2f 100644
--- a/include/arch/arm/arch/machine/gic_v2.h
+++ b/include/arch/arm/arch/machine/gic_v2.h
@@ -141,20 +141,9 @@ static inline void dist_enable_set(word_t irq)
     gic_dist->enable_set[word] = BIT(bit);
 }
 
-static inline irq_t getActiveIRQ(void)
+static inline irq_t get_gic_pending_interrupt(void)
 {
-    irq_t irq;
-    if (!IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])) {
-        active_irq[CURRENT_CPU_INDEX()] = gic_cpuiface->int_ack;
-    }
-
-    if (IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])) {
-        irq = CORE_IRQ_TO_IRQT(CURRENT_CPU_INDEX(), active_irq[CURRENT_CPU_INDEX()] & IRQ_MASK);
-    } else {
-        irq = irqInvalid;
-    }
-
-    return irq;
+    return gic_cpuiface->int_ack;
 }
 
 /*
@@ -179,13 +168,9 @@ static inline void maskInterrupt(bool_t disable, irq_t irq)
     }
 }
 
-static inline void ackInterrupt(irq_t irq)
+static inline void gic_ack_interrupt(irq_t irq)
 {
-    assert(IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])
-           && (active_irq[CURRENT_CPU_INDEX()] & IRQ_MASK) == IRQT_TO_IRQ(irq));
-    gic_cpuiface->eoi = active_irq[CURRENT_CPU_INDEX()];
-    active_irq[CURRENT_CPU_INDEX()] = IRQ_NONE;
-
+    gic_cpuiface->eoi = irq;
 }
 
 
diff --git a/include/arch/arm/arch/machine/gic_v3.h b/include/arch/arm/arch/machine/gic_v3.h
index 6d6ffd2b39..b5306c809a 100644
--- a/include/arch/arm/arch/machine/gic_v3.h
+++ b/include/arch/arm/arch/machine/gic_v3.h
@@ -260,23 +260,11 @@ static inline void gic_enable_set(word_t irq)
 
 }
 
-static inline irq_t getActiveIRQ(void)
+static inline irq_t get_gic_pending_interrupt(void)
 {
-    irq_t irq;
-
-    if (!IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])) {
-        uint32_t val = 0;
-        SYSTEM_READ_WORD(ICC_IAR1_EL1, val);
-        active_irq[CURRENT_CPU_INDEX()] = val;
-    }
-
-    if (IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])) {
-        irq = CORE_IRQ_TO_IRQT(CURRENT_CPU_INDEX(), active_irq[CURRENT_CPU_INDEX()] & IRQ_MASK);
-    } else {
-        irq = irqInvalid;
-    }
-
-    return irq;
+    uint32_t val = 0;
+    SYSTEM_READ_WORD(ICC_IAR1_EL1, val);
+    return (irq_t)val;
 }
 
 /*
@@ -307,15 +295,10 @@ static inline void maskInterrupt(bool_t disable, irq_t irq)
     }
 }
 
-static inline void ackInterrupt(irq_t irq)
+static inline void gic_ack_interrupt(irq_t irq)
 {
-    assert(IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])
-           && (active_irq[CURRENT_CPU_INDEX()] & IRQ_MASK) == IRQT_TO_IRQ(irq));
-
     /* Set End of Interrupt for active IRQ: ICC_EOIR1_EL1 */
-    SYSTEM_WRITE_WORD(ICC_EOIR1_EL1, active_irq[CURRENT_CPU_INDEX()]);
-    active_irq[CURRENT_CPU_INDEX()] = IRQ_NONE;
-
+    SYSTEM_WRITE_WORD(ICC_EOIR1_EL1, hw_irq);
 }
 
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
diff --git a/include/kernel/thread.h b/include/kernel/thread.h
index a4f0a6ba6f..5043437d80 100644
--- a/include/kernel/thread.h
+++ b/include/kernel/thread.h
@@ -146,7 +146,7 @@ static inline void commitTime(void)
         NODE_STATE(ksCurSC)->scConsumed += NODE_STATE(ksConsumed);
     }
 
-    NODE_STATE(ksConsumed) = 0llu;
+    NODE_STATE(ksConsumed) = 0;
 }
 
 static inline bool_t PURE isSchedulable(const tcb_t *thread)
diff --git a/include/model/statedata.h b/include/model/statedata.h
index 18e3379b4f..9e355e6d8e 100644
--- a/include/model/statedata.h
+++ b/include/model/statedata.h
@@ -114,10 +114,18 @@ extern word_t ksDomainTime;
 #endif
 extern word_t tlbLockCount VISIBLE;
 
-extern char ksIdleThreadTCB[CONFIG_MAX_NUM_NODES][BIT(seL4_TCBBits)];
-
+/* For the idle thread, we follow the kernel's memory allocation pattern used
+ * for all other thread. Every TCB exists in a memory block of the size
+ * BIT(seL4_TCBBits), which has additional management data before the actual
+ * tcb_t data. Every SC exists in a memory block of the size
+ * BIT(seL4_MinSchedContextBits), but there is no additional data besides
+ * sched_context_t in there.
+ */
+typedef char mem_block_tcb_t[BIT(seL4_TCBBits)];
+extern mem_block_tcb_t ksIdleThreadTCB[CONFIG_MAX_NUM_NODES];
 #ifdef CONFIG_KERNEL_MCS
-extern char ksIdleThreadSC[CONFIG_MAX_NUM_NODES][BIT(seL4_MinSchedContextBits)];
+typedef char mem_block_sc_t[BIT(seL4_MinSchedContextBits)];
+extern mem_block_sc_t ksIdleThreadSC[CONFIG_MAX_NUM_NODES];
 #endif
 
 #ifdef CONFIG_KERNEL_LOG_BUFFER
diff --git a/include/object/structures.h b/include/object/structures.h
index 6ca259bca8..1115670efc 100644
--- a/include/object/structures.h
+++ b/include/object/structures.h
@@ -411,6 +411,7 @@ compile_assert(notification_size_sane, sizeof(notification_t) == BIT(seL4_Notifi
 /* Check the IPC buffer is the right size */
 compile_assert(ipc_buf_size_sane, sizeof(seL4_IPCBuffer) == BIT(seL4_IPCBufferSizeBits))
 #ifdef CONFIG_KERNEL_MCS
+compile_assert(sc_size_sane, sizeof(sched_context_t) <= BIT(seL4_MinSchedContextBits))
 compile_assert(sc_core_size_sane, (sizeof(sched_context_t) + MIN_REFILLS *sizeof(refill_t) ==
                                    seL4_CoreSchedContextBytes))
 compile_assert(reply_size_sane, sizeof(reply_t) == BIT(seL4_ReplyBits))
diff --git a/src/kernel/boot.c b/src/kernel/boot.c
index 90efe980e0..0eaa288aab 100644
--- a/src/kernel/boot.c
+++ b/src/kernel/boot.c
@@ -467,23 +467,24 @@ BOOT_CODE bool_t init_sched_control(cap_t root_cnode_cap, word_t num_nodes)
 
 BOOT_CODE void create_idle_thread(void)
 {
-    pptr_t pptr;
-
 #ifdef ENABLE_SMP_SUPPORT
-    for (unsigned int i = 0; i < CONFIG_MAX_NUM_NODES; i++) {
-#endif /* ENABLE_SMP_SUPPORT */
-        pptr = (pptr_t) &ksIdleThreadTCB[SMP_TERNARY(i, 0)];
-        NODE_STATE_ON_CORE(ksIdleThread, i) = TCB_PTR(pptr + TCB_OFFSET);
-        configureIdleThread(NODE_STATE_ON_CORE(ksIdleThread, i));
+    for (unsigned int core = 0; core < CONFIG_MAX_NUM_NODES; core++) {
+#else
+    const unsigned int core = 0;
+#endif
+        tcb_t *tcb = TCB_PTR((pptr_t)&ksIdleThreadTCB[core] + TCB_OFFSET);
 #ifdef CONFIG_DEBUG_BUILD
-        setThreadName(NODE_STATE_ON_CORE(ksIdleThread, i), "idle_thread");
+        setThreadName(tcb, "idle_thread");
 #endif
-        SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbAffinity = i);
+        configureIdleThread(tcb);
+        SMP_COND_STATEMENT(tcb->tcbAffinity = core;)
+        NODE_STATE_ON_CORE(ksIdleThread, core) = tcb;
+
 #ifdef CONFIG_KERNEL_MCS
-        configure_sched_context(NODE_STATE_ON_CORE(ksIdleThread, i), SC_PTR(&ksIdleThreadSC[SMP_TERNARY(i, 0)]),
-                                usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS));
-        SMP_COND_STATEMENT(NODE_STATE_ON_CORE(ksIdleThread, i)->tcbSchedContext->scCore = i;)
-        NODE_STATE_ON_CORE(ksIdleSC, i) = SC_PTR(&ksIdleThreadSC[SMP_TERNARY(i, 0)]);
+        sched_context_t *sc = SC_PTR(&ksIdleThreadSC[core]);
+        configure_sched_context(tcb, sc, usToTicks(CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_MS));
+        SMP_COND_STATEMENT(tcb->tcbSchedContext->scCore = core;)
+        NODE_STATE_ON_CORE(ksIdleSC, core) = sc;
 #endif
 #ifdef ENABLE_SMP_SUPPORT
     }
diff --git a/src/machine/capdl.c b/src/machine/capdl.c
index e09191f123..b7b940d203 100644
--- a/src/machine/capdl.c
+++ b/src/machine/capdl.c
@@ -135,10 +135,10 @@ void obj_sc_print_attrs(cap_t sc_cap)
 void obj_ut_print_attrs(cte_t *slot, tcb_t *tcb)
 {
     /* might have two untypeds with the same address but different size */
-    printf("%p_%lu_untyped = ut (%lu bits, paddr: %p) {",
+    printf("%p_%"SEL4_PRIu_word"_untyped = ut (%"SEL4_PRIu_word" bits, paddr: %p) {",
            (void *)cap_untyped_cap_get_capPtr(slot->cap),
-           (long unsigned int)cap_untyped_cap_get_capBlockSize(slot->cap),
-           (long unsigned int)cap_untyped_cap_get_capBlockSize(slot->cap),
+           (word_t)cap_untyped_cap_get_capBlockSize(slot->cap),
+           (word_t)cap_untyped_cap_get_capBlockSize(slot->cap),
            WORD_PTR(cap_untyped_cap_get_capPtr(slot->cap)));
 
     /* there is no need to check for a NullCap as NullCaps are
@@ -162,7 +162,7 @@ void obj_ut_print_attrs(cte_t *slot, tcb_t *tcb)
 
 void obj_cnode_print_attrs(cap_t cnode)
 {
-    printf("(%lu bits)\n", (long unsigned int)cap_cnode_cap_get_capCNodeRadix(cnode));
+    printf("(%"SEL4_PRIu_word" bits)\n", (word_t)cap_cnode_cap_get_capCNodeRadix(cnode));
 }
 
 void obj_tcb_print_cnodes(cap_t cnode, tcb_t *tcb)
@@ -196,29 +196,63 @@ void obj_tcb_print_cnodes(cap_t cnode, tcb_t *tcb)
 
 void cap_cnode_print_attrs(cap_t cnode)
 {
-    printf("(guard: %lu, guard_size: %lu)\n",
-           (long unsigned int)cap_cnode_cap_get_capCNodeGuard(cnode),
-           (long unsigned int)cap_cnode_cap_get_capCNodeGuardSize(cnode));
+    printf("(guard: %"SEL4_PRIu_word", guard_size: %"SEL4_PRIu_word")\n",
+           (word_t)cap_cnode_cap_get_capCNodeGuard(cnode),
+           (word_t)cap_cnode_cap_get_capCNodeGuardSize(cnode));
 }
 
 void cap_ep_print_attrs(cap_t ep)
 {
+    unsigned int cnt_attr = 0;
+
     printf("(");
-    cap_endpoint_cap_get_capCanReceive(ep) ? putchar('R') : 0;
-    cap_endpoint_cap_get_capCanSend(ep) ? putchar('W') : 0;
-    cap_endpoint_cap_get_capCanGrant(ep) ? putchar('G') : 0;
-    cap_endpoint_cap_get_capCanGrantReply(ep) ? putchar('P') : 0;
-    long unsigned int badge = cap_endpoint_cap_get_capEPBadge(ep);
-    badge ? printf(", badge: %lu)\n", badge) : printf(")\n");
+    if (cap_endpoint_cap_get_capCanReceive(ep)) {
+        cnt_attr++;
+        putchar('R');
+    }
+    if (cap_endpoint_cap_get_capCanSend(ep)) {
+        cnt_attr++;
+        putchar('W');
+    }
+    if (cap_endpoint_cap_get_capCanGrant(ep)) {
+        cnt_attr++;
+        putchar('G');
+    }
+    if (cap_endpoint_cap_get_capCanGrantReply(ep)) {
+        cnt_attr++;
+        putchar('P');
+    }
+    word_t badge = (word_t)cap_endpoint_cap_get_capEPBadge(ep);
+    if (0 != badge) {
+        if (cnt_attr > 0) {
+            printf(", ");
+        }
+        printf("badge: %"SEL4_PRIu_word, badge);
+    }
+    printf(")\n");
 }
 
 void cap_ntfn_print_attrs(cap_t ntfn)
 {
+    unsigned int cnt_attr = 0;
+
     printf("(");
-    cap_notification_cap_get_capNtfnCanReceive(ntfn) ? putchar('R') : 0;
-    cap_notification_cap_get_capNtfnCanSend(ntfn) ? putchar('W') : 0;
-    long unsigned int badge = cap_notification_cap_get_capNtfnBadge(ntfn);
-    badge ? printf(", badge: %lu)\n", badge) : printf(")\n");
+    if (cap_notification_cap_get_capNtfnCanReceive(ntfn)) {
+        cnt_attr++;
+        putchar('R');
+    }
+    if (cap_notification_cap_get_capNtfnCanSend(ntfn)) {
+        cnt_attr++;
+        putchar('W');
+    }
+    word_t badge = (word_t)cap_notification_cap_get_capNtfnBadge(ntfn);
+    if (badge) {
+        if (cnt_attr > 0) {
+            printf(", ");
+        }
+        printf("badge: %"SEL4_PRIu_word, badge);
+    }
+    printf(")\n");
 }
 
 /*
diff --git a/src/model/statedata.c b/src/model/statedata.c
index f3bf19bf4e..8f4e13e535 100644
--- a/src/model/statedata.c
+++ b/src/model/statedata.c
@@ -97,12 +97,12 @@ word_t ksDomScheduleIdx;
 /* Only used by lockTLBEntry */
 word_t tlbLockCount = 0;
 
-/* Idle thread. */
-SECTION("._idle_thread") char ksIdleThreadTCB[CONFIG_MAX_NUM_NODES][BIT(seL4_TCBBits)] ALIGN(BIT(TCB_SIZE_BITS));
+/* memory for Idle thread TCB. */
+SECTION("._idle_thread") mem_block_tcb_t ksIdleThreadTCB[CONFIG_MAX_NUM_NODES] ALIGN(BIT(TCB_SIZE_BITS));
 
 #ifdef CONFIG_KERNEL_MCS
 /* Idle thread Schedcontexts */
-char ksIdleThreadSC[CONFIG_MAX_NUM_NODES][BIT(seL4_MinSchedContextBits)] ALIGN(BIT(seL4_MinSchedContextBits));
+mem_block_sc_t ksIdleThreadSC[CONFIG_MAX_NUM_NODES] ALIGN(BIT(seL4_MinSchedContextBits));
 #endif
 
 #if (defined CONFIG_DEBUG_BUILD || defined CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES)
diff --git a/tools/hardware.yml b/tools/hardware.yml
index cf55f22f9a..d84a560dea 100644
--- a/tools/hardware.yml
+++ b/tools/hardware.yml
@@ -177,6 +177,15 @@ devices:
       - index: 0
         kernel: WDT1_PPTR
         user: true
+  # i.MX6 UART
+  - compatible:
+      - fsl,imx6q-uart
+    regions:
+      - index: 0
+        kernel: UART_PPTR
+        macro: CONFIG_PRINTING
+        user: true
+        kernel_size: 0x10000
   # various serial consoles (`grep <compatible> serial/*`)
   - compatible:
       - amlogic,meson-gx-uart