• Efficiently verifiable conditi...

Result: Efficiently verifiable conditions for deadlock-freedom of large concurrent programs

Title:
Efficiently verifiable conditions for deadlock-freedom of large concurrent programs
Authors:
ATTIE, Paul C, CHOCKLER, Hana
Source:
VMCAI 2005 : verification, model checking, and abstract interpretation (Paris, 17-19 January 2005)Lecture notes in computer science. :465-481
Publisher Information:
Berlin: Springer, 2005.
Publication Year:
2005
Physical Description:
print, 28 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Logiciel, Software, Génie logiciel, Software engineering, Allocation ressource, Resource allocation, Asignación recurso, Approche probabiliste, Probabilistic approach, Enfoque probabilista, Complexité algorithme, Algorithm complexity, Complejidad algoritmo, Démonstration automatique, Automatic proving, Demostración automática, File attente, Queue, Fila espera, Interblocage, Deadlock, Interbloqueo, Machine état fini, Finite state machine, Máquina estado finito, Mémoire partagée, Shared memory, Memoria compartida, Méthode polynomiale, Polynomial method, Método polinomial, Non déterminisme, Non determinism, No determinismo, Priorité, Priority, Prioridad, Problème NP difficile, NP hard problem, Problema NP duro, Programme concurrent, Concurrent program, Programa competidor, Simultanéité informatique, Concurrency, Simultaneidad informatica, Temps polynomial, Polynomial time, Tiempo polinomial, Vérification programme, Program verification, Verificación programa
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
College of Computer and Information Science, Northeastern University, 360 Huntington Avenue, Boston, MA 02115, United States
MIT CSAIL, 32 Vassar Street, Cambridge, MA 02139, United States
Department of Computer Science, WPI, 100, Institute Road, Worcester, MA 01609, United States
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=16546768
Rights:
Copyright 2005 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.16546768
Database:
PASCAL Archive

Further Information

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.