return (((cycle_t) hi) << 32) + lo;
 }
+
+void gic_start_count(void)
+{
+       u32 gicconfig;
+
+       /* Start the counter */
+       gicconfig = gic_read(GIC_REG(SHARED, GIC_SH_CONFIG));
+       gicconfig &= ~(1 << GIC_SH_CONFIG_COUNTSTOP_SHF);
+       gic_write(GIC_REG(SHARED, GIC_SH_CONFIG), gicconfig);
+}
+
+void gic_stop_count(void)
+{
+       u32 gicconfig;
+
+       /* Stop the counter */
+       gicconfig = gic_read(GIC_REG(SHARED, GIC_SH_CONFIG));
+       gicconfig |= 1 << GIC_SH_CONFIG_COUNTSTOP_SHF;
+       gic_write(GIC_REG(SHARED, GIC_SH_CONFIG), gicconfig);
+}
+
 #endif
 
 static bool gic_local_irq_is_routable(int intr)
 
 extern cycle_t gic_read_compare(void);
 extern void gic_write_compare(cycle_t cnt);
 extern void gic_write_cpu_compare(cycle_t cnt, int cpu);
+extern void gic_start_count(void);
+extern void gic_stop_count(void);
 extern void gic_send_ipi(unsigned int intr);
 extern unsigned int plat_ipi_call_int_xlate(unsigned int);
 extern unsigned int plat_ipi_resched_int_xlate(unsigned int);