Tutorial

Tutorials given at conferences:

• Tutorial at PPoPP 2014: Programming Distributed Algorithms

• Tutorial at SPLASH 2014: Programming Distributed Algorithms

• Tutorial at PODC 2017: High-Level Specification of Distributed Algorithms (slides)

• Tutorial at PODC 2019: From Classical to Blockchain Consensus: What are the Exact Algorithms? (slides)

• Tutorial at RV 2020: Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness (slides, with a demo in video, code, tutorial paper in proceedings)

• Tutorial at PLDI 2023 (cross-listed at PODC 23): High-Level Executable Specification and Reasoning for Improving Distributed Algorithms (slides)

• Tutorial at ICDCS 2024: Consensus Algorithms from Classical To Blockchain: Quickly Program, Configure, Run, and Check (slides, including complete programs for 6 algorithms used in the demo: Two-Phase Commit, Basic Paxos, Multi-Paxos, Byzantine BPCon, Bitcoin Backbone, Leaderless OFT-Archipelago, short paper in proceedings)

Papers with details on DistAlgo and Paxos:

• From Clarity to Efficiency for Distributed Algorithms (OOPSLA 2012)

(DistAlgo language, compilation, optimization, implementation, and experiments with a dozen examples)

• High-Level Executable Specifications of Distributed Algorithms (SSS 2012)

(Methods for writing high-level specifications, with parts of multi-Paxos as a main example)

• From Clarity to Efficiency for Distributed Algorithms (arXiv 2014, revised 2017, TOPLAS 39(3) 2017)

(Extended description of DistAlgo language and optimization method, with a formal operational semantics)

• Moderately Complex Paxos Made Simple: High-Level Specification of Distributed Algorithms (arXiv 2017, PPDP 2019)

(Basic Paxos and Multi-Paxos for distributed consensus written at a high level in DistAlgo, code, liveness studied in a separate paper, video at PODC 2021)

Lamport's distributed mutual exclusion algorithm in DistAlgo: