page_coloring_init_cpu
extern void page_coloring_init_cpu();
if (&page_coloring_init_cpu) {
page_coloring_init_cpu();