multithreading - 如何有效地表示或建模锁定序列？

Question

我目前正在解决的问题需要使用两个或多个锁(本例中为文件锁)来避免并发问题。

但是，我无法表示我将用于解决方案的(锁定)模型。

即我想解释这个问题和我正在通过某种类型的图表编码的解决方案，这些图表可以让我显示锁定顺序、并发影响(例如，如果我们在此之前释放此锁，我们将遇到此问题等)和其他此类问题有用的信息。

表示锁模型的好方法是什么？

一方面，我一直在尝试使用流程图来做到这一点，这样我就可以展示导致我必须获取锁或不获取锁的代码流(例如，我使用独占非阻塞锁来确定是否一个进程已经在监视一个文件，如果没有，我启动监视器)，另一方面，我一直认为序列图就可以了，但我对结果不满意。

还有其他可用的可视化工具可以让我代表这个问题吗？

对于分布式系统等非常复杂的问题，工程师如何解决这个问题？

是否有任何一个图表可以说明这一点，或者它更像是用于描述这一点的图表集合？

Answer 1

Petri nets历史上用于建模并发(和并发分布式系统)。作为一个正式的数学概念，它们允许您严格推理操作序列、状态可达性(例如可以方便地证明 Not Acceptable 锁配置和/或资源状态永远不会发生)、活跃性、有界性、死锁和其他此类有用信息。此外，它们具有漂亮、干净的视觉表现。但使用 Petri 网时，我们必须处理低级概念，例如位置和转换，并且没有抽象建模的方法。因此，即使对于中等大小的问题，它们的视觉描述通常也会变得很大。彩色、优先级、定时和其他增强 Petri 网有时会发挥作用，但对于更复杂的抽象系统 UML statecharts更适合。

以下是有关使用 Petri 网进行锁定序列分析的一些说明(有关更多详细信息，请参阅出版物):

1. 来自 "Petri netBased Model for Concurrent Control of Database System" by HOD Jie,LI Fengying and WANG Huijiao 的两阶段锁定策略的 Petri 网建模
2. 用于晶圆流动模式共享策略的 Petri 网模型 "Scheduling Single-Armed Cluster Tools With Reentrant Wafer Flows"by Hwan-Yong Lee and Tae-Eog Lee (这个包含一个详细的死锁分析)