Basic results in automatic transformations of shared memory parallel programs into sequential programs

Abstract

We study the problem of developing a set of syntax-driven transformations for automatic translation of shared memory parallel programs into sequential programs. The result is a sequential program that is a “refinement” (its execution is consistent with one possible execution of the parallel program) of the original program. Consequently, the problem of debugging parallel programs is reduced to the problem of debugging sequential programs. Moreover, the efficiency of parallel programs can be increased by sequentializing code segments that include extra parallelism.

The main difficulty in developing such a system is to preserve the fairness property of any actual parallel execution, which states that no process can wait forever unserved. Thus, non termination of the sequential version (namely an infinite loop) is allowed only if there is at least one fair parallel execution that does not halt as well (i.e., a process that executes an infinite loop whose termination is not dependent on any other process).

We show that it is sufficient to consider the case of two sequential programs executed in parallel in order to solve the general case. We then describe several types of transformations and check their ability to preserve fairness. The results, with regards to the existence of such a transformation for general parallel programs are not conclusive; however, we do show that restricted cases (which are likely to appear in the reality) can be sequentialized using this set of transformations. The problem of detecting bad execution sequences is discussed in the last section. In particular, wrong versions of mutual exclusion algorithms are discussed. It is shown that synchronous type of transformations might overlook bad execution sequences of these algorithms. A new type of transformation, which works by nesting parallel while-loops, is developed. Indeed, it is shown that the transformed program reveals the known bug of Hyman's algorithm for mutual exclusion.