问一个互斥问题

kukucm

peterson算法合适共享贮存的多处理机吗?

cnwalker

http://jcst.ict.ac.cn/conc/daodu046.htm

似乎应该可以



本文提出了一种分离前提方法（split precondition approach），用它来构造分布式算法模型并证明算法的正确性。文中讨论了Peterson的双处理器分布式互斥算法，对其进行了精确的分析和形式化的说明。并给出了相关属性的证明。
    在分布式算法的研究中，人们主要关注的问题是分布式算法的正确执行，而不是并行处理的交叉顺序。我们可以通过恰当地构造分布式算法的模型，进而全面深入地分析分布式算法的各种属性来研究这个问题。这种分析可以是静态的，也可以是动态的。动态分析方法要依靠数量有限的测试性运行来观察分布式算法的行为。然而，由于此类方法无法考虑所有的执行情况，所以，它们并不可靠。为此，我们提出了这种称作分离前提方法的静态分析方法，并说明了怎样使用这种方法来研究一类通过共享变量来处理通信的分布式算法。这种方法不仅简单易行，而且准确性很高。不过，采用这种方法进行分析需要投入细致的人力工作。因为，在分离前提逻辑中，正确性是通过证明断言来保证的，断言在谓词逻辑中通常用公式表示。这些公式必需在系统的设计阶段嵌入到系统之中，其证明需要采用标准的谓词逻辑规则以及所论及系统的转移规则。由于我们是通过系统的转移规则来说明系统的，所以上述规则对我们来说不难得到。这样，开发一个基于规则的系统来评估断言的正确性就成为可能了。甚至可以考虑建立一个足够智能化的系统来进行人机协商，进而更新系统的规则库。
    我们的分离前提方法采用了简便的一阶谓词逻辑。我们将公式写出来，然后从逻辑上对其加以证明。本文证明了分离前提逻辑可以用作对分布式算法进行构模并证明其有效性的形式化手段。作为这种方法的优良性能的证明，我们以Peterson双处理器并行算法作为案例进行了分析。我们形式化地证明了它的安全属性、生命属性、死锁—自由属性等属性。在推理过程中，我们使用分离前提逻辑进行回溯推理，得出了某些状态不可能达到的结论。回溯推理能够有效地缩小搜索空间 ，因此，它是一种更加优越的面向目标的方法。
    就分布式算法的分析而言，分离前提算法有两点实质性的贡献。第一，它提供了一种优雅而严格的符号来描述分布式算法。第二，它为分布式算法正确性的系统分析提供了一个框架。
    本文不只是单纯论述一种已知算法的重新表示，还旨在证明分离前提逻辑既适用于分布式算法的构模，也适用于分布式算法的推理。我们期望这种方法能够大量地应用到其它分布式算法的分析中去。