+ /*
+ * Finally, call machine-dependent code to release the remaining
+ * resources including address space, the kernel stack and pcb.
+ * The address space is released by "vmspace_free(p->p_vmspace)";
+ * This is machine-dependent, as we may have to change stacks
+ * or ensure that the current one isn't reallocated before we
+ * finish. cpu_exit will end with a call to swtch(), finishing
+ * our execution (pun intended).
+ */
+ cpu_exit(p);
+ /* NOTREACHED */