Using true concurrency to model execution of parallel programs

Abstract

Parallel execution of a program R (intuitively regarded as a partial order) is usually modeled by sequentially executing one of the total orders (interleavings) into which it can be embedded. Our work deviates from this serialization principle by using true concurrency to model parallel execution. True concurrency is represented via completions of R to semi total orders, called time diagrams. These orders are characterized via a set of conditions (denoted by Ct), yielding orders or time diagrams which preserve some degree of the intended parallelism in R. Another way to express semi total orders is to use re-writing or derivation rules (denoted by Cx) which for any program R generates a set of semi-total orders. This paper includes a classification of parallel execution into three classes according to three different types of Ct conditions. For each class a suitable Cx is found and a proof of equivalence between the set of all time diagrams satisfying Ct and the set of all terminal Cx derivations of R is devised. This equivalence between time diagram conditions and derivation rules is used to define a novel notion of correctness for parallel programs. This notion is demonstrated by showing that a specific asynchronous program enforces synchronous execution, which always halts, showing that true concurrency can be useful in the context of parallel program verification. © 1994 Plenum Publishing Corporation.