Index: kernel/generic/src/main/main.c
===================================================================
--- kernel/generic/src/main/main.c	(revision c06eb06bfa73f0453ea411eebf5fa21013e9f555)
+++ kernel/generic/src/main/main.c	(revision d7e3fa668f022eef3ff46bde138d8a874b93f18d)
@@ -106,4 +106,6 @@
 size_t hardcoded_kdata_size = 0;	/**< Size of the kernel data in bytes. */
 
+uintptr_t stack_safe = 0;	/**< Lowest safe stack virtual address */
+
 void main_bsp(void);
 void main_ap(void);
@@ -133,6 +135,4 @@
 void main_bsp(void)
 {
-	uintptr_t stackaddr;
-
 	config.cpu_count = 1;
 	config.cpu_active = 1;
@@ -142,21 +142,21 @@
 	
 	config.kernel_size = ALIGN_UP(hardcoded_ktext_size + hardcoded_kdata_size, PAGE_SIZE);
-	stackaddr = config.base + config.kernel_size;
-	
-	/* Avoid placing kernel on top of init */
+	config.stack_size = CONFIG_STACK_SIZE;
+	
+	/* Initialy the stack is placed just after the kernel */
+	config.stack_base = config.base + config.kernel_size;
+	
+	/* Avoid placing stack on top of init */
 	count_t i;
-	bool overlap = false;
-	for (i = 0; i < init.cnt; i++)
-		if (PA_overlaps(stackaddr, CONFIG_STACK_SIZE, init.tasks[i].addr, init.tasks[i].size)) {
-			stackaddr = ALIGN_UP(init.tasks[i].addr + init.tasks[i].size, CONFIG_STACK_SIZE);
-			init.tasks[i].size = ALIGN_UP(init.tasks[i].size, CONFIG_STACK_SIZE) + CONFIG_STACK_SIZE;
-			overlap = true;
-		}
-	
-	if (!overlap)
-		config.kernel_size += CONFIG_STACK_SIZE;
+	for (i = 0; i < init.cnt; i++) {
+		if (PA_overlaps(config.stack_base, config.stack_size, init.tasks[i].addr, init.tasks[i].size))
+			config.stack_base = ALIGN_UP(init.tasks[i].addr + init.tasks[i].size, config.stack_size);
+	}
+	
+	if (config.stack_base < stack_safe)
+		config.stack_base = ALIGN_UP(stack_safe, PAGE_SIZE);
 	
 	context_save(&ctx);
-	context_set(&ctx, FADDR(main_bsp_separated_stack), stackaddr, THREAD_STACK_SIZE);
+	context_set(&ctx, FADDR(main_bsp_separated_stack), config.stack_base, THREAD_STACK_SIZE);
 	context_restore(&ctx);
 	/* not reached */
@@ -203,5 +203,6 @@
 
 	version_print();
-	printf("%.*p: hardcoded_ktext_size=%zdK, hardcoded_kdata_size=%zdK\n", sizeof(uintptr_t) * 2, config.base, hardcoded_ktext_size >> 10, hardcoded_kdata_size >> 10);
+	printf("kernel: %.*p hardcoded_ktext_size=%zdK, hardcoded_kdata_size=%zdK\n", sizeof(uintptr_t) * 2, config.base, hardcoded_ktext_size >> 10, hardcoded_kdata_size >> 10);
+	printf("stack:  %.*p size=%zdK\n", sizeof(uintptr_t) * 2, config.stack_base, config.stack_size >> 10);
 
 	arch_pre_smp_init();