Greetings

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 complete: void 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); break; } 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: devel@sel4.systems 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 sartakov@ksyslabs.org

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- Vasily A. Sartakov sartakov@ksyslabs.org