Distributed 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.
