Race condition in interrupt handling

Hello,

I'm playing around with L4:Pistachio on a 8-core machine a little bit, 
and it seems that I'm having a race condition in interrupt handling.

at src/api/v4/interrupt.cc, around Line 423:

             current->dequeue_send(handler_tcb);
             handler_tcb->set_tag(msg_tag_t::irq_tag());
             handler_tcb->set_partner(current->get_global_id());
             handler_tcb->unlock();

The routine overrides the handler_tcb directly. However, the handler 
might be in the middle of IPC (where it's in locked_waiting state in my 
machine), thus the handler enters an undefined state.

So what happens to my machine is that the program runs on L4:Pistachio, 
it can process the mouse interrupt for a while, then the interrupt 
controller goes into an inconsistent state:


     IRQ 12: IOAPIC 8, Line 12: vec 80, phys, high,  edge, masked dest 0
          redir entries mismatch hw        0      50 != soft        0   
10050
             hw: vec 80, phys, high,  edge, unmasked dest 0

I have no idea of how to fix it. Any suggestions are highly appreciated.

Cheers,

Haohui