diff --git a/libsel4platsupport/src/plat/pc99/hpet.c b/libsel4platsupport/src/plat/pc99/hpet.c
index b96deef..8a1f40d 100644
--- a/libsel4platsupport/src/plat/pc99/hpet.c
+++ b/libsel4platsupport/src/plat/pc99/hpet.c
@@ -37,6 +37,15 @@
     seL4_IRQHandler_Ack(data->irq);
 }
 
+static void
+hpet_destroy(seL4_timer_t *timer, vka_t *vka, vspace_t *vspace)
+{
+    timer_common_data_t *timer_data = (timer_common_data_t *) timer->data;
+    timer_common_destroy_frame(timer, vka, vspace);
+    /* clear the irq */
+    seL4_IRQHandler_Clear(timer_data->irq);
+}
+
 seL4_timer_t *
 sel4platsupport_get_hpet(vspace_t *vspace, simple_t *simple, acpi_t *acpi,
                                        vka_t *vka, seL4_CPtr notification, uint32_t irq_number)
@@ -53,7 +62,7 @@
     }
 
     /* check what range the IRQ is in */
-    hpet->destroy = timer_common_destroy;
+    hpet->destroy = hpet_destroy;
 
     if ((int)irq_number >= MSI_MIN || irq_number <= MSI_MAX) {
         irq = irq_number + IRQ_OFFSET;
diff --git a/libsel4platsupport/src/timer_common.c b/libsel4platsupport/src/timer_common.c
index ec17c59..e332482 100644
--- a/libsel4platsupport/src/timer_common.c
+++ b/libsel4platsupport/src/timer_common.c
@@ -18,23 +18,34 @@
 #ifdef CONFIG_LIB_SEL4_VSPACE
 
 static void
+timer_common_destroy_frame_internal(timer_common_data_t *data, vka_t *vka, vspace_t *vspace)
+{
+    if (data->vaddr != NULL) {
+        vspace_unmap_pages(vspace, data->vaddr, 1, seL4_PageBits, VSPACE_PRESERVE);
+    }
+    if (data->frame.capPtr != 0) {
+        vka_cnode_delete(&data->frame);
+        vka_cspace_free(vka, data->frame.capPtr);
+    }
+}
+
+void
+timer_common_destroy_frame(seL4_timer_t *timer, vka_t *vka, vspace_t *vspace)
+{
+    timer_common_data_t *timer_data = (timer_common_data_t *) timer->data;
+    if (timer_data != NULL) {
+        timer_common_destroy_frame_internal(timer_data, vka, vspace);
+    }
+}
+
+static void
 timer_common_destroy_internal(timer_common_data_t *timer_data, vka_t *vka, vspace_t *vspace)
 {
     if (timer_data != NULL) {
-
+        timer_common_destroy_frame_internal(timer_data, vka, vspace);
         if (timer_data->irq != 0) {
             seL4_IRQHandler_Clear(timer_data->irq);
-            cspacepath_t irq_path;
-            vka_cspace_make_path(vka, timer_data->irq, &irq_path);
-            vka_cnode_delete(&irq_path);
-            vka_cspace_free(vka, timer_data->irq);
-        }
-        if (timer_data->vaddr != NULL) {
-            vspace_unmap_pages(vspace, timer_data->vaddr, 1, seL4_PageBits, VSPACE_PRESERVE);
-        }
-        if (timer_data->frame.capPtr != 0) {
-            vka_cnode_delete(&timer_data->frame);
-            vka_cspace_free(vka, timer_data->frame.capPtr);
+            timer_common_cleanup_irq(vka, timer_data->irq);
         }
         free(timer_data);
     }
diff --git a/libsel4platsupport/src/timer_common.h b/libsel4platsupport/src/timer_common.h
index 358ab0e..59827c1 100644
--- a/libsel4platsupport/src/timer_common.h
+++ b/libsel4platsupport/src/timer_common.h
@@ -33,8 +33,9 @@
                                        vka_t *vka, seL4_CPtr notification, uint32_t irq_number, void *paddr);
 
 /*
- * Something went wrong, clean up everything we did in timer_common_init.
+ * clean up functions
  */
+void timer_common_destroy_frame(seL4_timer_t *timer, vka_t *vka, vspace_t *vspace);
 void timer_common_destroy(seL4_timer_t *timer, vka_t *vka, vspace_t *vspace);
 void timer_common_cleanup_irq(vka_t *vka, seL4_CPtr irq);
 
diff --git a/libsel4vspace/arch_include/arm/vspace/arch/page.h b/libsel4vspace/arch_include/arm/vspace/arch/page.h
index 6b1e678..c6c1226 100644
--- a/libsel4vspace/arch_include/arm/vspace/arch/page.h
+++ b/libsel4vspace/arch_include/arm/vspace/arch/page.h
@@ -42,6 +42,8 @@
 #define seL4_ARCH_Default_VMAttributes seL4_ARM_Default_VMAttributes
 #define seL4_ARCH_VMAttributes         seL4_ARM_VMAttributes
 #define seL4_ARCH_4KPage               seL4_ARM_SmallPageObject
+#define seL4_ARCH_LargePageObject      seL4_ARM_LargePageObject
+/* for the size of a large page use seL4_LargePageBits */
 /* Remap does not exist on all kernels */
 #define seL4_ARCH_Page_Remap           seL4_ARM_Page_Remap
 #define ARCHPageGetAddress             ARMPageGetAddress
diff --git a/libsel4vspace/arch_include/x86/vspace/arch/page.h b/libsel4vspace/arch_include/x86/vspace/arch/page.h
index 896f514..74d44b8 100644
--- a/libsel4vspace/arch_include/x86/vspace/arch/page.h
+++ b/libsel4vspace/arch_include/x86/vspace/arch/page.h
@@ -38,6 +38,8 @@
 #define seL4_ARCH_VMAttributes         seL4_X86_VMAttributes
 #define seL4_ARCH_4KPage               seL4_X86_4K
 #define seL4_ARCH_Uncached_VMAttributes seL4_X86_CacheDisabled
+#define seL4_ARCH_LargePageObject      seL4_X86_LargePageObject
+/* for size of a large page object use seL4_LargePageBits */
 /* Remap does not exist on all kernels */
 #define seL4_ARCH_Page_Remap           seL4_X86_Page_Remap
 #define ARCHPageGetAddress             X86PageGetAddress