search

utahplt / chorex

Choreographic programming in Elixir
https://hex.pm/packages/chorex
MIT License
14 stars 0 forks source link

channel choice? #7

Open bennn opened 3 weeks ago

bennn commented 3 weeks ago

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:

Screenshot 2024-06-10 at 2 34 37 PM

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 commented 3 weeks ago

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

ashton314 commented 3 weeks ago

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