You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Session types can de-multiplex messages incoming on one channel with the choice operator. But AFAIK they don't know what to do if several channels could receive a message at once.
This was a problem for AnQi in 6110 when he tried to model cache coherence protocols. There, the caches, directories, and interconnect layer could receive messages along several channels at any time:
Can choreographies demux sessions? (In general maybe not --- seems very hard to guarantee deadlock freedom.)
Apropos of deadlock-freedom: demuxing might come at the cost of deadlock-freedom; maybe that's a cost we're willing to bear. (The "Manifest Sharing with Session Types" paper drops deadlock-freedom to get closer to a real-world system.)
Session types can de-multiplex messages incoming on one channel with the choice operator. But AFAIK they don't know what to do if several channels could receive a message at once.
This was a problem for AnQi in 6110 when he tried to model cache coherence protocols. There, the caches, directories, and interconnect layer could receive messages along several channels at any time:

Can choreographies demux sessions? (In general maybe not --- seems very hard to guarantee deadlock freedom.)
The IRC paper does something very similar with full-duplex asynchony, but still I think it's not dealing with multiple channels at once:
https://doi.org/10.22152/programming-journal.org/2024/8/8
The text was updated successfully, but these errors were encountered: