Fix approach used for making PDs passive at run-time

[Ivan-Velickovic]

The approach of using seL4_NBSendRecv in the event handler loop of libmicrokit when PDs essentially 'make' themselves passive by sending a message to the monitor is not ideal for multiple reasons.

microkit/libmicrokit/src/main.c

Line 60 in ad271b5

tag = seL4_NBSendRecv(signal, signal_msg, INPUT_CAP, &badge, REPLY_CAP);

1. It will not scale/work in multi-core setups. Given that it is a non-blocking send, a scenario may occur where the monitor is already dealing with a message from one PD (meaning that it is not waiting on an endpoint) and another PD that wants to make itself passive on another core which means the message will be lost.
2. It affects verification as it leads to assumptions needing to be made about the scheduling of the system.

This issue was found in the process of verifying the passive PD changes in Microkit.

The current proposed solution is to have synchronisation using notifications so that all PDs block until they receive a notification from the monitor that all PDs that needed to be converted to passive have completed. This means that no PDs start their init procedure until everything else in the system is also ready to start their init procedure. This should remove any concurrency issues such as what happens when a PD is in the middle of being converted to passive and another PD on a separate core tries to communicate with it, I believe this may lead to lost notifications.

This solution is not final as we have not implemented and evaluated it, however, from our internal discussions it I think it is the cleanest solution and should require minimal changes to Microkit.

[gernotheiser]

+1