diff --git a/include/arch/x86/arch/model/statedata.h b/include/arch/x86/arch/model/statedata.h
index 5f6bf872a4637aa0204e1af4c0f13ae101de3880..6651f4f37401067e2b8b301c6c9051cd2ebfa377 100644
--- a/include/arch/x86/arch/model/statedata.h
+++ b/include/arch/x86/arch/model/statedata.h
@@ -17,9 +17,8 @@
 #include <object/structures.h>
 #include <arch/types.h>
 #include <plat/machine/devices.h>
-
+#include <plat/machine.h>
 #include <arch/object/iospace.h>
-#include <plat/machine/hardware.h>
 
 #include <mode/model/statedata.h>
 
diff --git a/include/arch/x86/arch/object/iospace.h b/include/arch/x86/arch/object/iospace.h
index e4cf83442503edd1a580246467ee0fe34f759cda..396b1247e4591b1b8f391076e7c4a2f5fafe6f01 100644
--- a/include/arch/x86/arch/object/iospace.h
+++ b/include/arch/x86/arch/object/iospace.h
@@ -14,6 +14,7 @@
 #include <types.h>
 #include <api/failures.h>
 #include <object/structures.h>
+#include <plat/machine/hardware_gen.h>
 
 static inline int vtd_get_root_index(dev_id_t dev)
 {
diff --git a/include/machine.h b/include/machine.h
index 16a63027930f787685c301fd25ee97c641f2a09d..a4b57ca10fa8c38dcb795f29ebd6d317e7da12d0 100644
--- a/include/machine.h
+++ b/include/machine.h
@@ -15,6 +15,7 @@
 #include <machine/registerset.h>
 
 #include <mode/machine.h>
+#include <plat/machine/hardware.h>
 
 static inline void* CONST
 ptrFromPAddr(paddr_t paddr)
diff --git a/include/machine/hardware.h b/include/machine/hardware.h
deleted file mode 100644
index 17b3937b67b618e9f34aa4aad6ecbaec16646e36..0000000000000000000000000000000000000000
--- a/include/machine/hardware.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
- *
- * @TAG(GD_GPL)
- */
-
-#ifndef __MACHINE_HARDWARE_H
-#define __MACHINE_HARDWARE_H
-
-#include <types.h>
-#include <arch/machine/hardware.h>
-#include <plat/machine/hardware.h>
-#include <plat/machine.h>
-
-void handleReservedIRQ(irq_t irq);
-void handleSpuriousIRQ(void);
-
-/** MODIFIES: [*] */
-void ackInterrupt(irq_t irq);
-
-/** MODIFIES: [*] */
-irq_t getActiveIRQ(void);
-
-/** MODIFIES: [*] */
-bool_t isIRQPending(void);
-
-/** MODIFIES: [*] */
-void maskInterrupt(bool_t disable, irq_t irq);
-
-#endif
diff --git a/include/plat/allwinnerA20/plat/machine/hardware.h b/include/plat/allwinnerA20/plat/machine/hardware.h
index dffae91ce2974b41cc3419cf2837c7f1f471c42a..ee41676d382d21148b2645774038a423de736598 100755
--- a/include/plat/allwinnerA20/plat/machine/hardware.h
+++ b/include/plat/allwinnerA20/plat/machine/hardware.h
@@ -58,4 +58,11 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { SPI1_PADDR                    , SPI1_PADDR                        + ( 2 << PAGE_BITS) },
 
 };
+
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+}
+
 #endif
diff --git a/include/plat/am335x/plat/machine/hardware.h b/include/plat/am335x/plat/machine/hardware.h
index 93faac360d8b2117a20026ac2b462bacc3f7bc46..67c25bea1cd1451e02ce9b881525ac35aaa42068 100644
--- a/include/plat/am335x/plat/machine/hardware.h
+++ b/include/plat/am335x/plat/machine/hardware.h
@@ -14,6 +14,7 @@
 #include <basic_types.h>
 #include <arch/linker.h>
 #include <plat/machine/devices.h>
+#include <plat/machine/interrupt.h>
 
 #define physBase          0x80000000
 #define kernelBase        0xf0000000
diff --git a/include/plat/am335x/plat/machine/interrupt.h b/include/plat/am335x/plat/machine/interrupt.h
new file mode 100644
index 0000000000000000000000000000000000000000..f8e6584aa99a48e3d4402c095b2513f52b490355
--- /dev/null
+++ b/include/plat/am335x/plat/machine/interrupt.h
@@ -0,0 +1,135 @@
+/*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ */
+
+#include <config.h>
+#include <types.h>
+#include <armv/machine.h>
+
+#include <machine/io.h>
+#include <kernel/vspace.h>
+#include <arch/machine.h>
+#include <arch/kernel/vspace.h>
+#include <plat/machine.h>
+#include <arch/linker.h>
+
+#define CMPER_REG(base, off) ((volatile uint32_t *)((base) + (off)))
+#define CMPER_TIMER3_CLKCTRL    0x84
+#define CMPER_CLKCTRL_DISABLE   0
+#define CMPER_CLKCTRL_ENABLE    2
+#define CMPER_CLKSEL_TIMER3     0x50c
+#define CMPER_CKLSEL_MOSC       1
+
+
+#define INTCPS_SYSCONFIG_SOFTRESET BIT(1)
+#define INTCPS_SYSSTATUS_RESETDONE BIT(0)
+#define INTCPS_CONTROL_NEWIRQAGR BIT(0)
+#define INTCPS_SIR_IRQ_SPURIOUSIRQFLAG 0xffffff80
+
+/*
+ * The struct below is used to discourage the compiler from generating literals
+ * for every single address we might access.
+ */
+volatile struct INTC_map {
+    uint32_t padding[4];
+    uint32_t intcps_sysconfig;
+    uint32_t intcps_sysstatus;
+    uint32_t padding2[10];
+    uint32_t intcps_sir_irq;
+    uint32_t intcps_sir_fiq;
+    uint32_t intcps_control;
+    uint32_t intcps_protection;
+    uint32_t intcps_idle;
+    uint32_t padding3[3];
+    uint32_t intcps_irq_priority;
+    uint32_t intcps_fiq_priority;
+    uint32_t intcps_threshold;
+    uint32_t padding4[5];
+    struct {
+        uint32_t intcps_itr;
+        uint32_t intcps_mir;
+        uint32_t intcps_mir_clear;
+        uint32_t intcps_mir_set;
+        uint32_t intcps_isr_set;
+        uint32_t intcps_isr_clear;
+        uint32_t intcps_pending_irq;
+        uint32_t intcps_pending_fiq;
+    } intcps_n[4];
+    uint32_t intcps_ilr[128];
+} *intc = (volatile void*)INTC_PPTR;
+
+
+/**
+   DONT_TRANSLATE
+ */
+static inline interrupt_t
+getActiveIRQ(void)
+{
+    uint32_t intcps_sir_irq = intc->intcps_sir_irq;
+    interrupt_t irq = (interrupt_t)(intcps_sir_irq & 0x7f);
+
+    if ((intcps_sir_irq & INTCPS_SIR_IRQ_SPURIOUSIRQFLAG) == 0) {
+        assert((irq / 32) < (sizeof intc->intcps_n / sizeof intc->intcps_n[0]));
+        if (intc->intcps_n[irq / 32].intcps_pending_irq & (1 << (irq & 31))) {
+            return irq;
+        }
+    }
+    return irqInvalid;
+}
+
+/* Check for pending IRQ */
+static inline bool_t
+isIRQPending(void)
+{
+    return getActiveIRQ() != irqInvalid;
+}
+
+/* Enable or disable irq according to the 'disable' flag. */
+/**
+   DONT_TRANSLATE
+*/
+static inline void
+maskInterrupt(bool_t disable, interrupt_t irq)
+{
+    assert(irq <= maxIRQ);
+    if (disable) {
+        intc->intcps_n[irq / 32].intcps_mir_set = 1 << (irq & 31);
+    } else {
+        intc->intcps_n[irq / 32].intcps_mir_clear = 1 << (irq & 31);
+    }
+}
+
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+}
+
+static inline void
+ackInterrupt(irq_t irq)
+{
+    /*
+     * am335x ref man, sec 6.2.2 only requires a DSB after NEWIRQAGR.
+     * I found that without dsb() or more code before, I get interrupts
+     * without the associated pending bit being set. Perhaps this
+     * indicates a missing barrier in code elsewhere? -TimN
+     */
+    dsb();
+    intc->intcps_control = INTCPS_CONTROL_NEWIRQAGR;
+    dsb();
+}
+
+static inline void
+handleSpuriousIRQ(void)
+{
+    /* Reset and re-enable IRQs. */
+    intc->intcps_control = INTCPS_CONTROL_NEWIRQAGR;
+    dsb();
+}
+
diff --git a/include/plat/apq8064/plat/machine/hardware.h b/include/plat/apq8064/plat/machine/hardware.h
index 69dd8682e673cbdf0be868cce4bd32cd483c3e53..4c73403c0c916639635d675b22c9075639b29ced 100644
--- a/include/plat/apq8064/plat/machine/hardware.h
+++ b/include/plat/apq8064/plat/machine/hardware.h
@@ -297,4 +297,10 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { /* .start */ SATA_PADDR                , /* .end */ SATA_PADDR                + (1 << PAGE_BITS) }
 };
 
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+}
+
 #endif /* !__PLAT_MACHINE_HARDWARE_H */
diff --git a/include/plat/exynos4/plat/machine/hardware.h b/include/plat/exynos4/plat/machine/hardware.h
index 58baeaeddb31d6b32e7adb6fa6169af4cab716f7..f7f7850ed67354768eeaf87eea3ac284e8bc6f88 100644
--- a/include/plat/exynos4/plat/machine/hardware.h
+++ b/include/plat/exynos4/plat/machine/hardware.h
@@ -218,4 +218,10 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { /* .start */ MODEMIF_PADDR          , /* .end */ MODEMIF_PADDR           + (1 << PAGE_BITS) },
 };
 
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+}
+
 #endif /* !__PLAT_MACHINE_HARDWARE_H */
diff --git a/include/plat/exynos5/plat/machine/hardware.h b/include/plat/exynos5/plat/machine/hardware.h
index deaaf4f07e1d8c063281a989decd6cb9c4e1df1f..d9776dd4b197b63f15cc09ffbae80598dd83bab6 100644
--- a/include/plat/exynos5/plat/machine/hardware.h
+++ b/include/plat/exynos5/plat/machine/hardware.h
@@ -11,8 +11,10 @@
 #ifndef __PLAT_MACHINE_HARDWARE_H
 #define __PLAT_MACHINE_HARDWARE_H
 
+#include <config.h>
 #include <basic_types.h>
 #include <arch/linker.h>
+#include <arch/object/vcpu.h>
 #include <plat/machine/devices.h>
 
 #define physBase          0x60000000
@@ -288,4 +290,15 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { /* .start */ AES1_SFR_PADDR        , /* .end */ AES1_SFR_PADDR         + (1 << PAGE_BITS) },
 };
 
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+    if ((config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) &&
+            (irq == INTERRUPT_VGIC_MAINTENANCE)) {
+        VGICMaintenance();
+        return;
+    }
+}
+
 #endif /* !__PLAT_MACHINE_HARDWARE_H */
diff --git a/include/plat/hikey/plat/machine/hardware.h b/include/plat/hikey/plat/machine/hardware.h
index 90e3a3168302bd33e58befe848d7eab359b4951d..3a6a4cf937b29340aec76ee141259b986ebb0e35 100755
--- a/include/plat/hikey/plat/machine/hardware.h
+++ b/include/plat/hikey/plat/machine/hardware.h
@@ -57,4 +57,10 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { /* .start = */ DMTIMER0_PADDR, /* .end = */ DMTIMER0_PADDR + (1 << PAGE_BITS) },
 };
 
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+}
+
 #endif
diff --git a/include/plat/imx31/plat/machine/hardware.h b/include/plat/imx31/plat/machine/hardware.h
index 04acf7481b9c1446fffc2f02c6365ead4736bf57..b0087ca5b15ee6a8c1d9c950899dc0d280376522 100644
--- a/include/plat/imx31/plat/machine/hardware.h
+++ b/include/plat/imx31/plat/machine/hardware.h
@@ -14,6 +14,8 @@
 #include <basic_types.h>
 #include <arch/linker.h>
 #include <plat/machine/devices.h>
+#include <plat/machine/interrupt.h>
+
 #define physBase          0x80000000
 #define kernelBase        0xf0000000
 
diff --git a/include/plat/imx31/plat/machine/interrupt.h b/include/plat/imx31/plat/machine/interrupt.h
new file mode 100644
index 0000000000000000000000000000000000000000..0f09514bf5173bf0fbd4a54a7e892230308b9a8b
--- /dev/null
+++ b/include/plat/imx31/plat/machine/interrupt.h
@@ -0,0 +1,98 @@
+/*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ */
+
+#ifndef __PLAT_MACHINE_INTERRUPT_H
+#define __PLAT_MACHINE_INTERRUPT_H
+
+#include <config.h>
+#include <basic_types.h>
+#include <arch/benchmark_overflowHandler.h>
+#include <plat/machine.h>
+
+/* Memory map for AVIC (Advanced Vectored Interrupt Controller). */
+volatile struct avic_map {
+    uint32_t intctl;
+    uint32_t nimask;
+    uint32_t intennum;
+    uint32_t intdisnum;
+    uint32_t intenableh;
+    uint32_t intenablel;
+    uint32_t inttypeh;
+    uint32_t inttypel;
+    uint32_t nipriority[8];
+    uint32_t nivecsr;
+    uint32_t fivecsr;
+    uint32_t intsrch;
+    uint32_t intsrcl;
+    uint32_t intfrch;
+    uint32_t intfrcl;
+    uint32_t nipndh;
+    uint32_t nipndl;
+    uint32_t fipndh;
+    uint32_t fipndl;
+    uint32_t vector[64];
+} *avic = (volatile void *)AVIC_PPTR;
+
+/* Get the active IRQ number from the AVIC.  Returns 0xff if
+ * there isn't one. Note this is also known as irqInvalid */
+/**
+   DONT_TRANSLATE
+ */
+static inline interrupt_t
+getActiveIRQ(void)
+{
+    return (avic->nivecsr >> 16) & 0xff;
+}
+
+/* Check for pending IRQ */
+static inline bool_t
+isIRQPending(void)
+{
+    return getActiveIRQ() != irqInvalid;
+}
+
+/* Enable or disable irq according to the 'disable' flag. */
+/**
+   DONT_TRANSLATE
+*/
+static inline void
+maskInterrupt(bool_t disable, interrupt_t irq)
+{
+    if (disable) {
+        avic->intdisnum = irq;
+    } else {
+        avic->intennum = irq;
+    }
+}
+
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
+    if (irq == KERNEL_PMU_IRQ) {
+        handleOverflowIRQ();
+    }
+#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
+}
+
+static inline void
+ackInterrupt(irq_t irq)
+{
+    /* empty on this platform */
+}
+
+static inline void
+handleSpuriousIRQ(void)
+{
+    /* do nothing */
+}
+
+#endif
diff --git a/include/plat/imx6/plat/machine/hardware.h b/include/plat/imx6/plat/machine/hardware.h
index c3fd3d9234d06bd265c4ce5912096d368c945586..f5f0959b2873c4763f72640bb3f2442359e40dfa 100644
--- a/include/plat/imx6/plat/machine/hardware.h
+++ b/include/plat/imx6/plat/machine/hardware.h
@@ -11,9 +11,11 @@
 #ifndef __PLAT_MACHINE_HARDWARE_H
 #define __PLAT_MACHINE_HARDWARE_H
 
+#include <config.h>
 #include <basic_types.h>
 #include <arch/linker.h>
 #include <plat/machine/devices.h>
+#include <arch/benchmark_overflowHandler.h>
 
 #define physBase          0x10000000
 #define kernelBase        0xe0000000
@@ -197,4 +199,14 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
 //  { /* .start = */ BOOT_ROM_PADDR         , /* .end = */ BOOT_ROM_PADDR          + ( 24 << 12)}
 };
 
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
+    if (irq == KERNEL_PMU_IRQ) {
+        handleOverflowIRQ();
+    }
+#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
+}
+
 #endif /* !__PLAT_MACHINE_HARDWARE_H */
diff --git a/include/plat/imx7/plat/machine/hardware.h b/include/plat/imx7/plat/machine/hardware.h
index 86ab62bec5199ee01f7c955e68bbcb05ec5b41cc..1cc04afe6402918f3bd8aa84d519c9a406fa1c0d 100644
--- a/include/plat/imx7/plat/machine/hardware.h
+++ b/include/plat/imx7/plat/machine/hardware.h
@@ -108,4 +108,10 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { FEC1_PADDR,               FEC1_PADDR              +   0x10000 },
 };
 
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+}
+
 #endif /* !__PLAT_MACHINE_HARDWARE_H */
diff --git a/include/plat/omap3/plat/machine/hardware.h b/include/plat/omap3/plat/machine/hardware.h
index 71f2c1dc9f377277c7fbe13eed2847a199967230..4bc8d16ca66582854f1ca7eb91b9b6c02435c4d3 100644
--- a/include/plat/omap3/plat/machine/hardware.h
+++ b/include/plat/omap3/plat/machine/hardware.h
@@ -13,7 +13,9 @@
 
 #include <basic_types.h>
 #include <arch/linker.h>
+#include <armv/machine.h>
 #include <plat/machine/devices.h>
+#include <plat/machine/interrupt.h>
 
 #define physBase          0x80000000
 #define kernelBase        0xf0000000
diff --git a/include/plat/omap3/plat/machine/interrupt.h b/include/plat/omap3/plat/machine/interrupt.h
new file mode 100644
index 0000000000000000000000000000000000000000..734a26e4954d885045d31d0ebd9f8bcf76025a90
--- /dev/null
+++ b/include/plat/omap3/plat/machine/interrupt.h
@@ -0,0 +1,128 @@
+/*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ */
+#ifndef __PLAT_MACHINE_INTERRUPT_H
+#define __PLAT_MACHINE_INTERRUPT_H
+
+#include <config.h>
+#include <types.h>
+#include <machine/io.h>
+#include <kernel/vspace.h>
+#include <arch/machine.h>
+#include <arch/kernel/vspace.h>
+#include <plat/machine.h>
+#include <arch/linker.h>
+#include <plat/machine/devices.h>
+#include <plat/machine/hardware.h>
+
+#define INTCPS_SIR_IRQ_SPURIOUSIRQFLAG 0xFF0000
+
+/*
+ * The struct below is used to discourage the compiler from generating literals
+ * for every single address we might access.
+ */
+volatile struct INTC_map {
+    uint32_t padding[4];
+    uint32_t intcps_sysconfig;
+    uint32_t intcps_sysstatus;
+    uint32_t padding2[10];
+    uint32_t intcps_sir_irq;
+    uint32_t intcps_sir_fiq;
+    uint32_t intcps_control;
+    uint32_t intcps_protection;
+    uint32_t intcps_idle;
+    uint32_t padding3[3];
+    uint32_t intcps_irq_priority;
+    uint32_t intcps_fiq_priority;
+    uint32_t intcps_threshold;
+    uint32_t padding4[5];
+    struct {
+        uint32_t intcps_itr;
+        uint32_t intcps_mir;
+        uint32_t intcps_mir_clear;
+        uint32_t intcps_mir_set;
+        uint32_t intcps_isr_set;
+        uint32_t intcps_isr_clear;
+        uint32_t intcps_pending_irq;
+        uint32_t intcps_pending_fiq;
+    } intcps_n[3];
+    uint32_t padding5[8];
+    uint32_t intcps_ilr[96];
+} *intc = (volatile void*)INTC_PPTR;
+
+/**
+   DONT_TRANSLATE
+ */
+static inline interrupt_t
+getActiveIRQ(void)
+{
+    uint32_t intcps_sir_irq = intc->intcps_sir_irq;
+    interrupt_t irq = (interrupt_t)(intcps_sir_irq & 0x7f);
+
+    /* Ignore spurious interrupts. */
+    if ((intcps_sir_irq & INTCPS_SIR_IRQ_SPURIOUSIRQFLAG) == 0) {
+        assert(irq <= maxIRQ);
+        if (intc->intcps_n[irq / 32].intcps_pending_irq & (1 << (irq & 31))) {
+            return irq;
+        }
+    }
+
+    /* No interrupt. */
+    return irqInvalid;
+}
+
+/* Check for pending IRQ */
+static inline bool_t
+isIRQPending(void)
+{
+    return getActiveIRQ() != irqInvalid;
+}
+
+/* Enable or disable irq according to the 'disable' flag. */
+/**
+   DONT_TRANSLATE
+*/
+static inline void
+maskInterrupt(bool_t disable, interrupt_t irq)
+{
+    if (disable) {
+        intc->intcps_n[irq / 32].intcps_mir_set = 1 << (irq & 31);
+    } else {
+        intc->intcps_n[irq / 32].intcps_mir_clear = 1 << (irq & 31);
+    }
+}
+
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+    /* We shouldn't be receiving any reserved IRQs anyway. */
+    maskInterrupt(true, irq);
+
+    return;
+}
+
+static inline void
+ackInterrupt(irq_t irq)
+{
+    intc->intcps_control = 1;
+    /* Ensure the ack has hit the interrupt controller before potentially
+     * re-enabling interrupts. */
+    dsb();
+}
+
+static inline void
+handleSpuriousIRQ(void)
+{
+    /* Reset and re-enable IRQs. */
+    intc->intcps_control = 1;
+    dsb();
+}
+
+#endif
diff --git a/include/plat/pc99/plat/machine/devices.h b/include/plat/pc99/plat/machine/devices.h
index c7016524d76e20e07bb1f6389c20258dd23c14ff..5e0d2c392754a0d8670e93a416da440d769846d3 100644
--- a/include/plat/pc99/plat/machine/devices.h
+++ b/include/plat/pc99/plat/machine/devices.h
@@ -12,7 +12,6 @@
 #define __PLAT_MACHINE_DEVICES_H
 
 #include <config.h>
-#include <plat/machine/hardware.h>
 
 #define PPTR_APIC PPTR_KDEV
 
diff --git a/include/plat/pc99/plat/machine/hardware.h b/include/plat/pc99/plat/machine/hardware.h
index bda9e8f69693af955289b39a2adb40acea1995fe..d8af7cb07a7585d549abbfba911e14986d25f867 100644
--- a/include/plat/pc99/plat/machine/hardware.h
+++ b/include/plat/pc99/plat/machine/hardware.h
@@ -11,13 +11,9 @@
 #ifndef __PLAT_MACHINE_HARDWARE_H
 #define __PLAT_MACHINE_HARDWARE_H
 
-#include <config.h>
-#include <types.h>
-#include <machine/timer.h>
-#include <machine/hardware.h>
+#include <plat/machine/interrupt.h>
 #include <plat/machine.h>
 #include <plat/machine/hardware_gen.h>
-
 #include <plat_mode/machine/hardware.h>
 
 void platAddDevices(void);
diff --git a/include/plat/pc99/plat/machine/interrupt.h b/include/plat/pc99/plat/machine/interrupt.h
new file mode 100644
index 0000000000000000000000000000000000000000..b789cd207950e6f8ec8228c909ca0e34e74a1e6d
--- /dev/null
+++ b/include/plat/pc99/plat/machine/interrupt.h
@@ -0,0 +1,120 @@
+/*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ */
+
+#ifndef __PLAT_MACHINE_INTERRUPT_H
+#define __PLAT_MACHINE_INTERRUPT_H
+
+#include <config.h>
+#include <types.h>
+#include <util.h>
+
+#include <arch/object/structures.h>
+#include <arch/model/statedata.h>
+#include <arch/kernel/apic.h>
+#include <plat/machine/acpi.h>
+#include <plat/machine/ioapic.h>
+#include <plat/machine/pic.h>
+#include <plat/machine/intel-vtd.h>
+
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+    if (config_set(CONFIG_IOMMU) && irq == irq_iommu) {
+        vtd_handle_fault();
+        return;
+    }
+}
+
+/* Get the IRQ number currently working on. */
+static inline irq_t
+getActiveIRQ(void)
+{
+    if (x86KScurInterrupt == int_invalid) {
+        return irqInvalid;
+    }
+    return x86KScurInterrupt - IRQ_INT_OFFSET;
+}
+
+/* Checks for pending IRQ */
+static inline bool_t
+isIRQPending(void)
+{
+    if (apic_is_interrupt_pending()) {
+        return true;
+    }
+
+    if (config_set(CONFIG_IRQ_PIC) && pic_is_irq_pending()) {
+        return true;
+    }
+
+    return false;
+}
+
+static inline void
+ackInterrupt(irq_t irq)
+{
+    if (config_set(CONFIG_IRQ_PIC) && irq <= irq_isa_max) {
+        pic_ack_active_irq();
+    } else {
+        apic_ack_active_interrupt();
+    }
+}
+
+static inline void
+handleSpuriousIRQ(void)
+{
+    /* do nothing */
+}
+
+static void inline
+updateIRQState(word_t irq, x86_irq_state_t state)
+{
+    assert(irq >= 0 && irq <= maxIRQ);
+    x86KSIRQState[irq] = state;
+}
+
+static inline void
+maskInterrupt(bool_t disable, irq_t irq)
+{
+    if (irq >= irq_isa_min && irq <= irq_isa_max) {
+        if (config_set(CONFIG_IRQ_PIC)) {
+            pic_mask_irq(disable, irq);
+        } else {
+            /* We shouldn't receive interrupts on the PIC range
+             * if not using the PIC, but soldier on anyway */
+        }
+    } else if (irq >= irq_user_min && irq <= irq_user_max) {
+        x86_irq_state_t state = x86KSIRQState[irq];
+        switch (x86_irq_state_get_irqType(state)) {
+        case x86_irq_state_irq_ioapic: {
+            uint32_t ioapic = x86_irq_state_irq_ioapic_get_id(state);
+            uint32_t pin = x86_irq_state_irq_ioapic_get_pin(state);
+            ioapic_mask(disable, ioapic, pin);
+            state =  x86_irq_state_irq_ioapic_set_masked(state, disable);
+            updateIRQState(irq, state);
+        }
+        break;
+        case x86_irq_state_irq_msi:
+            /* currently MSI interrupts can not be disabled */
+            break;
+        case x86_irq_state_irq_free:
+            /* A spurious interrupt, and the resulting mask here,
+             * could be from a user ripping out a vector before
+             * the interrupt reached the kernel. Silently ignore */
+            break;
+        }
+    } else {
+        /* masking some other kind of interrupt source, this probably
+         * shouldn't happen, but soldier on */
+    }
+}
+
+#endif
diff --git a/include/plat/tk1/plat/machine/hardware.h b/include/plat/tk1/plat/machine/hardware.h
index 77d9c8588e519a5c6a57b043f1b34a637fd81228..55e9d025d9c2a51f7136005ab782b62aa8b98d81 100644
--- a/include/plat/tk1/plat/machine/hardware.h
+++ b/include/plat/tk1/plat/machine/hardware.h
@@ -11,11 +11,14 @@
 #ifndef __PLAT_MACHINE_HARDWARE_H
 #define __PLAT_MACHINE_HARDWARE_H
 
+#include <config.h>
 #include <util.h>
 #include <basic_types.h>
 #include <arch/linker.h>
+#include <arch/object/vcpu.h>
 #include <plat/machine/devices.h>
 #include <plat/machine/hardware_gen.h>
+#include <plat/machine/smmu.h>
 #include <mode/machine/hardware.h>
 #include <mode/api/constants.h>
 
@@ -142,4 +145,25 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { USB3_PADDR,           USB3_PADDR + (BIT(seL4_PageBits) * 2) },           /* 8 KB region, 6 KB            */
 };
 
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
+    if (irq == KERNEL_PMU_IRQ) {
+        handleOverflowIRQ();
+    }
+#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
+
+    if ((config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) && (irq == INTERRUPT_VGIC_MAINTENANCE)) {
+        VGICMaintenance();
+        return;
+    }
+
+    if (config_set(CONFIG_ARM_SMMU) && (irq == INTERRUPT_SMMU)) {
+        plat_smmu_handle_interrupt();
+        return;
+    }
+}
+
 #endif
diff --git a/include/plat/zynq7000/plat/machine/hardware.h b/include/plat/zynq7000/plat/machine/hardware.h
index b9b3ee1acbd0c1386d910dddce20b33e970c6497..d0b1698aca12f5450d8511d4f227ff205759610d 100644
--- a/include/plat/zynq7000/plat/machine/hardware.h
+++ b/include/plat/zynq7000/plat/machine/hardware.h
@@ -11,9 +11,11 @@
 #ifndef __PLAT_MACHINE_HARDWARE_H
 #define __PLAT_MACHINE_HARDWARE_H
 
+#include <config.h>
 #include <basic_types.h>
 #include <arch/linker.h>
 #include <plat/machine/devices.h>
+#include <arch/benchmark_overflowHandler.h>
 
 #define physBase          0x00000000
 #define kernelBase        0xe0000000
@@ -117,4 +119,15 @@ static const p_region_t BOOT_RODATA dev_p_regs[] = {
     { /* .start = */ PL_M_AXI_GP1_PADDR, /* .end = */ PL_M_AXI_GP1_PADDR             + 0x40000000U},
 };
 
+/* Handle a platform-reserved IRQ. */
+static inline void
+handleReservedIRQ(irq_t irq)
+{
+#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
+    if (irq == KERNEL_PMU_IRQ) {
+        handleOverflowIRQ();
+    }
+#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
+}
+
 #endif /* !__PLAT_MACHINE_HARDWARE_H */
diff --git a/src/api/syscall.c b/src/api/syscall.c
index f56ce0926d8099272ff62633164dd52f108dac9d..8776110f5decb248c8c73d04c2181499a868b523 100644
--- a/src/api/syscall.c
+++ b/src/api/syscall.c
@@ -21,7 +21,7 @@
 #include <kernel/thread.h>
 #include <kernel/vspace.h>
 #include <machine/io.h>
-#include <machine/hardware.h>
+#include <plat/machine/hardware.h>
 #include <object/interrupt.h>
 #include <model/statedata.h>
 #include <string.h>
diff --git a/src/arch/arm/32/machine/hardware.c b/src/arch/arm/32/machine/hardware.c
index c40379a67add1cbeb31ec7c229de56da8da0a71d..7d340368a98d008cc9fc53a4945be982ccbc4da5 100644
--- a/src/arch/arm/32/machine/hardware.c
+++ b/src/arch/arm/32/machine/hardware.c
@@ -11,6 +11,7 @@
 #include <types.h>
 #include <machine/registerset.h>
 #include <arch/machine.h>
+#include <plat/machine/hardware.h>
 
 word_t PURE
 getRestartPC(tcb_t *thread)
diff --git a/src/arch/arm/armv/armv7-a/user_access.c b/src/arch/arm/armv/armv7-a/user_access.c
index ed71ff10407e5ce1487eef0316d2325ec9adbbf2..3b3d111e862310cfcea4f4856222ddaed2c6e050 100644
--- a/src/arch/arm/armv/armv7-a/user_access.c
+++ b/src/arch/arm/armv/armv7-a/user_access.c
@@ -8,7 +8,7 @@
  * @TAG(GD_GPL)
  */
 
-#include <machine/hardware.h>
+#include <plat/machine/hardware.h>
 #include <arch/user_access.h>
 
 #define PMUSERENR_ENABLE BIT(0)
diff --git a/src/arch/x86/object/interrupt.c b/src/arch/x86/object/interrupt.c
index cd89ed8399276251db7d93405c248fa8012109b8..68257767977740a75f083f5d3b915a5ef818fbc7 100644
--- a/src/arch/x86/object/interrupt.c
+++ b/src/arch/x86/object/interrupt.c
@@ -14,6 +14,7 @@
 #include <arch/api/invocation.h>
 #include <arch/linker.h>
 #include <plat/machine/pci.h>
+#include <plat/machine/hardware.h>
 
 void
 Arch_irqStateInit(void)
@@ -52,55 +53,6 @@ Arch_checkIRQ(word_t irq)
     return EXCEPTION_SYSCALL_ERROR;
 }
 
-static void inline
-updateIRQState(word_t irq, x86_irq_state_t state)
-{
-    assert(irq >= 0 && irq <= maxIRQ);
-    x86KSIRQState[irq] = state;
-}
-
-void
-Arch_updateIRQState(word_t irq, x86_irq_state_t state)
-{
-    updateIRQState(irq, state);
-}
-
-void
-maskInterrupt(bool_t disable, irq_t irq)
-{
-    if (irq >= irq_isa_min && irq <= irq_isa_max) {
-        if (config_set(CONFIG_IRQ_PIC)) {
-            pic_mask_irq(disable, irq);
-        } else {
-            /* We shouldn't receive interrupts on the PIC range
-             * if not using the PIC, but soldier on anyway */
-        }
-    } else if (irq >= irq_user_min && irq <= irq_user_max) {
-        x86_irq_state_t state = x86KSIRQState[irq];
-        switch (x86_irq_state_get_irqType(state)) {
-        case x86_irq_state_irq_ioapic: {
-            uint32_t ioapic = x86_irq_state_irq_ioapic_get_id(state);
-            uint32_t pin = x86_irq_state_irq_ioapic_get_pin(state);
-            ioapic_mask(disable, ioapic, pin);
-            state =  x86_irq_state_irq_ioapic_set_masked(state, disable);
-            Arch_updateIRQState(irq, state);
-        }
-        break;
-        case x86_irq_state_irq_msi:
-            /* currently MSI interrupts can not be disabled */
-            break;
-        case x86_irq_state_irq_free:
-            /* A spurious interrupt, and the resulting mask here,
-             * could be from a user ripping out a vector before
-             * the interrupt reached the kernel. Silently ignore */
-            break;
-        }
-    } else {
-        /* masking some other kind of interrupt source, this probably
-         * shouldn't happen, but soldier on */
-    }
-}
-
 static exception_t
 Arch_invokeIRQControl(irq_t irq, cte_t *handlerSlot, cte_t *controlSlot, x86_irq_state_t irqState)
 {
diff --git a/src/object/interrupt.c b/src/object/interrupt.c
index d7e78c59b5a8e5395cc5f125688240e525ae4ec9..b7c3fecc92ec3dff9f1127a04022fb0c0e5f8a48 100644
--- a/src/object/interrupt.c
+++ b/src/object/interrupt.c
@@ -21,6 +21,7 @@
 #include <kernel/cspace.h>
 #include <kernel/thread.h>
 #include <model/statedata.h>
+#include <machine/timer.h>
 
 exception_t
 decodeIRQControlInvocation(word_t invLabel, word_t length,
diff --git a/src/plat/allwinnerA20/machine/hardware.c b/src/plat/allwinnerA20/machine/hardware.c
index 5d055965836990528f27a015af5f66faa77ad5de..b9d3f032c7bdc2b6b1dc2e87c6e3a5bbcfc9ed78 100755
--- a/src/plat/allwinnerA20/machine/hardware.c
+++ b/src/plat/allwinnerA20/machine/hardware.c
@@ -19,12 +19,6 @@
 #include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
 
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-}
-
 #define TIMER_INTERVAL_US  (CONFIG_TIMER_TICK_MS * 1000)
 #define TIMER_MHZ          24ULL
 #define TIMER_TICKS        (TIMER_MHZ * TIMER_INTERVAL_US)
diff --git a/src/plat/am335x/machine/hardware.c b/src/plat/am335x/machine/hardware.c
index a48ff7c9106e40da7cef5fbf7202e08c5adf7eec..308d069ca92aef2542edc77a66f532ce8681471f 100644
--- a/src/plat/am335x/machine/hardware.c
+++ b/src/plat/am335x/machine/hardware.c
@@ -20,111 +20,6 @@
 #include <plat/machine/hardware.h>
 
 
-#define CMPER_REG(base, off) ((volatile uint32_t *)((base) + (off)))
-#define CMPER_TIMER3_CLKCTRL    0x84
-#define CMPER_CLKCTRL_DISABLE   0
-#define CMPER_CLKCTRL_ENABLE    2
-#define CMPER_CLKSEL_TIMER3     0x50c
-#define CMPER_CKLSEL_MOSC       1
-
-
-#define INTCPS_SYSCONFIG_SOFTRESET BIT(1)
-#define INTCPS_SYSSTATUS_RESETDONE BIT(0)
-#define INTCPS_CONTROL_NEWIRQAGR BIT(0)
-#define INTCPS_SIR_IRQ_SPURIOUSIRQFLAG 0xffffff80
-
-/*
- * The struct below is used to discourage the compiler from generating literals
- * for every single address we might access.
- */
-volatile struct INTC_map {
-    uint32_t padding[4];
-    uint32_t intcps_sysconfig;
-    uint32_t intcps_sysstatus;
-    uint32_t padding2[10];
-    uint32_t intcps_sir_irq;
-    uint32_t intcps_sir_fiq;
-    uint32_t intcps_control;
-    uint32_t intcps_protection;
-    uint32_t intcps_idle;
-    uint32_t padding3[3];
-    uint32_t intcps_irq_priority;
-    uint32_t intcps_fiq_priority;
-    uint32_t intcps_threshold;
-    uint32_t padding4[5];
-    struct {
-        uint32_t intcps_itr;
-        uint32_t intcps_mir;
-        uint32_t intcps_mir_clear;
-        uint32_t intcps_mir_set;
-        uint32_t intcps_isr_set;
-        uint32_t intcps_isr_clear;
-        uint32_t intcps_pending_irq;
-        uint32_t intcps_pending_fiq;
-    } intcps_n[4];
-    uint32_t intcps_ilr[128];
-} *intc = (volatile void*)INTC_PPTR;
-
-
-/**
-   DONT_TRANSLATE
- */
-
-interrupt_t
-getActiveIRQ(void)
-{
-    uint32_t intcps_sir_irq = intc->intcps_sir_irq;
-    interrupt_t irq = (interrupt_t)(intcps_sir_irq & 0x7f);
-
-    if ((intcps_sir_irq & INTCPS_SIR_IRQ_SPURIOUSIRQFLAG) == 0) {
-        assert((irq / 32) < (sizeof intc->intcps_n / sizeof intc->intcps_n[0]));
-        if (intc->intcps_n[irq / 32].intcps_pending_irq & (1 << (irq & 31))) {
-            return irq;
-        }
-    }
-    return irqInvalid;
-}
-
-/* Check for pending IRQ */
-bool_t isIRQPending(void)
-{
-    return getActiveIRQ() != irqInvalid;
-}
-
-/* Enable or disable irq according to the 'disable' flag. */
-/**
-   DONT_TRANSLATE
-*/
-void
-maskInterrupt(bool_t disable, interrupt_t irq)
-{
-    assert(irq <= maxIRQ);
-    if (disable) {
-        intc->intcps_n[irq / 32].intcps_mir_set = 1 << (irq & 31);
-    } else {
-        intc->intcps_n[irq / 32].intcps_mir_clear = 1 << (irq & 31);
-    }
-}
-
-/* Handle a platform-reserved IRQ. */
-void handleReservedIRQ(irq_t irq)
-{
-}
-
-void
-ackInterrupt(irq_t irq)
-{
-    /*
-     * am335x ref man, sec 6.2.2 only requires a DSB after NEWIRQAGR.
-     * I found that without dsb() or more code before, I get interrupts
-     * without the associated pending bit being set. Perhaps this
-     * indicates a missing barrier in code elsewhere? -TimN
-     */
-    dsb();
-    intc->intcps_control = INTCPS_CONTROL_NEWIRQAGR;
-    dsb();
-}
-
 #define TIMER_INTERVAL_MS (CONFIG_TIMER_TICK_MS)
 
 #define TIOCP_CFG_SOFTRESET BIT(0)
@@ -264,14 +159,6 @@ initIRQController(void)
     while (!(intc->intcps_sysstatus & INTCPS_SYSSTATUS_RESETDONE)) ;
 }
 
-void
-handleSpuriousIRQ(void)
-{
-    /* Reset and re-enable IRQs. */
-    intc->intcps_control = INTCPS_CONTROL_NEWIRQAGR;
-    dsb();
-}
-
 void plat_cleanL2Range(paddr_t start, paddr_t end) {}
 void plat_invalidateL2Range(paddr_t start, paddr_t end) {}
 void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end) {}
diff --git a/src/plat/apq8064/machine/hardware.c b/src/plat/apq8064/machine/hardware.c
index 8ce072ebd48b557c0bf05fe1591e08d73324fd6d..1a2e02d2d3d910c8781f8d15670bf05c05203cd3 100644
--- a/src/plat/apq8064/machine/hardware.c
+++ b/src/plat/apq8064/machine/hardware.c
@@ -20,12 +20,6 @@
 #include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
 
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-}
-
 void plat_cleanL2Range(paddr_t start, paddr_t end) {}
 void plat_invalidateL2Range(paddr_t start, paddr_t end) {}
 void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end) {}
diff --git a/src/plat/exynos4/machine/Makefile b/src/plat/exynos4/machine/Makefile
index c020b6923b0b874aeea0b26556c1e526ce173786..e8438175fb3e2730a3f99b23dcf0f3d1150e295f 100644
--- a/src/plat/exynos4/machine/Makefile
+++ b/src/plat/exynos4/machine/Makefile
@@ -11,6 +11,4 @@
 DIRECTORIES += src/plat/${PLAT}/machine
 DIRECTORIES += src/plat/exynos_common
 
-PLAT_C_SOURCES += machine/hardware.c
-
 PLAT_C_SOURCES += ../exynos_common/mct.c ../exynos_common/io.c
diff --git a/src/plat/exynos4/machine/hardware.c b/src/plat/exynos4/machine/hardware.c
deleted file mode 100644
index d8a528920cb8f3b87cadce6b84edd2af4a273ed7..0000000000000000000000000000000000000000
--- a/src/plat/exynos4/machine/hardware.c
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
- *
- * @TAG(GD_GPL)
- */
-
-#include <config.h>
-#include <types.h>
-#include <machine/io.h>
-#include <kernel/vspace.h>
-#include <arch/machine.h>
-#include <arch/kernel/vspace.h>
-#include <plat/machine.h>
-#include <arch/linker.h>
-#include <plat/machine/devices.h>
-#include <plat/machine/hardware.h>
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-}
-
-
diff --git a/src/plat/exynos5/machine/hardware.c b/src/plat/exynos5/machine/hardware.c
index 8730fdd6cac80e07fd3dbda6661208473e893b36..30b8eaeb2745dbe47763df24f0f5b844b3dc47f8 100644
--- a/src/plat/exynos5/machine/hardware.c
+++ b/src/plat/exynos5/machine/hardware.c
@@ -19,16 +19,6 @@
 #include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
 
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-    if ((config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) && (irq == INTERRUPT_VGIC_MAINTENANCE)) {
-        VGICMaintenance();
-        return;
-    }
-}
-
 void plat_cleanL2Range(paddr_t start, paddr_t end) {}
 void plat_invalidateL2Range(paddr_t start, paddr_t end) {}
 void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end) {}
diff --git a/src/plat/hikey/machine/hardware.c b/src/plat/hikey/machine/hardware.c
index 92c93a60062dc5db12a2b884ee2aedd17d3a76ea..c2e427ded4dff0c56baaa2cc5c69d9f366811441 100644
--- a/src/plat/hikey/machine/hardware.c
+++ b/src/plat/hikey/machine/hardware.c
@@ -19,14 +19,6 @@
 #include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
 
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-}
-
-
-
 #define TIMER_CLOCK_HZ		1200000
 #define TIMER_RELOAD_VAL	(TIMER_CLOCK_HZ * CONFIG_TIMER_TICK_MS / 1000)
 
diff --git a/src/plat/imx31/machine/hardware.c b/src/plat/imx31/machine/hardware.c
index 4c047fc8717b53e5c73fe6dc6ef09b008f4097ea..d7f3fad694cbdaea04ff9b2e83fc72d3b0a5c6d8 100644
--- a/src/plat/imx31/machine/hardware.c
+++ b/src/plat/imx31/machine/hardware.c
@@ -27,78 +27,6 @@
 #define L2_LINE_START(a) ROUND_DOWN(a, L2_LINE_SIZE_BITS)
 #define L2_LINE_INDEX(a) (L2_LINE_START(a)>>L2_LINE_SIZE_BITS)
 
-/* Memory map for AVIC (Advanced Vectored Interrupt Controller). */
-volatile struct avic_map {
-    uint32_t intctl;
-    uint32_t nimask;
-    uint32_t intennum;
-    uint32_t intdisnum;
-    uint32_t intenableh;
-    uint32_t intenablel;
-    uint32_t inttypeh;
-    uint32_t inttypel;
-    uint32_t nipriority[8];
-    uint32_t nivecsr;
-    uint32_t fivecsr;
-    uint32_t intsrch;
-    uint32_t intsrcl;
-    uint32_t intfrch;
-    uint32_t intfrcl;
-    uint32_t nipndh;
-    uint32_t nipndl;
-    uint32_t fipndh;
-    uint32_t fipndl;
-    uint32_t vector[64];
-} *avic = (volatile void *)AVIC_PPTR;
-
-/* Get the active IRQ number from the AVIC.  Returns 0xff if
- * there isn't one. Note this is also known as irqInvalid */
-/**
-   DONT_TRANSLATE
- */
-interrupt_t
-getActiveIRQ(void)
-{
-    return (avic->nivecsr >> 16) & 0xff;
-}
-
-/* Check for pending IRQ */
-bool_t isIRQPending(void)
-{
-    return getActiveIRQ() != irqInvalid;
-}
-
-/* Enable or disable irq according to the 'disable' flag. */
-/**
-   DONT_TRANSLATE
-*/
-void
-maskInterrupt(bool_t disable, interrupt_t irq)
-{
-    if (disable) {
-        avic->intdisnum = irq;
-    } else {
-        avic->intennum = irq;
-    }
-}
-
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
-    if (irq == KERNEL_PMU_IRQ) {
-        handleOverflowIRQ();
-    }
-#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
-}
-
-void
-ackInterrupt(irq_t irq)
-{
-    /* empty on this platform */
-}
-
 /* Memory map for EPIT (Enhanced Periodic Interrupt Timer). */
 volatile struct epit_map {
     uint32_t epitcr;
@@ -257,9 +185,3 @@ initIRQController(void)
     /* Do nothing */
 }
 
-void
-handleSpuriousIRQ(void)
-{
-    /* Do nothing */
-}
-
diff --git a/src/plat/imx6/machine/Makefile b/src/plat/imx6/machine/Makefile
index 88c7afac7181c6d20d9089e59ab6cda112ebac5e..eca30a0280e8f0f17f71c6bf1b7e10cf50a797a4 100644
--- a/src/plat/imx6/machine/Makefile
+++ b/src/plat/imx6/machine/Makefile
@@ -10,5 +10,4 @@
 
 DIRECTORIES += src/plat/${PLAT}/machine
 
-PLAT_C_SOURCES += machine/hardware.c \
-                  machine/io.c
+PLAT_C_SOURCES += machine/io.c
diff --git a/src/plat/imx6/machine/hardware.c b/src/plat/imx6/machine/hardware.c
deleted file mode 100644
index 381c36a72c26893113846ec8fc8826b4cbfe5fee..0000000000000000000000000000000000000000
--- a/src/plat/imx6/machine/hardware.c
+++ /dev/null
@@ -1,36 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
- *
- * @TAG(GD_GPL)
- */
-
-#include <config.h>
-#include <types.h>
-#include <machine/io.h>
-#include <kernel/vspace.h>
-#include <arch/machine.h>
-#include <arch/kernel/vspace.h>
-#include <plat/machine.h>
-#include <arch/linker.h>
-#include <plat/machine/devices.h>
-#include <plat/machine/hardware.h>
-#include <stdint.h>
-#include <arch/benchmark_overflowHandler.h>
-
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
-    if (irq == KERNEL_PMU_IRQ) {
-        handleOverflowIRQ();
-    }
-#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
-}
-
-
-
diff --git a/src/plat/imx7/machine/hardware.c b/src/plat/imx7/machine/hardware.c
index 75aaf07049a8e396e9723f63265959379ba125f6..ba4ab338a847d247a61f48dfea07e1d099b598d4 100644
--- a/src/plat/imx7/machine/hardware.c
+++ b/src/plat/imx7/machine/hardware.c
@@ -18,12 +18,6 @@
 #include <arch/linker.h>
 #include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-}
-
 
 /* co-processor code to read and write GPT */
 
diff --git a/src/plat/omap3/machine/hardware.c b/src/plat/omap3/machine/hardware.c
index de50d4fc4b2c62ec042f64d39e5e1f2d6a3c5766..3fa8c137d93468dbb119c1cae8621bb17de575a5 100644
--- a/src/plat/omap3/machine/hardware.c
+++ b/src/plat/omap3/machine/hardware.c
@@ -19,104 +19,8 @@
 #include <plat/machine/devices.h>
 #include <plat/machine/hardware.h>
 
-
-
 #define INTCPS_SYSCONFIG_SOFTRESET BIT(1)
 #define INTCPS_SYSSTATUS_RESETDONE BIT(0)
-#define INTCPS_SIR_IRQ_SPURIOUSIRQFLAG 0xFF0000
-
-/*
- * The struct below is used to discourage the compiler from generating literals
- * for every single address we might access.
- */
-volatile struct INTC_map {
-    uint32_t padding[4];
-    uint32_t intcps_sysconfig;
-    uint32_t intcps_sysstatus;
-    uint32_t padding2[10];
-    uint32_t intcps_sir_irq;
-    uint32_t intcps_sir_fiq;
-    uint32_t intcps_control;
-    uint32_t intcps_protection;
-    uint32_t intcps_idle;
-    uint32_t padding3[3];
-    uint32_t intcps_irq_priority;
-    uint32_t intcps_fiq_priority;
-    uint32_t intcps_threshold;
-    uint32_t padding4[5];
-    struct {
-        uint32_t intcps_itr;
-        uint32_t intcps_mir;
-        uint32_t intcps_mir_clear;
-        uint32_t intcps_mir_set;
-        uint32_t intcps_isr_set;
-        uint32_t intcps_isr_clear;
-        uint32_t intcps_pending_irq;
-        uint32_t intcps_pending_fiq;
-    } intcps_n[3];
-    uint32_t padding5[8];
-    uint32_t intcps_ilr[96];
-} *intc = (volatile void*)INTC_PPTR;
-
-/**
-   DONT_TRANSLATE
- */
-
-interrupt_t
-getActiveIRQ(void)
-{
-    uint32_t intcps_sir_irq = intc->intcps_sir_irq;
-    interrupt_t irq = (interrupt_t)(intcps_sir_irq & 0x7f);
-
-    /* Ignore spurious interrupts. */
-    if ((intcps_sir_irq & INTCPS_SIR_IRQ_SPURIOUSIRQFLAG) == 0) {
-        assert(irq <= maxIRQ);
-        if (intc->intcps_n[irq / 32].intcps_pending_irq & (1 << (irq & 31))) {
-            return irq;
-        }
-    }
-
-    /* No interrupt. */
-    return 0xff;
-}
-
-/* Check for pending IRQ */
-bool_t isIRQPending(void)
-{
-    return getActiveIRQ() != 0xff;
-}
-
-/* Enable or disable irq according to the 'disable' flag. */
-/**
-   DONT_TRANSLATE
-*/
-void
-maskInterrupt(bool_t disable, interrupt_t irq)
-{
-    if (disable) {
-        intc->intcps_n[irq / 32].intcps_mir_set = 1 << (irq & 31);
-    } else {
-        intc->intcps_n[irq / 32].intcps_mir_clear = 1 << (irq & 31);
-    }
-}
-
-/* Handle a platform-reserved IRQ. */
-void handleReservedIRQ(irq_t irq)
-{
-    /* We shouldn't be receiving any reserved IRQs anyway. */
-    maskInterrupt(true, irq);
-
-    return;
-}
-
-void
-ackInterrupt(irq_t irq)
-{
-    intc->intcps_control = 1;
-    /* Ensure the ack has hit the interrupt controller before potentially
-     * re-enabling interrupts. */
-    dsb();
-}
 
 #define TIMER_INTERVAL_MS (CONFIG_TIMER_TICK_MS)
 
@@ -201,18 +105,6 @@ initIRQController(void)
     while (!(intc->intcps_sysstatus & INTCPS_SYSSTATUS_RESETDONE)) ;
 }
 
-/**
-   DONT_TRANSLATE
- */
-void
-handleSpuriousIRQ(void)
-{
-    /* Reset and re-enable IRQs. */
-    intc->intcps_control = 1;
-    dsb();
-}
-
-
 void plat_cleanL2Range(paddr_t start, paddr_t end) {}
 void plat_invalidateL2Range(paddr_t start, paddr_t end) {}
 void plat_cleanInvalidateL2Range(paddr_t start, paddr_t end) {}
diff --git a/src/plat/pc99/machine/hardware.c b/src/plat/pc99/machine/hardware.c
index 89a164d141af7462dc9571788b4eca49d10c71f1..19920ee5b2919d228e2388c3501ebd9dd473e7c2 100644
--- a/src/plat/pc99/machine/hardware.c
+++ b/src/plat/pc99/machine/hardware.c
@@ -33,58 +33,6 @@ void platAddDevices(void)
     } );
 }
 
-/* ============================== interrupts/IRQs ============================== */
-
-/* Handle a platform-reserved IRQ. */
-void handleReservedIRQ(irq_t irq)
-{
-    if (config_set(CONFIG_IOMMU) && irq == irq_iommu) {
-        vtd_handle_fault();
-        return;
-    }
-}
-
-/* Get the IRQ number currently working on. */
-irq_t getActiveIRQ(void)
-{
-    if (x86KScurInterrupt == int_invalid) {
-        return irqInvalid;
-    } else {
-        return x86KScurInterrupt - IRQ_INT_OFFSET;
-    }
-}
-
-/* Checks for pending IRQ */
-bool_t isIRQPending(void)
-{
-    if (apic_is_interrupt_pending()) {
-        return true;
-    }
-#ifdef CONFIG_IRQ_PIC
-    if (pic_is_irq_pending()) {
-        return true;
-    }
-#endif
-    return false;
-}
-
-void ackInterrupt(irq_t irq)
-{
-#ifdef CONFIG_IRQ_PIC
-    if (irq <= irq_isa_max) {
-        pic_ack_active_irq();
-    } else
-#endif
-    {
-        apic_ack_active_interrupt();
-    }
-}
-
-void handleSpuriousIRQ(void)
-{
-    /* Do nothing */
-}
-
 /* ============================== timer ============================== */
 
 void resetTimer(void)
diff --git a/src/plat/tk1/machine/hardware.c b/src/plat/tk1/machine/hardware.c
index 6df28f43d8d6efd3c305d1d6dab995e6e8f936dc..35f32416b15523e429be111f1e0a14b38fc3f8f0 100644
--- a/src/plat/tk1/machine/hardware.c
+++ b/src/plat/tk1/machine/hardware.c
@@ -21,30 +21,7 @@
 #include <plat/machine/smmu.h>
 #include <arch/benchmark_overflowHandler.h>
 
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
-    if (irq == KERNEL_PMU_IRQ) {
-        handleOverflowIRQ();
-    }
-#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
-
-    if ((config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) && (irq == INTERRUPT_VGIC_MAINTENANCE)) {
-        VGICMaintenance();
-        return;
-    }
-
-    if (config_set(CONFIG_ARM_SMMU) && (irq == INTERRUPT_SMMU)) {
-        plat_smmu_handle_interrupt();
-        return;
-    }
-
-}
-
 /* co-processor code to read and write GPT */
-
 static void
 write_cntp_ctl(uint32_t v)
 {
diff --git a/src/plat/zynq7000/machine/Makefile b/src/plat/zynq7000/machine/Makefile
index fde620e5a55c0e07144f0c0e06960f3b49e6b6f9..36753b6caf476895a9332ed54755171757b17319 100644
--- a/src/plat/zynq7000/machine/Makefile
+++ b/src/plat/zynq7000/machine/Makefile
@@ -8,4 +8,4 @@
 # @TAG(GD_GPL)
 #
 
-PLAT_C_SOURCES += machine/hardware.c machine/io.c
+PLAT_C_SOURCES += machine/io.c
diff --git a/src/plat/zynq7000/machine/hardware.c b/src/plat/zynq7000/machine/hardware.c
deleted file mode 100644
index ee469dc6a7906d807d5aa2f5f73c30a274efd83b..0000000000000000000000000000000000000000
--- a/src/plat/zynq7000/machine/hardware.c
+++ /dev/null
@@ -1,36 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
- *
- * @TAG(GD_GPL)
- */
-
-#include <config.h>
-#include <types.h>
-#include <machine/io.h>
-#include <kernel/vspace.h>
-#include <arch/machine.h>
-#include <arch/kernel/vspace.h>
-#include <plat/machine.h>
-#include <arch/linker.h>
-#include <plat/machine/devices.h>
-#include <plat/machine/hardware.h>
-#include <arch/benchmark_overflowHandler.h>
-
-/* Handle a platform-reserved IRQ. */
-void
-handleReservedIRQ(irq_t irq)
-{
-#ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
-    if (irq == KERNEL_PMU_IRQ) {
-        handleOverflowIRQ();
-    }
-#endif /* CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT */
-}
-
-
-
-