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.
翻译:基于Future实现的乱序编排能显著改善延迟与吞吐量,但其实际表现取决于通信延迟、计算时间、故障与恢复等资源因素。现有形式化模型(如Ozone的O3)虽能描述可能出现的执行序列,却无法直接解释这些执行发生的概率或持续时间。本文提出AsInst——一种用于建模具有乱序执行能力的异步编排语义的概率性资源感知语言。AsInst程序被解释为时间贝叶斯网络,同时建模运行时产生的数值及其可用时间。我们证明该核心语义能正确对应基于Future的网络语义,并展示AsInst可编码Ozone风格的选择合并条件语句。通过案例研究,我们完成了通信故障恢复建模与运行时性能分析。