Abstract
We present a framework for statically detecting deadlocks in a concurrent object language with asynchronous invocations and operations for getting values and releasing the control. Our approach is based on the integration of two static analysis techniques: (i) an inference algorithm to extract abstract descriptions of methods in the form of behavioral types, called contracts, and (ii) an evaluator that computes a fixpoint semantics returning a finite state model of contracts. A potential deadlock is detected when a circular dependency is found in some state of the model. We discuss the theory and the prototype implementation of our framework. Our tool is validated on an industrial case study based on the Fredhopper Access Server (FAS) developed by SDL Fredhoppper. In particular we verify one of the core concurrent components of FAS to be deadlock-free.
Partly funded by the EU project FP7-231620 HATS: Highly Adaptable and Trustworthy Software using Formal Models (http://www.hats-project.eu).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: Static race detection for Java. ACM Trans. Program. Lang. Syst. 28 (2006)
The ABS Language Specification, ABS version 1.2.0 edition (September 2012), http://tools.hats-project.eu/download/absrefmanual.pdf
Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe program.: preventing data races and deadlocks. In: Proc. OOPSLA 2002, pp. 211–230. ACM (2002)
Carlsson, R., Millroth, H.: On cyclic process dependencies and the verification of absence of deadlocks in reactive systems (1997)
Coppo, M.: Type inference with recursive type equations. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 184–198. Springer, Heidelberg (2001)
de Boer, F., Bravetti, M., Grabe, I., Lee, M., Steffen, M., Zavattaro, G.: A petri net based analysis of deadlocks for active objects and futures. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 110–127. Springer, Heidelberg (2013)
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: In PLDI 03: Programming Language Design and Implementation, pp. 338–349. ACM (2003)
Flores-Montoya, A.E., Albert, E., Genaim, S.: May-happen-in-parallel based deadlock analysis for concurrent objects. In: Beyer, D., Boteale, M. (eds.) FMOODS/FORTE 2013. LNCS, vol. 7892, pp. 273–288. Springer, Heidelberg (2013)
Giachino, E., Laneve, C.: Analysis of deadlocks in object groups. In: Bruni, R., Dingel, J. (eds.) FORTE/FMOODS 2011. LNCS, vol. 6722, pp. 168–182. Springer, Heidelberg (2011)
Giachino, E., Laneve, C.: A beginner’s guide to the deadLock Analysis Model. In: TGC, Springer, Heidelberg (2013)
Giachino, E., Lascu, T.A.: Lock Analysis for an Asynchronous Object Calculus. In: Proc. 13th ICTCS (2012)
Henglein, F.: Type inference with polymorphic recursion. ACM Trans. Program. Lang. Syst. 15(2), 253–289 (1993)
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.) FMCO 2011. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011)
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and System Modeling 6(1), 35–58 (2007)
Kerfoot, E., McKeever, S., Torshizi, F.: Deadlock freedom through object ownership. In: Wrigstad, T. (ed.) 5th International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO), in Conjunction with ECOOP 2009 (2009)
Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: The undecidability of the semi-unification problem. Inf. Comput. 102(1), 83–101 (1993)
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)
Puntigam, F., Peter, C.: Types for active objects with static deadlock prevention. Fundam. Inform. 48(4), 315–341 (2001)
Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing active objects to concurrent components. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 275–299. Springer, Heidelberg (2010)
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)
Suenaga, K., Kobayashi, N.: Type-based analysis of deadlock for a concurrent calculus with interrupts. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 490–504. Springer, Heidelberg (2007)
Vasconcelos, V.T., Martins, F., Cogumbreiro, T.: Type inference for deadlock detection in a multithreaded polymorphic typed assembly language. In: Proc. PLACES 2009. EPTCS, vol. 17, pp. 95–109 (2009)
West, S., Nanz, S., Meyer, B.: A modular scheme for deadlock prevention in an object-oriented programming model. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 597–612. Springer, Heidelberg (2010)
Wong, P.Y.H., Albert, E., Muschevici, R., Proença, J., Schäfer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. Journal on Software Tools for Technology Transfer 14(5), 567–588 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giachino, E., Grazia, C.A., Laneve, C., Lienhardt, M., Wong, P.Y.H. (2013). Deadlock Analysis of Concurrent Objects: Theory and Practice. In: Johnsen, E.B., Petre, L. (eds) Integrated Formal Methods. IFM 2013. Lecture Notes in Computer Science, vol 7940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38613-8_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-38613-8_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38612-1
Online ISBN: 978-3-642-38613-8
eBook Packages: Computer ScienceComputer Science (R0)