Probabilistic, Resource-Aware, Asynchronous, Out-of-Order Choreographies

Futures-based implementations of out-of-order choreographies can substantially improve latency and throughput, but their actual behavior depends on resources such as communication delay, computation time, failures, and recovery. Existing formal models such as Ozone's O3 describe which executions are possible, but do not directly explain how likely those executions are or how long they take. In this work we present AsInst, a probabilistic, resource-aware language for modeling the semantics of asynchronous choreographies with out-of-order execution. AsInst programs are interpreted as temporal Bayesian networks that model both the values produced at runtime and the times at which they become available. We prove that this central semantics correctly captures a corresponding futures-style network semantics. We also show that AsInst can encode Ozone-style select-and-merge conditionals, and we use case studies to model communication-failure recovery and analyze runtime performance.