Abstract
We present a novel deadlock analysis for concurrent objects based on the results inferred by a points-to analysis and a may-happen-in-parallel (MHP) analysis. Similarly to other analysis, we build a dependency graph such that the absence of cycles in the graph ensures deadlock freeness. An MHP analysis provides an over-approximation of the pairs of program points that may be running in parallel. The crux of the method is that the analysis integrates the MHP information within the dependency graph in order to discard unfeasible cycles that otherwise would lead to false positives. We argue that our analysis is more precise and/or efficient than previous proposals for deadlock analysis of concurrent objects. As regards accuracy, we are able to handle cases that other analyses have pointed out as challenges. As regards efficiency, the complexity of our deadlock analysis is polynomial.
This work was funded in part by the Information & Communication Technologies program of the European Commission, Future and Emerging Technologies (FET), under the ICT-231620 HATS project, and by the Spanish projects TIN2008-05624, TIN2012-38137, PRI-AIBDE-2011-0900 and S2009TIC-1465 PROMETIDOS-CM.
Chapter PDF
Similar content being viewed by others
References
Agha, G.A.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)
Albert, E., Flores-Montoya, A.E., Genaim, S.: Analysis of May-Happen-in-Parallel in Concurrent Objects. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 35–51. Springer, Heidelberg (2012)
Armstrong, J., Virding, R., Wistrom, C., Williams, M.: Concurrent Programming in Erlang. Prentice Hall (1996)
de Boer, F.S., 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)
de Boer, F.S., Grabe, I., Steffen, M.: Termination detection for active objects. J. Log. Algebr. Program. 81(4), 541–557 (2012)
de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007)
Giachino, E., Grazia, C.A., Laneve, C., Lienhardt, M., Wong, P.: Deadlock Analysis of Concurrent Objects – Theory and Practice (2013)
Giachino, E., Laneve, C.: Analysis of Deadlocks in Object Groups. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 168–182. Springer, Heidelberg (2011)
Haller, P., Odersky, M.: Scala actors: Unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2-3), 202–220 (2009)
Holt, R.C.: Some Deadlock Properties of Computer Systems. ACM Comput. Surv. 4(3), 179–196 (1972)
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 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011)
Masticola, S.P., Ryder, B.G.: A Model of Ada Programs for Static Deadlock Detection in Polynomial Time. In: Parallel and Distributed Debugging, pp. 97–107. ACM (1991)
Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for java. ACM Trans. Softw. Eng. Methodol. 14, 1–41 (2005)
Naik, M., Park, C., Sen, K., Gay, D.: Effective static deadlock detection. In: Proc. of ICSE, pp. 386–396. IEEE (2009)
Smaragdakis, Y., Bravenboer, M., Lhoták, O.: Pick your contexts well: understanding object-sensitivity. In: POPL, pp. 17–30. ACM (2011)
Steensgaard, B.: Points-to analysis in almost linear time. In: Symposium on Principles of Programming Languages, pp. 32–41 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Flores-Montoya, A.E., Albert, E., Genaim, S. (2013). May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects. In: Beyer, D., Boreale, M. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2013 2013. Lecture Notes in Computer Science, vol 7892. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38592-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-38592-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38591-9
Online ISBN: 978-3-642-38592-6
eBook Packages: Computer ScienceComputer Science (R0)