进程创建的语义及等价性

Semantics for Process Creation and Their Equivalence

针对一个基于共享变量的带有进程创建的命令式语言 ,用变迁系统描述了它的结构操作语义 ,并用扩展的状态变迁迹模型定义了它的指称语义 .在该模型下 ,状态变迁被区分为两种不同形式 ,分别表示发生在原进程和被创建进程中的状态变迁 ,这样便可以定义适当的语义复合运算 ,在对命令的指称进行复合时根据变迁类型的不同对变迁迹进行串行或交错连接 ,恰当地反映了进程的并发运行受到创建命令在程序中的相对位置的限制 .

A shared variable language with process creation is defined in this paper.Its structural operational semantics is described using transition systems and its denotational semantics is defined with an extension of transition trace model.Extended state transitions can differentiate transitions occurring in a created process from those occurring in the original process.Based on this extension, some semantic composition operators can be defined to sequentially compose or interleave the transition traces of respective commands according to the types of the extended state transitions occurring in them,which illustrates that the execution of the concurrent processes are limited by their creation spots in the program.The equivalence of the two semantics is proved at the end.