diff --git a/hermit/arch/x86/kernel/gdt.c b/hermit/arch/x86/kernel/gdt.c
index 6d73aaeba..5a16a36ca 100644
--- a/hermit/arch/x86/kernel/gdt.c
+++ b/hermit/arch/x86/kernel/gdt.c
@@ -52,7 +52,7 @@ size_t get_kernel_stack(void)
 {
 	task_t* curr_task = per_core(current_task);
 
-	return (size_t) curr_task->stack + curr_task->id * KERNEL_STACK_SIZE - 16; // => stack is 16byte aligned
+	return (size_t) curr_task->stack + KERNEL_STACK_SIZE - 0x10; // => stack is 16byte aligned
 }
 
 /* Setup a descriptor in the Global Descriptor Table */
diff --git a/hermit/kernel/tasks.c b/hermit/kernel/tasks.c
index a76114a8c..da17d4fd2 100644
--- a/hermit/kernel/tasks.c
+++ b/hermit/kernel/tasks.c
@@ -109,7 +109,7 @@ int set_idle_task(void)
 			task_table[i].status = TASK_IDLE;
                         task_table[i].last_core = core_id;
                         task_table[i].last_stack_pointer = NULL;
-                        task_table[i].stack = (char*) ((size_t)&boot_stack + core_id * KERNEL_STACK_SIZE);;
+                        task_table[i].stack = (char*) ((size_t)&boot_stack + core_id * KERNEL_STACK_SIZE);
                         task_table[i].prio = IDLE_PRIO;
                         spinlock_init(&task_table[i].vma_lock);
                         task_table[i].vma_list = NULL;
@@ -120,7 +120,6 @@ int set_idle_task(void)
 			per_core(current_task) = readyqueues[core_id].idle = task_table+i;
 			ret = 0;
 
-
 			break;
 		}
 	}