From Clarity to Efficiency for Distributed Algorithms

标题：分布式算法从清晰到高效分布式算法是分布式系统的核心，在日常生活中越来越不可或缺。从搜索引擎到社交网络，从云计算到移动计算，以低成本开发高保证高性能的分布式应用程序的能力是几乎所有计算机应用程序成功和增长的关键。然而，开发具有严格正确性保证的分布式算法的高效实现仍然是一项具有挑战性的、反复出现的任务。这个项目开发了非常先进的方法和工具，用于高级规范和分布式算法的高效实现，并提供正式和严格验证的正确性保证。该项目还将这些结果应用于最重要和最困难的分布式算法，并将这些结果用于开发教材。更广泛的影响是对高效、可靠和健壮的分布式系统的开发以及分布式系统的语言和算法教学的显著改进。为了轻松而清晰地表达和推理分布式算法，该项目开发了DistAlgo语言，该语言将高级不确定性控制与高级消息历史查询相结合，用于指定同步条件。用于获得高效实现的方法通过系统地将昂贵的查询转换成高效的增量计算，从一般的非确定性控制和从对消息历史的量化两者生成高效的消息处理程序。正确性保证方法首先将DistAlgo转换为TLA+；其次，为了使具有挑战性的验证任务可行，它使用适当的形式化验证工具，如TLA工具箱，利用规范中的高层结构。智能的优点是一种强大而严格的语言，它结合了伪代码语言、形式规范语言和分布式算法编程语言的优点；提出了一种通过增量来进行程序优化的原则性方法，即微积分中的离散对应；以及用于分布式算法的形式验证的新技术。

Title: From Clarity to Efficiency for Distributed AlgorithmsDistributed algorithms are at the core of distributed systems, which are increasingly indispensable in daily lives. From search engines to social networks, and from cloud computing to mobile computing, the ability to develop high-assurance high-performance distributed applications at low cost is the key to the success and growth of virtually all computer applications. Yet, developing efficient implementations of distributed algorithms with rigorous correctness guarantees remains a challenging, recurring task. This project develops significantly advanced methods and tools for high-level specifications and efficient implementations of distributed algorithms with formally and rigorously verified correctness guarantees. The project also applies the results to the most important and difficult distributed algorithms and uses the results in developing teaching materials. The broader impacts are significant improvements to the development of efficient, reliable, and robust distributed systems, and to the teaching of languages and algorithms for distributed systems.To express and to reason about distributed algorithms easily and clearly, the project develops the language DistAlgo, which combines high-level non-deterministic control with high-level message-history queries for specifying synchronization conditions. The method for obtaining efficient implementations generates efficient message handlers from both general non-deterministic control and from quantifications over message histories, by systematically transforming expensive queries into efficient incremental computations. The method for correctness guarantees first translates DistAlgo to TLA+; next, to make the challenging verification tasks feasible, it uses appropriate formal verification tools like TLA Toolbox, to exploit high-level constructs in the specifications. The intellectual merits are a powerful and rigorous language that combines advantages of pseudocode languages, formal specification languages, and programming languages for distributed algorithms; advancement of a principled method for program optimization by incrementalization, the discrete counterpart of differentiation in calculus; and new technologies for formal verification of distributed algorithms.