×

Deadlock detection in linear recursive programs. (English) Zbl 1445.68052

Bernardo, Marco (ed.) et al., Formal methods for executable software models. 14th international school on formal methods for the design of computer, communication, and software systems, SFM 2014, Bertinoro, Italy, June 16–20, 2014. Advanced lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8483, 26-64 (2014).
Summary: Deadlock detection in recursive programs that admit dynamic resource creation is extremely complex and solutions either give imprecise answers or do not scale.
We define an algorithm for detecting deadlocks of linear recursive programs of a basic model. The theory that underpins the algorithm is a generalization of the theory of permutations of names to so-called mutations, which transform tuples by introducing duplicates and fresh names.
Our algorithm realizes the back-end of deadlock analyzers for object-oriented programming languages, once the association programs/basic-model-programs has been defined as front-end.
For the entire collection see [Zbl 1305.68021].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

Software:

PIPER; ABS; TyPiCal
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: Static race detection for Java. TOPLAS 28 (2006)
[2] Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. In: POPL 2012, pp. 203–214. ACM (2012) · Zbl 1321.68184 · doi:10.1145/2103656.2103681
[3] Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe program.: preventing data races and deadlocks. In: OOPSLA, pp. 211–230. ACM (2002)
[4] Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31, 560–599 (1984) · Zbl 0628.68025 · doi:10.1145/828.833
[5] Carlsson, R., Millroth, H.: On cyclic process dependencies and the verification of absence of deadlocks in reactive systems (1997)
[6] Caromel, D., Henrio, L., Serpette, B.P.: Asynchronous and deterministic objects. In: POPL, pp. 123–134. ACM (2004) · Zbl 1325.68052 · doi:10.1145/964001.964012
[7] Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. SIGPLAN Not. 37(1), 45–57 (2002) · Zbl 1323.68365 · doi:10.1145/565816.503278
[8] Comtet, L.: Advanced Combinatorics: The Art of Finite and Infinite Expansions, Dordrecht, Netherlands (1974) · Zbl 0283.05001
[9] Requirement elicitation. Deliverable 5.1 of project FP7-231620 (HATS) (August 2009), http://www.hats-project.eu/sites/default/files/Deliverable51_rev2.pdf .
[10] Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338–349. ACM (2003) · doi:10.1145/781131.781169
[11] Flores-Montoya, A.E., Albert, E., Genaim, S.: May-happen-in-parallel based deadlock analysis for concurrent objects. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE 2013. LNCS, vol. 7892, pp. 273–288. Springer, Heidelberg (2013) · Zbl 06294488 · doi:10.1007/978-3-642-38592-6_19
[12] Gay, S.J., Nagarajan, R.: Types and typechecking for communicating quantum processes. MSCS 16(3), 375–406 (2006) · Zbl 1122.68059
[13] Giachino, E., Grazia, C.A., Laneve, C., Lienhardt, M., Wong, P.Y.H.: Deadlock analysis of concurrent objects: Theory and practice. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 394–411. Springer, Heidelberg (2013) · Zbl 06248480 · doi:10.1007/978-3-642-38613-8_27
[14] Giachino, E., Laneve, C., Lienhardt, M.: A Framework for Deadlock Detection in ABS (2013), http://www.cs.unibo.it/ laneve (submitted)
[15] Giachino, E., Laneve, C., Lienhardt, M.: Deadlock Framework for ABS (DF4ABS) - online interface (2013), http://www.cs.unibo.it/ giachino/siteDat/
[16] Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theor. Comput. Sci. 311(1-3), 121–163 (2004) · Zbl 1070.68105 · doi:10.1016/S0304-3975(03)00325-6
[17] Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011) · Zbl 06060083 · doi:10.1007/978-3-642-25271-6_8
[18] Kobayashi, N.: A partially deadlock-free typed process calculus. TOPLAS 20(2), 436–482 (1998) · doi:10.1145/276393.278524
[19] Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006) · Zbl 1151.68537 · doi:10.1007/11817949_16
[20] Kobayashi, N.: TyPiCal (2007), http://www.kb.ecei.tohoku.ac.jp/ koba/typical/
[21] Laneve, C., Padovani, L.: The must preorder revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212–225. Springer, Heidelberg (2007) · Zbl 1151.68319 · doi:10.1007/978-3-540-74407-8_15
[22] Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980) · Zbl 0452.68027 · doi:10.1007/3-540-10235-3
[23] Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, ii. Inf. and Comput. 100, 41–77 (1992) · Zbl 0752.68037 · doi:10.1016/0890-5401(92)90009-5
[24] Montanari, U., Pistore, M.: An introduction to history dependent automata. Electr. Notes Theor. Comput. Sci. 10, 170–188 (1997) · Zbl 0925.68289 · doi:10.1016/S1571-0661(05)80696-6
[25] Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol. 2136, pp. 560–572. Springer, Heidelberg (2001) · Zbl 0999.68110 · doi:10.1007/3-540-44683-4_49
[26] Nielson, H.R., Nielson, F.: Higher-order concurrent programs with finite communication topology. In: POPL, pp. 84–97. ACM (1994)
[27] Parastatidis, S., Webber, J.: MEP SSDL Protocol Framework (April 2005), http://ssdl.org
[28] Schrter, C., Esparza, J.: Reachability analysis using net unfoldings. In: CS&P 2000, pp. 255–270 (2000)
[29] Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41–57. Springer, Heidelberg (2006) · Zbl 1225.68103 · doi:10.1007/11874683_3
[30] Suenaga, K.: Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 155–170. Springer, Heidelberg (2008) · Zbl 05488152 · doi:10.1007/978-3-540-89330-1_12
[31] Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972) · Zbl 0251.05107 · doi:10.1137/0201010
[32] Vasconcelos, V.T., Martins, F., Cogumbreiro, T.: Type inference for deadlock detection in a multithreaded polymorphic typed assembly language. In: PLACES. EPTCS, vol. 17, pp. 95–109 (2009)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.