×

zbMATH — the first resource for mathematics

Deadlock analysis of unbounded process networks. (English) Zbl 1355.68193
Summary: 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.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
TyPiCal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Boyapati, C.; Lee, R.; Rinard, M., Ownership types for safe program: preventing data races and deadlocks, (OOPSLA, (2002), ACM), 211-230
[2] Flanagan, C.; Qadeer, S., A type and effect system for atomicity, (PLDI, (2003), ACM), 338-349
[3] Abadi, M.; Flanagan, C.; Freund, S. N., Types for safe locking: static race detection for Java, ACM Trans. Program. Lang. Syst., 28, 207-255, (2006)
[4] Kobayashi, N., A new type system for deadlock-free processes, (CONCUR, LNCS, vol. 4137, (2006), Springer), 233-247 · Zbl 1151.68537
[5] Suenaga, K., Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references, (APLAS, LNCS, vol. 5356, (2008), Springer), 155-170
[6] Vasconcelos, V. T.; Martins, F.; Cogumbreiro, T., Type inference for deadlock detection in a multithreaded polymorphic typed assembly language, (PLACES, EPTCS, vol. 17, (2009)), 95-109
[7] Milner, R., A calculus of communicating systems, LNCS, vol. 92, (1980), Springer · Zbl 0452.68027
[8] Kobayashi, N., : type-based static analyzer for the pi-calculus, (2007), at
[9] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, II, Inf. Comput., 100, 41-77, (1992) · Zbl 0752.68037
[10] Padovani, L., Deadlock and lock freedom in the linear π-calculus, (CSL-LICS’14, (2014), ACM), 72:1-72:10 · Zbl 1392.68311
[11] Giachino, E.; Laneve, C., A Beginner’s guide to the deadlock analysis model, (TGC’2012, LNCS, vol. 8191, (2013), Springer-Verlag), 49-63
[12] Giachino, E.; Laneve, C., Deadlock detection in linear recursive programs, (Proceedings of SFM-14:ESM, LNCS, vol. 8483, (2014), Springer-Verlag), 26-64 · Zbl 1445.68052
[13] Giachino, E.; Kobayashi, N.; Laneve, C., Deadlock analysis of unbounded process networks, (25th International Conference on Concurrency Theory, CONCUR 2014, Lecture Notes in Computer Science, vol. 8704, (2014), Springer), 63-77 · Zbl 1417.68128
[14] Davey, B. A.; Priestley, H. A., Introduction to lattices and order, (2002), Cambridge University Press · Zbl 1002.06001
[15] Kobayashi, N., A partially deadlock-free typed process calculus, ACM Trans. Program. Lang. Syst., 20, 2, 436-482, (1998)
[16] Kobayashi, N., Type systems for concurrent programs, (10th Anniversary Colloquium of UNU/IIST, LNCS, vol. 2757, (2003), Springer), 439-453 · Zbl 1274.68076
[17] Kobayashi, N., Type-based information flow analysis for the pi-calculus, Acta Inform., 42, 4-5, 291-347, (2005) · Zbl 1081.68061
[18] Kobayashi, N.; Pierce, B. C.; Turner, D. N., Linearity and the pi-calculus, ACM Trans. Program. Lang. Syst., 21, 5, 914-947, (1999)
[19] Kobayashi, N., A type system for lock-free processes, Inf. Comput., 177, 122-159, (2002) · Zbl 1093.68065
[20] Henglein, F., Type inference with polymorphic recursion, ACM Trans. Program. Lang. Syst., 15, 2, 253-289, (1993)
[21] Giachino, E.; Laneve, C.; Lienhardt, M., A framework for deadlock detection in ABS, Softw. Syst. Model., (2015), in press
[22] Caires, L.; Vieira, H. T., Conversation types, Theor. Comput. Sci., 411, 51-52, 4399-4440, (2010) · Zbl 1207.68222
[23] Pun, K. I.; Steffen, M.; Stolz, V., Deadlock checking by data race detection, J. Log. Algebraic Methods Program., 83, 5-6, 400-426, (2014) · Zbl 1371.68199
[24] L. Padovani, Personal communication, 2014.
[25] Kobayashi, N.; Sangiorgi, D., A hybrid type system for lock-freedom of mobile processes, ACM Trans. Program. Lang. Syst., 32, 5, (2010)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.