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)
) 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.
On Tue 23-Feb-2016 2:59 PM, ぷ风过无痕?? wrote:
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
EPState_Recv ——> EPState_Idle ——>EPState_send
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).
EPState_Recv ——> EPState_Idle
Am I right???
Devel mailing list
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.