Abstract
In recent work, Flanagan and Qadeer proposed atomicity declarations as a light-weight mechanism for specifying non-interference properties in concurrent programming languages such as Java, and they provided a type and effect system to verify atomicity properties. While verification of atomicity specifications via a static type system has several advantages (scalability, compositional checking), we show that verification via model-checking also has several advantages (fewer unchecked annotations, greater coverage of Java idioms, stronger verification). In particular, we show that by adapting the Bogor model-checker, we naturally address several properties that are difficult to check with a static type system.
This work was supported in part by the U.S. Army Research Office (DAAD190110564), by DARPA/IXO’s PCES program (AFRL Contract F33615-00-C-3044), by NSF (CCR-0306607) by Lockheed Martin, and by Intel Corporation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Rajamani, S.: Bebop: a symbolic model-checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)
Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder – a second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: ICSE (2000)
Dwyer, M.B., Hatcliff, J., Ranganath, V., Robby: Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Technical Report TR2003-1, SAnToS Laboratory, Kansas State University (2003)
Dwyer, M.B., Wallentine, V.: A framework for parallel adaptive grid simulations. Concurrency: Practice and Experience 9(11), 1293–1310 (1997)
Flanagan, C., Freund, S.N.: Type-based race detection for Java. In: PLDI (2000)
Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. In: Proceedings of POPL (2003) (to appear)
Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for sharedmemory programs. In: ESOP (2000)
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI (2003)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall International, Englewood Cliffs (1991)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–294 (1997)
Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Communications of the ACM 18(12) (1975)
Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)
Bogor Website (2003), http://bogor.projects.cis.ksu.edu
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems 15(4), 391–411 (1997)
Stoller, S.: Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer, Springer (2002)
Stoller, S., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 489–504. Springer, Heidelberg (2003)
Wang, L., Stoller, S.D.: Run-time analysis for atomicity. In: Proceedings of the Workshop on Runtime Verification. ENTCS, vol. 89.2 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hatcliff, J., Robby, Dwyer, M.B. (2004). Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. In: Steffen, B., Levi, G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2004. Lecture Notes in Computer Science, vol 2937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24622-0_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-24622-0_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20803-7
Online ISBN: 978-3-540-24622-0
eBook Packages: Springer Book Archive