一句话：提出一种高层分布式算法语言及自动优化，将复杂同步条件转为增量更新，从而高效实现逻辑量化。
该文研究如何既保持分布式算法高层、清晰的描述方式，又避免基于消息历史序列的逻辑量化同步条件导致低效执行和无界内存。作者设计了一种高层分布式算法语言，给出其操作语义，并提出新优化：在消息收发时自动将复杂同步条件转换为必要辅助值的增量更新，其核心是首个通用且高效实现逻辑量化的方法。文中还实现了编译器与优化原型，并在多种重要分布式算法上成功应用。评估表明，该语言与实现能够支撑从清晰描述到高效执行的转换。
This article describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows in which complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly. We present new optimizations that automatically transform complex synchronization conditions into incremental updates of necessary auxiliary values as messages are sent and received. The core of the optimizations is the first general method for efficient implementation of logic quantifications. We have developed an operational semantics of the language, implemented a prototype of the compiler and the optimizations, and successfully used the language and implementation on a variety of important distributed algorithms.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{LiuSL17,
title = {From Clarity to Efficiency for Distributed Algorithms},
author = {Yanhong A. Liu and Scott D. Stoller and Bo Lin},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {39},
number = {3},
year = {2017},
doi = {10.1145/2994595}
}