Efficiently verifiable conditions for deadlock-freedom of large concurrent programs

Paul C. Attie, Hana Chockler

Research output: Contribution to journalConference article

19 Scopus citations

Abstract

We present two polynomial-time algorithms for automatic verification of deadlock-freedom of large finite-state concurrent programs. We consider shared-memory concurrent programs in which a process can nondeterministically choose amongst several (enabled) actions at any step. As shown in [23], deadlock-freedom analysis is NP-hard even for concurrent programs of restricted form (no nondeterministic choice). Therefore, research in this area concentrates either on the search for efficiently checkable sufficient conditions for deadlock-freedom, or on improving the complexity of the check in some special cases. In this paper, we present two efficiently checkable sufficient conditions for deadlock freedom. Our algorithms apply to programs which are expressed in a particular syntactic form, in which variables are shared between pairs of processes. The first algorithm improves the complexity of the deadlock check of Attie and Emerson [4] to polynomial in all parameters, as opposed to the exponential complexity of [4]. The second algorithm involves a conceptually new construction of a "global wait-for graph" for all processes. Its running time is also polynomial in all its parameters, and it is more discriminating than the first algorithm. We illustrate our algorithms by applying them to several examples of concurrent programs that implement resource allocation and priority queues. To the best of our knowledge, this is the first work that describes polynomially checkable conditions for assuring deadlock freedom of large concurrent programs.

Original languageEnglish (US)
Pages (from-to)465-481
Number of pages17
JournalLecture Notes in Computer Science
Volume3385
StatePublished - Sep 9 2005
Externally publishedYes
Event6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2005 - Paris, France
Duration: Jan 17 2005Jan 19 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Efficiently verifiable conditions for deadlock-freedom of large concurrent programs'. Together they form a unique fingerprint.

  • Cite this