> The test is basically doing the following:
> 1- test_ep_recycle() creates a badged ep.
> 2- The call_func() thread invoke seL4_Call(), (the second invocation). At 
> this point, call_func() thread blocks waiting for a reply (on the same ep).
> 3- test_ep_recycle() recycles all badged ep caps (including the one 
> call_func() is blocking on). The kernel then invalidates cnodes of these 
> endpoints, and set the state of the thread blocking on it as 
> ThreadState_Restart, hence it will restart to do the seL4_Call() again.
> 4- call_func() thread resumes (restarted) and tries to do seL4_Call() on 
> invalid endpoint which is no longer in its cspace, and should get the error 
> seL4_InvalidCapability as a label.

thank you for explanation 

> One thing to check is to make sure the the call_func() thread is actually 
> "Restarted" (assuming that arch-independent recycle code works correctly) 
> meaning that it tries to invoke seL4_Call() again (the actual swi/trap-like 
> instruction) after test_cp_recycle() recycles its endpoint. The 
> arch-dependent functions in the kernel to do this are getRestartPC() and 
> setNextPC().

I think that the problem is somewhere here, i.e. with  "getRestartPC()" and 
"setNextPC()». The second one is clear: we set address to return when syscall 

setNextPC(tcb_t *thread, word_t v)
    setRegister(thread, LR_svc, v);

and here I am using CP0_EPC, But what about FaultInstruction? Is it an address 
of instruction which causes «syscall»? If so, this code is a bit strange: 

    case ThreadState_Restart: {
        word_t pc;

        pc = getRestartPC(ksCurThread);
        setNextPC(ksCurThread, pc);
        setThreadState(ksCurThread, ThreadState_Running);

we take address that causes syscall from the ksCurThread and set them back. 
Thus, FaultInstruction should point to something different, right? 

> Hope that helps.
> Regards,
> Hesham
> ________________________________________
> From: Devel <> on behalf of Vasily A.Sartakov 
> <>
> Sent: Friday, October 14, 2016 12:33 AM
> To:
> Subject: [seL4] endpoint.c
> Hello.
> I have a problem with endpoint.c test (RECYCLE0001):
> Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 
> of file /long/path/apps/sel4test-tests/src/tests/endpoints.c
> I am reading MR(0) in call_func above this check  and see, that seL4_Call 
> returns values that were sent before. For example, 100 for the first thread, 
> 101 for the second and etc. Thus, as far I understand, cnode_recycle does not 
> work at all. I am pretty sure that my seL4_Call syscall was implemented 
> properly. I have looked inside the kernel, and tried to track everything 
> related to cteRecycle and do not see anything platform specific. I know that 
> it is a complicated question, but any ideas or hints where to look?
> Thank you
> --
> Vasily A. Sartakov
> _______________________________________________
> Devel mailing list

Vasily A. Sartakov

Devel mailing list

Reply via email to