Index: kernel/arch/arm32/include/arch/cycle.h
===================================================================
--- kernel/arch/arm32/include/arch/cycle.h	(revision 3bacee1839e6f355100ab4ea86bb211e9ecf19ed)
+++ kernel/arch/arm32/include/arch/cycle.h	(revision 1cac8753dba1dcd1e470087cba35d1d4f93975a2)
@@ -52,7 +52,10 @@
 	if ((ID_PFR1_read() & ID_PFR1_GEN_TIMER_EXT_MASK) ==
 	    ID_PFR1_GEN_TIMER_EXT) {
-	    uint32_t low = 0, high = 0;
-	    asm volatile( "MRRC p15, 0, %[low], %[high], c14": [low]"=r"(low), [high]"=r"(high));
-	   return ((uint64_t)high << 32) | low;
+		uint32_t low = 0, high = 0;
+		asm volatile (
+		    "MRRC p15, 0, %[low], %[high], c14"
+		    : [low] "=r" (low), [high] "=r" (high)
+		);
+		return ((uint64_t)high << 32) | low;
 	} else {
 		return (uint64_t)PMCCNTR_read() * 64;