A Systematic Approach to Parallel Program Verification

Tadao TAKAOKA
Department of Computer Science, Ibaraki University, Hitachi, Ibaraki 316, Japan.
takaoka@cis.ibaraki.ac.jp

Abstract

In this paper we investigate parallel program verification with directed graphs and assertion matrices. The parallel computational model is that with shared variables and comprising processes run asynchronously. A program graph is a direct product of the flowcharts of comprising processes. The vertices of the graph correspond to global control points of the given parallel program, and each edge corresponds to an execution of one statement of one process, whereby the control moves in the process. We attach assertions to the vertices in the graph, and statements to the edges which are either assignment statements or branching operations. If we can verify the consistencies of the assertions over edges, we say the set of assertions are induced by the parallel program and the pre-condition. It is usually difficult to find these assertions.

When we only have two processes, the set of assertions becomes an assertion matrix. We show that the assertion matrix can be decomposed into an independent part and dependent part uniquely. Using this property, we can prove the independent part first and then the dependent part using the information so far obtained, that is, incrementally.

Finally a new concept of eventual correctness is introduced, which states the partial correctness of the parallel program and its eventual termination.

Conference Home Page