A Systematic Approach to Parallel Program Verification

概要

論文の詳細を見る
In this paper we investigate parallel program verification with directed graphs and assertion matrices. The parallel computational model is that with shared variables and constituent processes run asynchronously. A program graph is a direct product of the flowcharts of constituent processes. The vertices of the graph correspond to global control points of the given parallel program, and edges correspond 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 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.
一般社団法人情報処理学会の論文
1996-07-15