+static void mark_clear_cache(void *target)
+{
+ u_long offset = (char *)target - (char *)BASE_ADDR;
+ u_int mask = 1u << ((offset >> 12) & 31);
+ if (!(needs_clear_cache[offset >> 17] & mask)) {
+ char *start = (char *)((u_long)target & ~4095ul);
+ start_tcache_write(start, start + 4096);
+ needs_clear_cache[offset >> 17] |= mask;
+ }
+}
+