动态编排-分布式应用程序的安全更新
Dynamic Choreographies - Safe Runtime Updates of Distributed Applications
摘要：
编写没有通信死锁和竞争的分布式应用程序是复杂的。当应用程序在运行时更新时，保留这些属性就更难了。我们提出了DIOC，一种用于编程分布式应用程序的语言，该语言通过构造而免于死锁和竞争。DIOC程序将整个分布式应用程序描述为一个独特的实体（编排）。DIOC允许程序员指定应用程序的哪些部分可以更新。在运行时，这些部分可以被来自应用程序外部的新DIOC片段替换。DIOC程序是用一种称为DPOC的低级语言编译的，为每个站点生成代码。我们正式的DIOC和DPOC语义标记的过渡系统，并证明编译的正确性作为一个跟踪等价的结果。作为推论，DPOC应用程序没有通信死锁和竞争，即使在运行时更新的情况下也是如此。
英文摘要：
Programming distributed applications free from communication deadlocks and races is complex. Preserving these properties when applications are updated at runtime is even harder. We present DIOC, a language for programming distributed applications that are free from deadlocks and races by construction. A DIOC program describes a whole distributed application as a unique entity (choreography). DIOC allows the programmer to specify which parts of the application can be updated. At runtime, these parts may be replaced by new DIOC fragments from outside the application. DIOC programs are compiled, generating code for each site, in a lower-level language called DPOC. We formalise both DIOC and DPOC semantics as labelled transition systems and prove the correctness of the compilation as a trace equivalence result. As corollaries, DPOC applications are free from communication deadlocks and races, even in presence of runtime updates.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
