状态及其变换

进程和消息

单个进程或线程（以下统称进程），是顺序执行单元。进程之间的通信方式有资源共享和消息传递。

资源共享方式（memory, file etc)需要同步机制（lock模型）来实现对资源的并发访问。

同步和异步

同步和异步的不同，关键在于对时间和并发的理解。异步意味着并发，任务完成时的通知机制。
对每个任务（task or job）, 其各自的生命周期，即状态变迁，也可以理解为不同的阶段（pipeline方式）。

并发和分布

从进程及进程间关系的角度来理解，并行和分布具有统一性。并行(parallel)主要是指节点内的并发(concurrency)，分布(distributed)则指跨越节点边界的并发。

Replication

共享资源需要冗余，来保障安全和提高效率。如果说自己与自己不需要考虑一致性的话，replication却是自己和自己的一致性1*N。世上没有完全相同的两片树叶。需要不同的一致性模型，来实现replication的俗世价值。

形式化模型技术

图论
Petri Net
自动机

引用

The high-performance computation based on parallel computing has been the third underpinning of the human being"s scientific study. High performance is the first reason to use parallel programs, and correctness is the chiefly condition to use it. However, the tools which were used to aid parallel programs design and analysis pay attentions only to one of the two aspects--high-performance or correctness.The author presents a prototype of a tool that provides both performance analysis and verification of the parallel programs from design running to analysis of results. Also, this thesis presents the principles and methods to design CAPSE tools founded on the traits of previous tools. We think the Petri net is superior over other models to model the MPI parallel programs by comparison.The parallel program based on message passing is the most popular paradigm now, and MPI has become the most popularly accepted standard of this pattern. This thesis studies the features of the MPI functions, and gives the Petri net models of them and C language in which they are nested, and presents the preliminary steps and method to model an MPI program. We present the concepts of statically executable and concurrently correct parallel program, and study the safeness strongly connectedness reachability reversibility and liveness of MPI parallel program"s model MPInet, and present some possible reasons to disobey these properties, for instance, lack-of-sending message orphan message non-match message deadlock (including inconsistency deadlock and circular deadlock) livelock and so on. At the same time, we present algorithms using the graph traversal and reachability graph/tree T-invariants to verify these properties and reasons.