Identification of Interfering Statements in a Shared Object Paradigm

. Some parallel programming languages allow objects to be shared by different processes under multiple variable names. In such languages correctness proving based on interference freedom tests is a problem since the control points where the same object is shared by different processes are not obvious. This paper proposes a method to statically identify shared objects and their control points. This is achieved by tracing the object ownership at intraoperation, interoperation and interprocess levels. 1 Introduction Owicki and Gries [6] have developed a proof methodology for proving the correctness of parallel programs with shared variables. In their methodology, the proof outlines are specified as Hoare triples, fQgSfRg with their usual meaning of partial correctness. Each process is considered as separate and the proof outline is proved to hold separately at first. In the second stage, the assertions in process P j are proved not being falsified by statements in P i for all j 6= i; i.e..