Index: kernel/arch/ia32/src/asm.S
===================================================================
--- kernel/arch/ia32/src/asm.S	(revision a7220ded2adcc7fd89141a6e52314711ef30dee8)
+++ kernel/arch/ia32/src/asm.S	(revision c8cd9a87c0d92113f6ee42360d37e17847cbdef9)
@@ -175,10 +175,4 @@
 
 /*
- * Size of the entire istate structure including the error word and the
- * hardware-saved part.
- */
-#define ISTATE_REAL_SIZE  (ISTATE_SOFT_SIZE + 24)
-
-/*
  * The SYSENTER syscall mechanism can be used for syscalls with
  * four or fewer arguments. To pass these four arguments, we
@@ -191,5 +185,9 @@
 .global sysenter_handler
 sysenter_handler:
-	subl $(ISTATE_REAL_SIZE), %esp
+
+	/*
+	 * Note that the space needed for the istate structure has been
+	 * preallocated on the stack by before_thread_runs_arch().
+	 */
 
 	/*
@@ -260,6 +258,4 @@
 	movl ISTATE_OFFSET_ESP(%esp), %ecx
 
-	addl $(ISTATE_REAL_SIZE), %esp
-	
 	sysexit   /* return to userspace */
 
Index: kernel/arch/ia32/src/proc/scheduler.c
===================================================================
--- kernel/arch/ia32/src/proc/scheduler.c	(revision a7220ded2adcc7fd89141a6e52314711ef30dee8)
+++ kernel/arch/ia32/src/proc/scheduler.c	(revision c8cd9a87c0d92113f6ee42360d37e17847cbdef9)
@@ -39,4 +39,5 @@
 #include <arch.h>
 #include <arch/context.h>  /* SP_DELTA */
+#include <arch/interrupt.h>
 #include <arch/pm.h>
 #include <arch/asm.h>
@@ -63,5 +64,5 @@
 	if (CPU->arch.fi.bits.sep) {
 		/* Set kernel stack for CP3 -> CPL0 switch via SYSENTER */
-		write_msr(IA32_MSR_SYSENTER_ESP, kstk);
+		write_msr(IA32_MSR_SYSENTER_ESP, kstk - sizeof(istate_t));
 	}