Keep it fair: Equivalence and composition

TitleKeep it fair: Equivalence and composition
Publication TypeJournal Article
Year of Publication2019
AuthorsMennicke, S., and T. Prehn
Refereed DesignationRefereed
JournalJournal of Logical and Algebraic Methods in Programming
Start Page1

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 first contribution is an equivalence spectrum in which fairness assumptions are preserved. Although the identified equivalences allow for reasoning about correctness incorporating fairness assumptions, this does not necessarily allow for the lifting of arguments from sequential processes to parallel compositions employing arbitrary synchronization mechanisms. Our second contribution is, therefore, an analysis of parallel composition operators and their synchronization mechanisms in this respect.