Abstract
This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permissionaccounting separation logic. As usual, each lock is associated with a resource invariant, i.e., when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parameterized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ábrahám, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Tool-supported proof system for multithreaded Java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 1–32. Springer, Heidelberg (2003)
Andrews, G.: Concurrent Programming: Principles and Practice. Benjamin/Cummings (1991)
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6) (2004)
Bornat, R., O’Hearn, P.W., Calcagno, C., Parkinson, M.: Permission accounting in separation logic. In: Principles of Programming Languages. ACM Press, New York (2005)
Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (2002)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, Springer, Heidelberg (2003)
Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM SIGPLAN Notices, vol. 33(10). ACM Press, New York (1998)
de Boer, F.S.: A sound and complete shared-variable concurrency model for multi-threaded Java programs. In: International Conference on Formal Methods for Open Object-based Distributed Systems (2007)
DeLine, R., Fähndrich, M.: Typestates for objects. In: European Conference on Object-Oriented Programming (2004)
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Asian Programming Languages and Systems Symposium (2007)
Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java’s reentrant locks. Technical Report ICIS-R08014, Radboud University Nijmegen (2008)
Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork/join. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 199–215. Springer, Heidelberg (2008)
Hobor, A., Appel, A., Nardelli, F.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353–367. Springer, Heidelberg (2008)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages (2001)
Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: International Conference on Formal Engineering Methods (2006)
Müller, P. (ed.): Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262, p. 195. Springer, Heidelberg (2002)
Naftalin, M., Wadler, P.: Java Generics. O’Reilly, Sebastopol (2006)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1–3), 271–307 (2007)
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2) (1999)
Parkinson, M.: Local Reasoning for Java. Ph.D thesis, University of Cambridge (2005)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Principles of Programming Languages (2005)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark. IEEE Press, Los Alamitos (2002)
Wadler, P.: A taste of linear logic. In: Mathematical Foundations of Computer Science (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haack, C., Huisman, M., Hurlin, C. (2008). Reasoning about Java’s Reentrant Locks. In: Ramalingam, G. (eds) Programming Languages and Systems. APLAS 2008. Lecture Notes in Computer Science, vol 5356. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89330-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-89330-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89329-5
Online ISBN: 978-3-540-89330-1
eBook Packages: Computer ScienceComputer Science (R0)