并行程序Petri网模型的结构性质.pdfVIP

计算机研究与发展 ISSN 1000．1239|CN 11—1777|TP Journal of Computer Research and Development 44(12)：2130～2135。2007 并行程序Petri网模型的结构性质 崔焕庆 吴哲辉 (山东科技大学信息科学与工程学院 青岛 266510) (smart0193@163．com) Structural Properties of Parallel Program’S Petri Net Model Cui Huanqing and Wu Zhehui (College of Information Science and Engineering，Shandong University of Science and Technology，Qingdao 266510) Abstract High—performance computing based on parallel programming is used in many fields，and correctness is the basis of parallel programs，but parallel programs are more difficult to verify than the sequential programs because of their complexity．Thus it is necessary to model them．Petri net is often used to model the parallel program，and most research work verifies the program from the point of view of Petri net．In this paper，the message—passing parallel program is transformed into Petri net model firstly，and the structural properties of it are studied on the program’S ground．It is proved that for a concurrent correct paral!el program’S model，its Petri net model is strongly connected and satisfies controlled siphon property， each of its process—subnets is conservative，and each of its transitions belongs to a support of T—invariant． Two examples，one is a simple point—to—point non—blocking communication and the other is a producer— consumer system，are given to show the applications of these properties in verification of the parallel program．These properties can be used in beforehand verification of the parallel program，and this method avoids state explosion caused by verification with dynamical properties．Thus it can improve the efficiency of program design and verification．This method can be generalized easily． Key words parallel program；Petri net；MPINet；structural property；verification 摘 要 正确性是并行程序的基础，但是由于它的复杂性，其验证要比串行程序困难得多，因此