Abstract
We study the type system introduced by Boyapati and Rinard in their paper “A Parameterized Type System for Race-Free Java Programs” and try to infer the type annotations (“lock types”) needed by their type checker to show that a program is free of race conditions. Boyapati and Rinard automatically generate some of these annotations using default types and static inference of lock types for local variables, but in practice, the programmer still needs to annotate on the order of 1 in every 25 lines of code. We use run-time techniques, based on the lockset algorithm, in conjunction with some static analysis to automatically infer most or all of the annotations.
This work was supported in part by NSF under Grant CCR-9876058 and ONR under Grants N00014-01-1-0109 and N00014-02-1-0363. Authors’ Email:{ragarwal,stoller}@cs.sunysb.edu Web: http://www.cs.sunysb.edu/~ragarwal http://www.cs.sunysb.edu/~stoller
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.
Similar content being viewed by others
References
Aldrich, J., Kostadinov, V., Chambers, C.: Alias annotations for program understanding. In: Proc. 17th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), ACM Press, New York (2002)
Agarwal, R., Stoller, S.D.: Type inference for parameterized racefree Java. Technical Report DAR 03–10, Computer Science Department, SUNY at Stony Brook (October 2003)
Boyapati, C., Rinard, M.C.: A parameterized type system for race-free Java programs. In: Proc. 16th ACM Conference on Object- Oriented Programming, Systems, Languages and Applications (OOPSLA). SIGPLAN Notices, vol. 36(11), pp. 56–69. ACM Press, New York (2001)
Cousot, P., Cousot, R.: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238–252 (1977)
Ernst, M.D.: Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington, Department of Computer Science and Engineering (2000)
Flanagan, C., Freund, S.: Type-based race detection for Java. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 219–232. ACM Press, New York (2000)
Flanagan, C., Freund, S.: Detecting race conditions in large programs. In: Workshop on Program Analysis for Software Tools and Engineering (PASTE), June 2001, pp. 90–96. ACM Press, New York (2001)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), ACM Press, New York (2002)
Grossman, D.: Type-safe multithreading in Cyclone. In: Proc. ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI), pp. 13–25. ACM Press, New York (2003)
Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 69–82. ACM Press, New York (2002)
Naik, M., Palsberg, J.: A type system equivalent to a model checker. Master’s thesis, Purdue University (2003)
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems 15(4), 391–411 (1997)
von Praun, C., Gross, T.R.: Object race detection. In: Proc. 16th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2001. SIGPLAN Notices, vol. 36(11), pp. 70–82. ACM Press, New York (2001)
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
Agarwal, R., Stoller, S.D. (2004). Type Inference for Parameterized Race-Free Java. 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_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-24622-0_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20803-7
Online ISBN: 978-3-540-24622-0
eBook Packages: Springer Book Archive