I'm tring to understand how the alien thread works. I'm not confident in what I have got.

Please correct me:

When an alien thread invokes an IPC call, it raises an exception, which would be caught by the

excenption handler as configured.

The exception handler could get the status of the alien thread by reading exception regs in UTCB

( l4_utcb_exc() ).

The exception handler could also set this IPC call allowed or not.

If this IPC call is allowed, the alien thread acts like a non-alien thread the performs the IPC call.

// This is what I doubt since the alien example does not provide a valid IPC call.

If this IPC call is not allowed, the alien thread executes from where it raise the exception.