Keep it Fair: Equivalences

TL;DR

This paper introduces an equivalence spectrum for concurrent and distributed systems that preserves fairness assumptions, enabling more realistic and compositional correctness reasoning.

Contribution

It presents a novel spectrum of equivalences that maintain fairness assumptions, facilitating compositional correctness proofs in distributed systems.

Findings

Identifies equivalences that preserve fairness assumptions.

Enables compositional reasoning about correctness with fairness.

Improves modeling accuracy by filtering unrealistic behaviors.

Abstract

For models of concurrent and distributed systems, it is important and also challenging to establish correctness in terms of safety and/or liveness properties. Theories of distributed systems consider equivalences fundamental, since they (1) preserve desirable correctness characteristics and (2) often allow for component substitution making compositional reasoning feasible. Modeling distributed systems often requires abstraction utilizing nondeterminism which induces unintended behaviors in terms of infinite executions with one nondeterministic choice being recurrently resolved, each time neglecting a single alternative. These situations are considered unrealistic or highly improbable. Fairness assumptions are commonly used to filter system behaviors, thereby distinguishing between realistic and unrealistic executions. This allows for key arguments in correctness proofs of distributed systems, which would not be possible otherwise. Our contribution is an equivalence spectrum in which fairness assumptions are preserved. The identified equivalences allow for (compositional) reasoning about correctness incorporating fairness assumptions.