从全局编排到可证明正确且高效的分布式实现
分布式、并行与集群计算
2019-06-03 v1 软件工程
摘要
我们定义了一种方法，用于从高阶全局编排自动综合可证明正确且高效的分布式实现。全局编排描述了由接口描述的一组所提供进程之间的执行与通信逻辑。编排层面的操作包括多方通信、选择、循环与分支。编排由主节点触发，即每个编排有一个主节点来触发其执行。这允许自动生成无冲突且无需控制器的分布式实现。所综合实现的执行行为遵循编排的行为。此外，控制器的缺失保证了实现的效率并减少了运行时所需的通信。进而，我们定义了将分布式实现翻译为等价的 Promela 版本。该翻译允许针对行为性质验证分布式系统。我们实现了一个 Java 原型来验证该方法，并将其应用于自动综合微服务架构。我们以自动综合一个经过验证的分布式购物系统为例说明了我们的方法。
引用
@article{arxiv.1905.13529,
title = {From Global Choreographies to Provably Correct and Efficient Distributed Implementations},
author = {Mohamad Jaber and Yliès Falcone and Paul Attie and Al-Abbass Khalil and Rayan Hallal},
journal= {arXiv preprint arXiv:1905.13529},
year = {2019}
}