Compiler ensures safe stateful service composition across hardware targets
Coexponential Exploration in the Clef Programming Language
Programming LanguagesDistributed, Parallel, and Cluster ComputingLogic in Computer Science
Summary
Programming services that keep track of state and interact with many users is tricky, especially when running on different hardware. The authors study a way to keep these services organized and safe by tracking who owns what state and how requests are handled. Their method uses a special way to pause and resume work (continuations) to keep everything in order, even if messages get delayed or reordered. They also build proofs that these rules protect against common problems like deadlocks and inconsistent replies. This helps developers write normal stateful programs while the compiler makes sure they will work well across different machines.
What this means in practice
- •For concurrent software developers: Write stateful services with compiler-verified safe interaction patterns that work correctly across hardware platforms.
- •For distributed system engineers: Maintain request identity and prevent circular waits when handling distributed service requests that may suspend or reorder messages.
Authors
Houston Haynes
Abstract
Clef was created as a concurrent programming language whose compiler tracks state ownership, waiting computations and request dependencies. We develop a coexponential account of stateful services and their client pools within this design. Delimited continuations retain the computation and resources needed to complete each interaction. These structures give our compiler premises for verifying service composition and preserving it through native lowering to multiple hardware targets. We connect finite actor state transitions to the initial, service and final rules of a coexponential server. A separate operational account relates actor dispatch to single-use continuation frames. We prove state-ownership and reply preservation for that translation, give a finite communication-summary analysis, and circular-wait exclusion from the conditions needed. A further result identifies when changing service order preserves both state and replies. Our Program Semantic Graph retains these facts through compilation. We are researching reusable proofs to confirm the ownership and communication interfaces, while our BAREWire implementation connects message meaning to its unboxed representation across respective endpoints. A distributed worker example preserves request identity across suspension, reordered replies and boundary conversion. Urschel's elimination-growth bounds supply quantitative premises for a solver service, whose accuracy and failure budget compose with the protocol contract. The design we envision connects automatic structural analysis, reusable proof terms and native realization. Protocols determine the admissible interactions, continuations expose their storage requirements, and retained dependencies support differential compilation. Developers can express ordinary stateful services while the compiler carries the conditions for their correct composition across execution targets.