diff --git a/libsel4bench/arch_include/riscv/sel4bench/arch/sel4bench.h b/libsel4bench/arch_include/riscv/sel4bench/arch/sel4bench.h
index e652fb6..f42b54b 100644
--- a/libsel4bench/arch_include/riscv/sel4bench/arch/sel4bench.h
+++ b/libsel4bench/arch_include/riscv/sel4bench/arch/sel4bench.h
@@ -15,16 +15,18 @@
 
 #if __riscv_xlen == 32
 #define SEL4BENCH_READ_CCNT(var) \
-    uint32_t nH1, nL, nH2; \
-    asm volatile("rdcycleh %0\n" \
-                 "rdcycle %1\n" \
-                 "rdcycleh %2\n" \
-                 : "=r"(nH1), "=r"(nL), "=r"(nH2)); \
-    if (nH1 < nH2) { \
-        asm volatile("rdcycle %0" : "=r"(nL); \
-        nH1 = nH2; \
-    } \
-    var = ((uint64_t)((uint64_t) nH1 << 32 | (nL);
+    do { \
+        uint32_t nH1, nL, nH2; \
+        asm volatile("rdcycleh %0\n" \
+                    "rdcycle %1\n" \
+                    "rdcycleh %2\n" \
+                    : "=r"(nH1), "=r"(nL), "=r"(nH2)); \
+        if (nH1 < nH2) { \
+            asm volatile("rdcycle %0" : "=r"(nL)); \
+            nH1 = nH2; \
+        } \
+        var = ((uint64_t)nH1 << 32) | nL; \
+    } while(0)
 #else
 #define SEL4BENCH_READ_CCNT(var) \
     asm volatile("rdcycle %0" :"=r"(var));
@@ -36,16 +38,18 @@
 
 #if __riscv_xlen == 32
 #define SEL4BENCH_READ_PCNT(idx, var) \
-    uint32_t nH1, nL, nH2; \
-    asm volatile("csrr %0, hpmcounterh" #idx \
-                 "csrr %1, hpmcounter" #idx \
-                 "csrr %2, hpmcounterh" #idx \
-                 : "=r"(nH1), "=r"(nL), "=r"(nH2)); \
-    if (nH1 < nH2) { \
-        asm volatile("csrr %0, hpmcounter" #idx : "=r"(nL); \
-        nH1 = nH2; \
-    } \
-    var = ((uint64_t)((uint64_t) nH1 << 32 | (nL);
+    do { \
+        uint32_t nH1, nL, nH2; \
+        asm volatile("csrr %0, hpmcounterh" #idx \
+                    "csrr %1, hpmcounter" #idx \
+                    "csrr %2, hpmcounterh" #idx \
+                    : "=r"(nH1), "=r"(nL), "=r"(nH2)); \
+        if (nH1 < nH2) { \
+            asm volatile("csrr %0, hpmcounter" #idx : "=r"(nL)); \
+            nH1 = nH2; \
+        } \
+        var = ((uint64_t)nH1 << 32) | nL; \
+    } while(0)
 #else
 #define SEL4BENCH_READ_PCNT(idx, var) \
     asm volatile("csrr %0, hpmcounter" #idx : "=r"(var));