>  I now see what is happening.  On the pmax, the initial SR value is
> initialized in the pcb before calling main().  However, the kernel has
> called tsleep() at least once prior to forking any kthread processes,
> and tsleep() results in cpu_switch() being called at a non-zero SPL.
> Cpu_switch() saves the current SR in the current pcb - oops.

The problem seems derived from a mismatch between pcb0 contents and
processor state at the time configure() completes inside main().

So, I propose here to make sure processor state (spl0) gets in sync
with pcb0 at the bottom of cpu_configure().  This could be done, [1]
special "trumpoline" code to make self-context switch of proc0 (==
kernel itself), or [2] uglier but just straight piece of codes.

I'm yet to investigate the usefulness of this idea.  Comment?

Tohru Nishimura