On Fri, Dec 07, 2007 at 04:51:55PM +0100, Manuel Bouyer wrote:
> Hum, I may have a clue. The xenevt (src/sys/arch/xen/xen/xenevt.c) bypass
> the SPL system. It shouldn't deal directly with the scheduler when
> ci->ci_ilevel >= IPL_SOFTSERIAL, but call softint_schedule().
> 
> The code is sys/arch/xen/xen/xenevt.c. The interrupt handler will call
> xenevt_event().

OK, it looks like it's because it can call softint_schedule() even if
ci_ilevel is >= IPL_HIGH. I'll try to come up with a solution based on
atomic ops only.

-- 
Manuel Bouyer <bouyer@antioche.eu.org>
     NetBSD: 26 ans d'experience feront toujours la difference
--