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
[email protected]
https://sel4.systems/lists/listinfo/devel
