Kishon's Poker Game

TL;DR

This paper introduces a novel approach for verifying distributed algorithms' correctness by using high-level Tarskian system executions, demonstrated through the Kishon's Poker algorithm, which simplifies reasoning about concurrency.

Contribution

The paper presents a new method for correctness proofs of distributed algorithms that separates process specifications from communication objects, improving clarity and abstraction.

Findings

The approach effectively proves correctness without interleaving complexities.

Kishon's Poker algorithm serves as a practical example for the new method.

Comparison shows advantages over standard global state-based proofs.

Abstract

We present an approach for proving the correctness of distributed algorithms that obviate interleaving of processes' actions. The main part of the correctness proof is conducted at a higher abstract level and uses Tarskian system executions that combine two separate issues: the specification of the serial process that executes its protocol alone (no concurrency here), and the specification of the communication objects (no code here). In order to explain this approach a short algorithm for two concurrent processes that we call "Kishon's Poker" is introduced and is used as a platform where this approach is compared to the standard one which is based on the notions of global state, step, and history.