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.
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.
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
commented
5 months ago
The approach of using
seL4_NBSendRecvin 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.https://github.com/seL4/microkit/blob/ad271b5c1b4df2f16d43cafc1bfe1f7faf6d2de5/libmicrokit/src/main.c#L60
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
initprocedure until everything else in the system is also ready to start theirinitprocedure. 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.