I am working on dynamic binary translator. Please tell me if anybody know if in L4-microkernel interrupted kernel PC is ever used in interrupt handlers?