Step in Tine: Forking Processes in Functional Choreographies
This work solves a known limitation in choreographic programming by adding dynamic process forking, benefiting developers of concurrent systems who need both safety guarantees and flexibility.
The authors introduce λ⨝, the first functional choreographic language with process forking, enabling dynamic spawning of processes while guaranteeing deadlock freedom. They demonstrate its applicability to load balancers and parallel divide-and-conquer.
Traditional concurrent-programming techniques require programmers to painstakingly write programs for each participant in a concurrent system. Choreographic programming, in contrast, allows a programmer to write one centralized program and compile it to individual programs. This approach simplifies critical properties like deadlock freedom, but it complicates forking new processes, a core primitive in concurrent programming. This work addresses that gap with the choreographic fork calculus $λ{\pitchfork}$, the first functional choreographic language with process forking. $λ{\pitchfork}$ provides a deadlock-freedom guarantee while allowing programs to dynamically determine when to spawn new processes, what they will do, and who will communicate with them. In doing so, it supports practical applications like load balancers and parallel divide-and-conquer.