Efficiently verifiable conditions for deadlock-freedom of large concurrent programs

Paul C. Attie, Hana Chockler

Research output: Contribution to journalConference article

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

Fingerprint

Deadlock
Concurrent
Polynomials
Automatic Verification
Priority Queue
Polynomial
Sufficient Conditions
Syntactics
Shared Memory
Resource Allocation
Polynomial-time Algorithm
Resource allocation
NP-complete problem
Choose
Data storage equipment
Graph in graph theory

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. / Attie, Paul C.; Chockler, Hana.

In: Lecture Notes in Computer Science, Vol. 3385, 09.09.2005, p. 465-481.

Research output: Contribution to journalConference article

@article{7ff6cfbd05d74002970879dbcbaa9250,
title = "Efficiently verifiable conditions for deadlock-freedom of large concurrent programs",
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.",
author = "Attie, {Paul C.} and Hana Chockler",
year = "2005",
month = "9",
day = "9",
language = "English (US)",
volume = "3385",
pages = "465--481",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Efficiently verifiable conditions for deadlock-freedom of large concurrent programs

AU - Attie, Paul C.

AU - Chockler, Hana

PY - 2005/9/9

Y1 - 2005/9/9

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=24144495514&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=24144495514&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:24144495514

VL - 3385

SP - 465

EP - 481

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -