Tasks in Modular Proofs of Concurrent Algorithms

TL;DR

This paper introduces a systematic method to convert concurrent task specifications into sequential ones, enabling modular, computer-checked proofs of distributed algorithms that lack inherent sequential specifications.

Contribution

It presents a novel transformation technique for tasks into sequential specifications, facilitating modular proof construction in distributed algorithms.

Findings

Transformations enable modular proofs for any task.

Supports composition of proofs using sequential objects.

Applied to renaming algorithms with splitters.

Abstract

Proving correctness of distributed or concurrent algorithms is a mind-challenging and complex process. Slight errors in the reasoning are difficult to find, calling for computer-checked proof systems. In order to build computer-checked proofs with usual tools, such as Coq or TLA+, having sequential specifications of all base objects that are used as building blocks in a given algorithm is a requisite to provide a modular proof built by composition. Alas, many concurrent objects do not have a sequential specification. This article describes a systematic method to transform any task, a specification method that captures concurrent one-shot distributed problems, into a sequential specification involving two calls, Set and Get. This transformation allows system designers to compose proofs, thus providing a framework for modular computer-checked proofs of algorithms designed using tasks and sequential objects as building blocks. The Moir&Anderson implementation of renaming using splitters is an iconic example of such algorithms designed by composition.