Index: generic/src/main/main.c
===================================================================
--- generic/src/main/main.c	(revision 39539da93686d95cdb2334c202ac8cb2ad77347e)
+++ generic/src/main/main.c	(revision 7453929d2544639ed584538be3d0bcaa203a825c)
@@ -166,7 +166,7 @@
 		config.base, hardcoded_ktext_size/1024, hardcoded_kdata_size/1024);
 
-	arch_late_init();
-	
+	arch_pre_smp_init();
 	smp_init();
+	arch_post_smp_init();
 	printf("config.memory_size=%dM\n", config.memory_size/(1024*1024));
 	printf("config.cpu_count=%d\n", config.cpu_count);