Some questions about L4 operating system