You are observing the common case, which is also the case the fastpath is optimized for, where the receive thread is typically queued on the endpoint before send thread attempts to send. This case is made more likely by ReplyWait and a trend of running servers (the ones doing the Recv) at a higher priority.

The Receive and Send states effectively differentiate which thread (sender or receiver) got to the endpoint first. The Receive state occurs when the endpoint state is Idle and a thread does a Recv. Then when the Send happens the send can complete straight away so the endpoint transitions to Idle. However, if the Send happens before the Recv, then the endpoint will still be in the Idle state and will transition to the Send state.

I cannot imagine how you 'tested' this, but if I do the same kernel change and run sel4test (which has fairly good, although not total, kernel code coverage) (https://github.inside.nicta.com.au/seL4/sel4test-manifest) I clearly see the endpoint going to the Send state.

You can test this quite trivially by implementing the following pseudo-code

seL4_CPtr endpoint = some how allocate and endpoint object
seL4_Send(endpoint, seL4_MessageInfo_new(0, 0, 0, 0));

And observe the endpoint immediately going into the Send state.

Adrian

On Tue 23-Feb-2016 2:59 PM, ぷ风过无痕?? wrote:
Hi everyone,
I find an interesting problem when I read the code of endpoint(kernel\src\object\endpoint.c). In the sendIPC and receiveIPC functions , I see there are 3 states for an endpoint(Idle , send , receive). Below it is the state machine diagram.
                           sendIPC
EPState_Recv ——> EPState_Idle ——>EPState_send

                           receiveIPC
EPState_send——> EPState_Idle ——>EPState_Recv 


But when I add some print infomation, I find the endpoint can never reach the Send state. I think the correct state machine diagram just has two states(idle and receive).
                           sendIPC
EPState_Recv ——> EPState_Idle

                           receiveIPC
EPState_Idle ——>EPState_Recv 

Am I right???


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



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.