From Clarity to Efficiency for Distributed Algorithms

Abstract

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

References in corpus (3)

• Applying Prolog to Develop Distributed Systems
• A Linear Logic Programming Language for Concurrent Programming over Graph Structures
• Demand-Driven Incremental Object Queries

Cited by in corpus (8)

• Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms
• Discrete Math with Programming: A Principled Approach
• Incremental Computation: What Is the Essence?
• Recursive Rules with Aggregation: A Simple Unified Semantics
• High-level Cryptographic Abstractions
• Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness
• Benchmarking for Integrating Logic Rules with Everything Else
• Algorithm Diversity for Resilient Systems