PicoServer App - get_sender_id() returning wrong value

[samikool]

Apologies if this is the wrong place for this question, but I am having a problem with the PicoServer App.

Essentially, I have ported an ethernet driver from the Zynq7000 to the Zync Ultrascale+, and am trying to use the PicoServer App to test it. It works about 90% of the time I load and run it, but sometimes it flakes out. I have done a lot of investigation but am a bit stuck as this is the first project I have worked on in either seL4 or camkes.

Right now, I have the Listener component start up and get its socket into the listening state, then I signal the echo client to start up and attempt to make a connection. From my understanding of the app, these components should enter the while loop at the bottom and call seL4_Wait(() and then be woken up by the PicoServer when their socket receives an event. However, I am running into one of two scenarios.

1. I leave the seL4_Wait() call alone, and the Listener socket is never woken up, even though, when I trace down the TCP/IP stack, I see the syn from the Echo going out and trying to make the connection.

2. I change seL4_Wait() to and seL4_Poll() call, and the connection is made between the two components, however at times it doesn't work as mentioned above. Specifically when I attempt to send data, either data is not sent, or it says data is sent but the listener doesn't actually receive anything.

I am a little stuck on where to start debugging situation 1, but in situation 2, I have traced the problem to when the component checks its client_id, which then corresponds to what socket gets returned from the PicoServer. A call is made to pico_send_get_sender_id(), which switches on the pico_send_badge to return the ID of the Echo component. At times pico_send_badge is not correctly set to the Echo component's badge, which is causing the wrong badge to get returned, which then causes the wrong client_id to get returned, which then causes the wrong socket to get returned. The stack then attempts to send from the Listener socket instead of the echo socket, which obviously causes an error. At times the error happens on the receiving end, where the Echo component's socket is returned and it tries to receive the data it just sent to the Listener socket, which again causes an error.

My best guess is that since there is a single handle message function being called by potentially two different component threads, that the pico_send_badge is not getting read/written correctly at times. I've tried adding the volatile keyword, but it didn't fix this issue.

I am a bit at a loss on how to progress in debugging this issue. If anyone has any suggestions, or needs more info please let me know. This is my first issue on creation on Github so if this is the wrong place for this or I'm leaving something out please let me know.