并行程序与状态序列——交叉语义约定的研究

Parallel Programs and State Sequences——A Study of Interleaving Convention

许多程序模型是以数学或逻辑为基础设计并分析的,但程序模型的实现首先是个物理系统,它依物理规律,而非数学或逻辑规则活动。但人们习惯于用状态序列对并列程序模型的语义作数学处理。一旦偏序的状态空间用交叉的方法全序化,并用于论证程序性质,误导就在所难免。所谓误导,指的是与实际运行的偏差,借助于Petri网,可以将它们暴露出来。其实偏差的出现与Petri网的基本现象冲突(conflict)、冲撞(contact)、并发(concurrency)和混惑(confusion)相关。本文用Petri网分析误导的情况。

A program system is, in the first place, a physical system, which behaves in accordance with physical laws. But it is a common convention for parallel programming models to rely on state sequences in their mathematical semantic treatment. When a partially ordered state space is fully ordered by interleaving, misleading results may emerge in program property argumentation. Possible misleading results, i.e. deviations from real execution, can be revealed with the help of Petri Nets. These deviations are related to what is called conflict, contact, concurrency and confusion in Petri Nets. This paper analyzes such misleading situations in terms of Petri Nets.