channel choice?

[bennn]

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

[bennn]

related: https://www.sciencedirect.com/science/article/pii/S0890540124000294

[ashton314]

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.)