+// void sysFlushDcache( void *p, size_t len );
+// 64-bit version
+// %rdi = ptr, %rsi = length
+COMMPAGE_FUNCTION_START(sys_flush_dcache_64, 64, 4)
+ testq %rsi,%rsi // length 0?
+ jz 2f // yes
+ mfence // ensure previous stores make it to memory
+ clflush -1(%rdi,%rsi) // make sure last line is flushed
+1:
+ clflush (%rdi) // flush a line
+ addq $64,%rdi
+ subq $64,%rsi
+ ja 1b
+ mfence // make sure memory is updated before we return
+2: