Abstract
We present a constraint-based effect inference algorithm for deadlock checking. The static analysis is developed for a concurrent calculus with higherorder functions and dynamic lock creation. The analysis is context-sensitive and locks are summarised based on their creation-site. The resulting effects can be checked for deadlocks using state space exploration. We use a specific deadlocksensitive simulation relation to show that the effects soundly over-approximate the behaviour of a program, in particular that deadlocks in the program are preserved in the effects.
Partly funded by the EU projects FP7-610582 (Envisage) and FP7-612985 (UpScale).
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
Agarwal, R., Wang, L., Stoller, S.D.: Detecting potential deadlocks with static analysis and run-time monitoring. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) Haifa Verification Conf. 2005. LNCS, vol. 3875, pp. 191–207. Springer, Heidelberg (2006)
Amtoft, T., Nielson, H.R., Nielson, F.: Type and Effect Systems: Behaviours for Concurrency. Imperial College Press (1999)
Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA 2002, Seattle, USA. ACM (2002); SIGPLAN Notices
Coffman Jr., E.G., Elphick, M., Shoshani, A.: System deadlocks. Computing Surveys 3(2) (1971)
Damas, L.: Type Assignment in Programming Languages. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, CST-33-85 (1985)
Damas, L., Milner, R.: Principal type-schemes for functional programming languages. In: Ninth POPL, Albuquerque, NM. ACM (1982)
Dijkstra, E.W.: Cooperating sequential processes. Technical Report EWD-123, TU Eindhoven (1965)
Hindley, J.R.: The principal type-scheme of an object in combinatory logic. Transactions of the AMS 146 (1969)
Kidd, N., Reps, T.W., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. STTT 13(6) (2011)
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)
Mossin, C.: Flow Analysis of Typed Higher-Order Programs. PhD thesis, DIKU, University of Copenhagen, Denmark. Technical Report DIKU-TR-97/1 (1997)
Naik, M., Park, C.-S., Sen, K., Gay, D.: Effective static deadlock detection. In: 31st International Conference on Software Engineering (ICSE 2009). IEEE (2009)
Pun, K.I., Steffen, M., Stolz, V.: Deadlock checking by a behavioral effect system for lock handling. J. of Logic and Algebraic Programming 81(3) (2012)
Pun, K.I., Steffen, M., Stolz, V.: Lock-polymorphic behaviour inference for deadlock checking. Tech. report 436, UiO, IFI (2013) (submitted for Journal Publication)
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)
Talpin, J.-P., Jouvelot, P.: Polymorphic Type, Region and Effect Inference. J. of Functional Programming 2(3) (1992)
Vasconcelos, V., Martins, F., Cogumbreiro, T.: Type inference for deadlock detection in a multithreaded polymorphic typed assembly language. In: PLACES 2009. EPTCS, vol. 17 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Pun, K.I., Steffen, M., Stolz, V. (2014). Effect-Polymorphic Behaviour Inference for Deadlock Checking. In: Giannakopoulou, D., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science, vol 8702. Springer, Cham. https://doi.org/10.1007/978-3-319-10431-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-10431-7_5
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10430-0
Online ISBN: 978-3-319-10431-7
eBook Packages: Computer ScienceComputer Science (R0)