diff --git a/hermit/usr/examples/jacobi.c b/hermit/usr/examples/jacobi.c
index 88bcf3f02..64fc55558 100644
--- a/hermit/usr/examples/jacobi.c
+++ b/hermit/usr/examples/jacobi.c
@@ -45,7 +45,7 @@ static unsigned long long start_tsc;
 inline static unsigned long long rdtsc(void)
 {
 	unsigned long lo, hi;
-	asm volatile ("rdtsc; mfence" : "=a"(lo), "=d"(hi) :: "memory");
+	asm volatile ("rdtsc" : "=a"(lo), "=d"(hi) :: "memory");
 	return ((unsigned long long) hi << 32ULL | (unsigned long long) lo);
 }
 
diff --git a/hermit/usr/examples/stream.c b/hermit/usr/examples/stream.c
index 549946bf6..9ac2937b2 100644
--- a/hermit/usr/examples/stream.c
+++ b/hermit/usr/examples/stream.c
@@ -422,7 +422,7 @@ static unsigned long long start_tsc;
 inline static unsigned long long rdtsc(void)
 {
 	unsigned long lo, hi;
-	asm volatile ("rdtsc; mfence" : "=a"(lo), "=d"(hi) :: "memory");
+	asm volatile ("rdtsc" : "=a"(lo), "=d"(hi) :: "memory");
 	return ((unsigned long long) hi << 32ULL | (unsigned long long) lo);
 }