基于Petri网的点到点通信并行程序验证

Verification of Parallel Programs of Point-To-Point Communication Based on Petri Net

基于消息传递的编程模式是目前编写高性能应用程序的主流,而点到点通信函数是最基本的函数。基于点到点通信函数的特点,使用Petri网模拟它们的执行过程,利用控制库所充分展示了各种点到点通信函数之间的区别。然后给出对基于点到点通信的并行程序进行建模和验证的过程,并举例说明了这个方法的有效性。

It is the message-passing mode that is the mainstream implementing high-performance applications, and point-to-point communication procedures are the basic. The differences between all kinds of point-to-point communication are illustrated with control places in simulating the peformance of the procedures by Petri net based on their characteristics. Furthermore, the steps to model and verify a program based on point-to-point communication are presented, and an example is provided to validate the method.