Index: sys/amd64/amd64/fpu.c
===================================================================
--- sys/amd64/amd64/fpu.c
+++ sys/amd64/amd64/fpu.c
@@ -916,6 +916,11 @@
 
 #define	FPU_KERN_CTX_FPUINITDONE 0x01
 #define	FPU_KERN_CTX_DUMMY	 0x02	/* avoided save for the kern thread */
+#ifdef INVARIANTS
+#define	FPU_KERN_CTX_INUSE	 0x04
+#else
+#define	FPU_KERN_CTX_INUSE	 0x00
+#endif
 
 struct fpu_kern_ctx {
 	struct savefpu *prev;
@@ -940,6 +945,7 @@
 fpu_kern_free_ctx(struct fpu_kern_ctx *ctx)
 {
 
+	KASSERT((ctx->flags & FPU_KERN_CTX_INUSE) == 0, ("free'ing inuse ctx"));
 	/* XXXKIB clear the memory ? */
 	free(ctx, M_FPUKERN_CTX);
 }
@@ -959,14 +965,16 @@
 {
 	struct pcb *pcb;
 
+	KASSERT((ctx->flags & FPU_KERN_CTX_INUSE) == 0, ("using inuse ctx"));
+
 	if ((flags & FPU_KERN_KTHR) != 0 && is_fpu_kern_thread(0)) {
-		ctx->flags = FPU_KERN_CTX_DUMMY;
+		ctx->flags = FPU_KERN_CTX_DUMMY | FPU_KERN_CTX_INUSE;
 		return (0);
 	}
 	pcb = td->td_pcb;
 	KASSERT(!PCB_USER_FPU(pcb) || pcb->pcb_save ==
 	    get_pcb_user_save_pcb(pcb), ("mangled pcb_save"));
-	ctx->flags = 0;
+	ctx->flags = FPU_KERN_CTX_INUSE;
 	if ((pcb->pcb_flags & PCB_FPUINITDONE) != 0)
 		ctx->flags |= FPU_KERN_CTX_FPUINITDONE;
 	fpuexit(td);
@@ -982,8 +990,13 @@
 {
 	struct pcb *pcb;
 
+	KASSERT((ctx->flags & FPU_KERN_CTX_INUSE) != 0,
+	    ("leaving not inuse ctx"));
+	ctx->flags &= ~FPU_KERN_CTX_INUSE;
+
 	if (is_fpu_kern_thread(0) && (ctx->flags & FPU_KERN_CTX_DUMMY) != 0)
 		return (0);
+	/* XXX - is this KASSERT needed? */
 	KASSERT((ctx->flags & FPU_KERN_CTX_DUMMY) == 0, ("dummy ctx"));
 	pcb = td->td_pcb;
 	critical_enter();