Deadlock analysis of unbounded process networks

Naoki Kobayashi 1 Cosimo Laneve 2, 3
3 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Deadlock detection in concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give imprecise answers or do not scale. To enable the analysis of such programs, (1) we define an algorithm for detecting deadlocks of a basic model featuring recursion and fresh name generation: the lam programs, and (2) we design a type system for value-passing CCS that returns lam programs. We show the soundness of the type system, and develop a type inference algorithm for it. The resulting algorithm is able to check deadlock-freedom of programs that cannot be handled by previous analyses, such as those that build unbounded networks.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2017, 252, pp.48 - 70. 〈10.1016/j.ic.2016.03.004〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01643152
Contributeur : Laneve Cosimo <>
Soumis le : mardi 21 novembre 2017 - 10:32:37
Dernière modification le : mercredi 10 octobre 2018 - 10:10:14

Lien texte intégral

Identifiants

Collections

Citation

Naoki Kobayashi, Cosimo Laneve. Deadlock analysis of unbounded process networks. Information and Computation, Elsevier, 2017, 252, pp.48 - 70. 〈10.1016/j.ic.2016.03.004〉. 〈hal-01643152〉

Partager

Métriques

Consultations de la notice

81