Static analysis of the synchronization structure of concurrent programs
Richard N. Taylor · 1980
Software systems which are composed of multiple, asynchronous, communicating processes are increasingly common, often appearing in embedded applications such as avionics systems, life-support systems, and nuclear reactor controllers. Techniques for assisting in ensuring the functional correctness of such systems are few but are clearly needed. The development of one such technique is the subject of this dissertation. In particular, research into the feasibility of developing static analysis techniques is presented. The questions of determining the various ways processes can synchronize, determining what program actions can occur in parallel, and detecting errors in the synchronization structure which result in infinite wait are all explored. Programs written in Ada and Ada-like programming languages are the particular subject of the research, such languages being chosen because of their higher level synchronization mechanisms and potential widespread application. Two major results are presented. The first is a demonstration that, for arbitrary programs, the analysis questions posed above must be considered intractable. The second result is the development of an analysis procedure which, in spite of being exponential in nature, is expected to be able to perform the specified analysis in an acceptably efficient manner for many standard applications. Also presented with the analysis procedure is a programming methodology whose application promotes efficient analysis as well as more understandable concurrent programs. Though the research focusses upon Ada programs the results are at such a level as to be applicable to other concurrent programming languages, such as CSP. In particular the results only depend upon the basic notion of a nondeterministic rendezvous.