1 - https://news.ycombinator.com/item?id=48287718 is my post on tla formal modeling complete with examples and decent pdf to go with it. Self contained assumes no background on tla
2 - part of the reason for doing (1) was to model homa's basic protocol. See pdf. I did not go into homa details there because I wanted to stay focused on tla.
3 - I have a kernel bypass homa transport api in development
4 - as wonderful as homa is for intra-data-center IO, the srpt part of the protocol is a bit tough to performantly code. More or less homa wants each NIC resource to be managed by one owner who chooses from among all tx streams that could be sent, which one has smallest srpt (shortest remaining processing time). This applies despite the fact client/servers sharing the NIC run in their own threads. Ive been using mpsc memory rings moving the smallest amount of data i can.
1 - https://news.ycombinator.com/item?id=48287718 is my post on tla formal modeling complete with examples and decent pdf to go with it. Self contained assumes no background on tla
2 - part of the reason for doing (1) was to model homa's basic protocol. See pdf. I did not go into homa details there because I wanted to stay focused on tla.
3 - I have a kernel bypass homa transport api in development
4 - as wonderful as homa is for intra-data-center IO, the srpt part of the protocol is a bit tough to performantly code. More or less homa wants each NIC resource to be managed by one owner who chooses from among all tx streams that could be sent, which one has smallest srpt (shortest remaining processing time). This applies despite the fact client/servers sharing the NIC run in their own threads. Ive been using mpsc memory rings moving the smallest amount of data i can.