mdw*_*326 5 concurrency multithreading process promela
我对这个词的含义不太确定。我在我们学习并发的课程中看到了它。我已经看到了许多有关数据交织的定义,但是我可以找到有关进程交织的任何信息。
当我直觉告诉我这是使用线程同时运行多个进程时,是正确的吗?
如果你把一个过程想象成一个(可能是无限的)语句序列/痕迹(例如通过循环展开获得),那么几个过程的可能交错集合由这些过程中的任何一个的所有可能的语句序列组成。
例如,考虑流程
int i;
proctype A() {
i = 1;
}
proctype B() {
i = 2;
}
Run Code Online (Sandbox Code Playgroud)
那么可能的交错是i = 1; i = 2and i = 2; i = 1,即可能的最终值i是 1 和 2。这当然可能更复杂,例如在存在受保护语句的情况下:那么交错序列中的下一个可能语句不一定是那些在下一个程序计数器的位置,但仅限于守卫允许的位置;考虑例如 proctype
proctype B() {
if
:: i == 0 -> i = 2
:: else -> skip
fi
}
Run Code Online (Sandbox Code Playgroud)
那么可能的交错(A()如前所述)是i = 1; skip和i = 2; i = 1,因此 的最终值只有一个i。
实际上,交错的概念对于 Spin 的并发性观点至关重要。在跟踪语义中,并发进程的可能跟踪集是单个进程的跟踪的可能交错集。
它只是意味着以任意顺序执行(数据访问或执行或...)**(请参阅注释)。在并发的情况下,通常指的是动作交错。如果进程 P 和 Q 是并行组合 (P||Q),那么它们的动作将交错。考虑以下流程:
PLAYING = (play_music -> stop_music -> STOP).
PERFORMING = (dance -> STOP).
||PLAY_PERFORM = (PLAYING || PERFORMING).
Run Code Online (Sandbox Code Playgroud)
因此每个原始过程可以表示为:(由LTSA模型检查工具生成)


那么动作交错的可能结果将是:
dance -> play_music -> stop_music
play_music -> dance -> stop_music
play_music -> stop_music -> dance
Run Code Online (Sandbox Code Playgroud)
**注意:这里的“任意”是指任意选择进程执行而不是其内部代码序列。每个进程中的代码执行将始终按顺序执行。
如果您仍然不满意,可以看一下:https://www.doc.ic.ac.uk/~jnm/book/firstbook/pdf/ch3.pdf
希望能帮助到你!:)