Deadlock Analysis of Unbounded Process Networks

Elena Giachino 1, 2 Naoki Kobayashi 3 Cosimo Laneve 1, 2
1 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 im-precise 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. As a byproduct of these two tech-niques, we have an algorithm that is more powerful than previous ones and that can be easily integrated in the current release of TyPiCal, a type-based analyser for pi-calculus.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01091749
Contributor : Laneve Cosimo <>
Submitted on : Saturday, December 6, 2014 - 9:18:14 AM
Last modification on : Saturday, January 27, 2018 - 1:30:54 AM
Long-term archiving on : Monday, March 9, 2015 - 6:06:58 AM

File

mfd.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Elena Giachino, Naoki Kobayashi, Cosimo Laneve. Deadlock Analysis of Unbounded Process Networks. CONCUR 2014 - Concurrency Theory - 25th International Conference, Sep 2014, Rome, Italy. pp.63 - 77, ⟨10.1007/978-3-662-44584-6_6⟩. ⟨hal-01091749⟩

Share

Metrics

Record views

179

Files downloads

204