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
Hi all
A friendly reminder that the seL4 developer hangout is on again next week.
Tue 11 Jun, 22:00 UTC.
For your local date and time please see https://sel4.systems/contact/.
Zoom link: https://unsw.zoom.us/j/82640784431
Birgit Brecknell
seL4 Foundation Project Coordinator
Sydney, Australia
Mon 9-5
Wed 2-5
Fri 9-5
birgit(a)sel4.systems <mailto:birgit@sel4.systems>
bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>
Hello,
I'm currently working with seL4 & Polarfire (RISCV) and I'm working with a single core at the moment (doing some testing and understanding how seL4 works).
Polarfire has 4 cores and I'd like to start using all of them in a multikernel configuration (every hart running its own sel4 kernel).
I've found the following RFC: https://sel4.atlassian.net/browse/RFC-17 where Kent McLeod has done some work (https://github.com/kent-mcleod/camkes-manifest/blob/kent/multicore2/master.…) but only for ARM.
Does someone know if the same approach will be taken for RISCV? or even better, if someone has already done it?
Thanks,
David.
