证明某个分布式算法满足mutual exclusion/progress。这件事有没有一个通用的算法可以做呢?

不幸地,停机问题HALTTM可以归约到PROGRESS和MUTUAL EXCLUSION

  • HALTTM \(\leq_m\) PROGRESS

    设HALTTM中的算法为A,在A后面加上critical section构成A’。输出A’。

    若A不停机,则critical section永远不会被执行,不满足progress。

    若A停机,则critical section会被执行,满足progress。

  • HALTTM \(\leq_m\) MUTUAL EXCLUSION

    设HALTTM中的算法为A,在A后面加上critical section构成A’。输出A’。

    若A停机,则不妨假设两个进程在执行A后sleep然后在很短时间内分别先后醒来进入critical section(两个进程之间没有通信,互不影响),从而不满足mutual exclusion。

    若A不停机,则没有进程可以进入critical section,显然满足mutual exclusion。

所以PROGRESS和MUTUAL EXCLUSION都是undecidable,显然MUTUAL EXCLUSION也是undecidable。

还有最后一线希望,如果能证明PROGRESS AND MUTUAL EXCLUSION (PAME)是decidable也好。可是HALTTM也可以归约到PAME。

  • HALTTM \(\leq_m\) PAME

    设HALTTM中的算法为A,在A后面加上Dijkstra’s Mutual Exclusion Algorithm构成A’。输出A’。

    Dijkstra’s Mutual Exclusion Algorithm已经被证明满足mutual exclusion和progress。所以:

    若A停机,则A’仍然满足mutual exclusion和progress,故A’ \(\in\) PAME。

    若A不停机,则A’不满足progress,故A’ \(\notin\) PAME。

这下彻底没希望了。只能根据不同的分布式算法制定不同的策略了。