Hello, I'll give a brief introduction since this is my first message here. I'm an undergraduate research assistant at the University of British Columbia, and I'm working with Margo Seltzer (https://www.seltzer.com/margo/) in the Systopia Lab. I'm helping with development of Sid Agrawal's (https://sid-agrawal.ca/) project built on seL4. I'm trying to determine what is the correct way to handle this situation: 1. Process 1 makes an seL4_Call to an endpoint that Process 2 is listening on. 2. Process 2 receives the message, and since we are running in non-MCS kernel, it will get a reply capability in its TCB. 3. Process 2 dies, for whatever reason, before it can reply to Process 1. If we wanted to unblock Process 1, what would be the correct approach? - I can use seL4_CNode_SaveCaller in Process 2 as soon as it receives a message, and store the slot number in some shared memory with the root task. Then when Process 2 dies, the root task is able to move the reply capability into its own cspace and send a reply indicating an error. This is not ideal for our purpose, because we do not want Process 2 to be able to perform any operations on its own cspace, but it needs its own root cnode capability in order to perform seL4_CNode_SaveCaller. - Is seL4_Call the wrong function for this purpose? We also considered using NBRecv and considering the call a failure after some timeout period. This is also not ideal since we would lose the convenience of the Call's reply cap, etc. - Is there some other solution that we are missing? As an aside: I notice that for the MCS kernel, if the reply cap is deleted, Process 1's thread state would be moved from ThreadState_BlockedOnReceive to ThreadState_Inactive. In non-MCS kernel, it seems that the state would remain ThreadState_BlockedOnReceive? Is there a reason for this? Best, Arya