Hi Indan, That makes a lot of sense. Thanks for the explanation. Best, Sid
On Mon, Aug 7, 2023 at 3:04 AM Indan Zupancic <in...@nul.nu> wrote: > [CAUTION: Non-UBC Email] > > Hello Sid, > > On 2023-08-05 03:05, Sid Agrawal wrote: > > I have a scenario and would like to understand how the kernel is > > expected > > to behave when I change the CSpace of a TCB when it is blocked on an > > EP. > > CSpace matters when system calls are done. That is, all access checks > are > done at the start of the system call. So changing the CSpace afterwards > should have no effect for on-going system calls. > > However, there is one exception: The CSpace change can cause the last > references to kernel objects to disappear, which will trigger the > destruction of those objects, with all side-effects. > > The root CSpace can be seen as a special cap slot in the TCB object. > Changing it will delete the old root cap, and if that was the only > reference to the CNode, then all the objects pointed to will also lose > a reference recursively. When an object has no references left, it is > deleted. > > > 1. A TCB (say TCB_1) is blocked on seL4_reply() on an endpoint (say > > EP_1). > > I'm assuming you mean seL4_Recv() or seL4_Call() here, seL4_reply() is > non-blocking. > > > 2. Now, another PD, which has the capability to TCB_1, changes the > > CSpace > > of TCB_1 by using seL4_TCB_SetSpace(). Let's assume that the VSpace is > > identical. > > > > This new CSpace can be different from the old CSpace in 4 ways: > > A. It doesn't have the endpoint EP_1 > > B. It has the endpoint EP_1 but at a different CSlot. > > C. It has the endpoint EP_1 at the same CSlot. But since it is a > > different > > CSpace(so CNodes shared), it is a minted copy of the EP_1. Let's call > > it > > EP_1-prime. > > D. It has the endpoint EP_1 at the same CSlot, and it is the same EP as > > I > > have shared the CNode containing the EP_1 from the original CSpace. New > > and > > old CSpaces share the CNode containing that EP_1 like two trees sharing > > a > > sub-tree. > > So what happens depends on whether EP_1 still exists after the call, > where > or how it fits on the CSpace doesn't matter. That is, cases A-D all > behave > the same if EP_1 still exists. Only in the case of A can EP_1 disappear, > in > which case the system call should return an error. > > Greetings, > > Indan > _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
