关于Peterson—Fischer二进程算法的断言式证明

AN ASSERTIONAL PROOF FOR PETERSON-FISCHER 2-MUTUAL ALGORITHM

本文旨在为Peterson—Fischer二进程互斥算法提供一个断言式证明,根据麻省理工学院Nancy A.Lynch教授的论述,这是一个未解决的问题,因此本文的意义在于填补这一空缺。

This paper purports to present an assertional proof for Peterson-Fischer 2-mutual exclusion algorithm. According to Nancy A. Lynch of MIT[1], this was an open problem. Hence the significance of this paper is to fill the gap.