Numerous edge-chasing deadlock detection algonthms were developed lor the cycle detection in distributed systems, but their detections had the n steps speed limitation and n （ n- 1） overhead limitation to detect a c...Numerous edge-chasing deadlock detection algonthms were developed lor the cycle detection in distributed systems, but their detections had the n steps speed limitation and n （ n- 1） overhead limitation to detect a cycle of size n under the one-resource request model. Since fast deadlock detection is critical, this paper proposed a new algorithm to speed up the detection process. In our algorithm, when the running of a transaction node is blocked, the being requested resource nodes reply it with the waiting or being waited message simultaneously, so the blocked node knows both its predecessors and successors, which helps it detecting a cycle of size 2 directly and locally. For the cycle of size n （ n 〉 2）, a special probe is produced which has the predecessors information of its originator, so the being detected nodes know their indirect predecessors and direct successors, and can detect the cycle within n - 2 steps. The proposed algorithm is formally proved to be correct by the invariant verification method. Performance evaluation shows that the message overhead of our detection is （ n^2 - n - 2）/2, hence both the detection speed and message cost of the proposed algorithm are better than that of the existing al gorithms.展开更多
Presents a method for deadlock avoidance algorithm used in Flexible Manufacturing System(FMS). This method is an improvement of the Banker algorithm. The Banker algorithm is commonly used in the Operating System (OS),...Presents a method for deadlock avoidance algorithm used in Flexible Manufacturing System(FMS). This method is an improvement of the Banker algorithm. The Banker algorithm is commonly used in the Operating System (OS), but some improvements will have to be made on the algorithm if this algorithm is used in FMS. The difference between the process in operating system and the job in the FMS is fully discussed. Based on this difference, the improvement is made. In order to improve the algorithm, formal methods are adopted to the manufacturing systems. The simulation model is translated into a format suitable for model checking. That is, the model is written into PROMELA, the input language of the popular model checker SPIN. After that, SPIN is used to verify that the model does not have deadlock. This algorithm proves to be highly effective in practice.展开更多
文摘Numerous edge-chasing deadlock detection algonthms were developed lor the cycle detection in distributed systems, but their detections had the n steps speed limitation and n （ n- 1） overhead limitation to detect a cycle of size n under the one-resource request model. Since fast deadlock detection is critical, this paper proposed a new algorithm to speed up the detection process. In our algorithm, when the running of a transaction node is blocked, the being requested resource nodes reply it with the waiting or being waited message simultaneously, so the blocked node knows both its predecessors and successors, which helps it detecting a cycle of size 2 directly and locally. For the cycle of size n （ n 〉 2）, a special probe is produced which has the predecessors information of its originator, so the being detected nodes know their indirect predecessors and direct successors, and can detect the cycle within n - 2 steps. The proposed algorithm is formally proved to be correct by the invariant verification method. Performance evaluation shows that the message overhead of our detection is （ n^2 - n - 2）/2, hence both the detection speed and message cost of the proposed algorithm are better than that of the existing al gorithms.
文摘Presents a method for deadlock avoidance algorithm used in Flexible Manufacturing System(FMS). This method is an improvement of the Banker algorithm. The Banker algorithm is commonly used in the Operating System (OS), but some improvements will have to be made on the algorithm if this algorithm is used in FMS. The difference between the process in operating system and the job in the FMS is fully discussed. Based on this difference, the improvement is made. In order to improve the algorithm, formal methods are adopted to the manufacturing systems. The simulation model is translated into a format suitable for model checking. That is, the model is written into PROMELA, the input language of the popular model checker SPIN. After that, SPIN is used to verify that the model does not have deadlock. This algorithm proves to be highly effective in practice.
