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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to