zbMATH — the first resource for mathematics

The pursuit of deadlock freedom. (English) Zbl 0626.68019
We introduce some combinatorial techniques for establishing the deadlock freedom of concurrent systems which are similar to the variant/invariant method of proving loop termination. Our methods are based on the local analysis of networks, which is combinatorially far easier than analysing all global states. They are illustrated by proving numerous examples to be free of deadlock, some of which are useful classes of network.

68N25 Theory of operating systems
Full Text: DOI
[1] Apt, K.R.; Francez, N.; De Roever, W.P., A proof system for communicating sequential processes, ACM toplas, 2, 3, 359-385, (July 1980)
[2] Brookes, S.D.; Hoare, C.A.R.; Roscoe, A.W., A theory of communicating sequential processes, J. assoc. comput. math., 31, 3, 560-599, (1984) · Zbl 0628.68025
[3] Brookes, S.D.; Roscoe, A.W., An improved failures model for communicating processes, (), 281-305 · Zbl 0565.68023
[4] Brookes, S.D.; Roscoe, A.W., Deadlock analysis in networks of communicating processes, (), 305-324 · Zbl 0578.68024
[5] \scBrookes, S. D., and Roscoe, A. W. Deadlock analysis in networks of communicating processes II, in press.
[6] Chandy, K.M.; Misra, J., Deadlock absence proofs for networks of communicating processes, Inform. process. lett., 9, 4, (1974) · Zbl 0456.68030
[7] Dijkstra, E.W.; Scholten, C.S., A class of simple communication patterns, ()
[8] Hoare, C.A.R., ()
[9] Owicki, S.S.; Gries, D., Verifying properties of parallel programs: an axiomatic approach, Commun. assoc. comput. Mach., 19, 5, 279-285, (1976) · Zbl 0322.68010
[10] Sifakis, J., Deadlocks and livelocks in transition systems, (), 587-599 · Zbl 0454.68050
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.