The Pursuit of Deadlock Freedom

Abstract

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 combinationally far easier than analysing all global states. They arc illustrated by proving numerous examples to be free of deadlock, some which are useful classes of network.