一句话:提出动态编排语言AIOC并编译为APOC,保证运行时更新后分布式应用仍无死锁与竞态。
编写无通信死锁和竞态的分布式应用本身就很复杂,而在运行时更新应用后继续保持这些性质更加困难。本文提出一种面向可更新分布式应用的编排式(choreographic)编程方法。作者定义了动态交互导向编排语言 AIOC,允许程序员从全局视角指定应用中哪些部分可以在运行时被外部新的 AIOC 片段替换;AIOC 程序被编译为面向每个参与者的进程级语言 APOC。论文证明,由 AIOC 规约生成的 APOC 分布式应用无死锁且无竞态,并且这些性质在任意运行时更新之后仍然成立。作者还实现了名为 AIOCJ 的编程框架,包含集成开发环境、从 AIOC 扩展到分布式 Jolie 程序的编译器以及支持执行的运行时环境。
Programming distributed applications free from communication deadlocks and race conditions is complex. Preserving these properties when applications are updated at runtime is even harder. We present a choreographic approach for programming updatable, distributed applications. We define a choreography language, called Dynamic Interaction-Oriented Choreography (AIOC), that allows the programmer to specify, from a global viewpoint, which parts of the application can be updated. At runtime, these parts may be replaced by new AIOC fragments from outside the application. AIOC programs are compiled, generating code for each participant in a process-level language called Dynamic Process-Oriented Choreographies (APOC). We prove that APOC distributed applications generated from AIOC specifications are deadlock free and race free and that these properties hold also after any runtime update. We instantiate the theoretical model above into a programming framework called Adaptable Interaction-Oriented Choreographies in Jolie (AIOCJ) that comprises an integrated development environment, a compiler from an extension of AIOCs to distributed Jolie programs, and a runtime environment to support their execution.Comment: arXiv admin note: text overlap with arXiv:1407.0970
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{PredaGGLM16,
title = {Dynamic Choreographies: Theory And Implementation},
author = {Mila Dalla Preda and Maurizio Gabbrielli and Saverio Giallorenzo and Ivan Lanese and Jacopo Mauro},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
year = {2017},
doi = {10.23638/lmcs-13(2:1)2017}
}