Necessary and Sufficient Conditions on Partial Orders for Modeling Concurrent Computations

TL;DR

This paper establishes necessary and sufficient conditions for partial orders to model concurrent computations, introducing properties like width-extensibility and interleaving-consistency, and provides algorithms for model conversion and predicate detection.

Contribution

It defines key properties of partial orders that characterize valid models of concurrent computations and introduces algorithms for converting between event-based and state-based models.

Findings

Partial orders are valid models iff they are width-extensible.

Asynchronous models require both width-extensibility and interleaving-consistency.

The theory improves understanding and algorithms for checkpointing and predicate detection.

Abstract

Partial orders are used extensively for modeling and analyzing concurrent computations. In this paper, we define two properties of partially ordered sets: width-extensibility and interleaving-consistency, and show that a partial order can be a valid state based model: (1) of some synchronous concurrent computation iff it is width-extensible, and (2) of some asynchronous concurrent computation iff it is width-extensible and interleaving-consistent. We also show a duality between the event based and state based models of concurrent computations, and give algorithms to convert models between the two domains. When applied to the problem of checkpointing, our theory leads to a better understanding of some existing results and algorithms in the field. It also leads to efficient detection algorithms for predicates whose evaluation requires knowledge of states from all the processes in the system.