Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs

Hana Chockler, Paul C. Attie

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

20 Citations (Scopus)

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
Title of host publicationProceedings of Verification, Model Checking, and Abstract Interpretation, 6th International Conference (VMCAI)
PublisherSpringer
Pages465-481
Number of pages17
Publication statusPublished - 17 Jan 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume3385

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