diff --git a/sys/platform/vkernel64/platform/systimer.c b/sys/platform/vkernel64/platform/systimer.c
--- a/sys/platform/vkernel64/platform/systimer.c
+++ b/sys/platform/vkernel64/platform/systimer.c
@@ -78,6 +78,12 @@ static sysclock_t vktimer_target;
 static struct timespec vktimer_ts;
 static sysclock_t vktimer_reload[MAXCPU];
 
+/* DF-5568 verification instrumentation (NOT part of the fix) */
+static uint64_t vkt_if_cnt;	/* entries into the wakeup if-body */
+static uint64_t vkt_swap_cnt;	/* executions of the atomic_swap_long body */
+SYSCTL_QUAD(_debug, OID_AUTO, vkt_if, CTLFLAG_RD, &vkt_if_cnt, 0, "");
+SYSCTL_QUAD(_debug, OID_AUTO, vkt_swap, CTLFLAG_RD, &vkt_swap_cnt, 0, "");
+
 extern int use_precise_timer;
 
 /*
@@ -299,8 +305,11 @@ vktimer_intr_reload(struct cputimer_intr *cti __unused, sysclock_t reload)
 	reload += sys_cputimer->count();
 	vktimer_reload[mycpu->gd_cpuid] = reload;
 	if (vktimer_cotd && (ssysclock_t)(reload - vktimer_target) < 0) {
-		while ((sysclock_t)(reload - vktimer_target) < 0)
+		++vkt_if_cnt;
+		while ((ssysclock_t)(reload - vktimer_target) < 0) {
+			++vkt_swap_cnt;
 			reload = atomic_swap_long(&vktimer_target, reload);
+		}
 		cothread_wakeup(vktimer_cotd, &vktimer_ts);
 	}
 }