paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Dynamic Choreographies: Theory And Implementation

动态编排:理论与实现
LMCS vol.Volume 13, Issue 22017匹配度 1/10 · 该论文属于编程语言与形式化方法中的动态编排/分布式程序编译,强调死锁与竞态自由及运行时更新,但未涉及用户核心关注的LLM/Agentic程序静态分析、AI辅助静态分析、浮点程序分析或贝叶斯程序分析。引用 65 inbox
Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, Jacopo Mauro
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:提出动态编排语言AIOC并编译为APOC,保证运行时更新后分布式应用仍无死锁与竞态。

编写无通信死锁和竞态的分布式应用本身就很复杂,而在运行时更新应用后继续保持这些性质更加困难。本文提出一种面向可更新分布式应用的编排式(choreographic)编程方法。作者定义了动态交互导向编排语言 AIOC,允许程序员从全局视角指定应用中哪些部分可以在运行时被外部新的 AIOC 片段替换;AIOC 程序被编译为面向每个参与者的进程级语言 APOC。论文证明,由 AIOC 规约生成的 APOC 分布式应用无死锁且无竞态,并且这些性质在任意运行时更新之后仍然成立。作者还实现了名为 AIOCJ 的编程框架,包含集成开发环境、从 AIOC 扩展到分布式 Jolie 程序的编译器以及支持执行的运行时环境。

问题
如何编写可在运行时更新的分布式应用,并在更新前后始终保持无通信死锁与无竞态。
方法
定义全局视角的动态交互导向编排语言 AIOC,将其编译为进程级语言 APOC,并证明生成应用及其运行时更新均保持无死锁、无竞态。
评估
通过理论证明建立 AIOC 到 APOC 编译及更新后的无死锁、无竞态性质,并实现 AIOCJ 框架(IDE、编译器和运行时)验证方法的可行性。
原文摘要(Abstract)

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

BibTeX
@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}
}