Amit Sasturkar
Scott D. Stoller
ABSTRACT
Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose at run-time. This motivated the development of type systems that statically ensure the absence of some common kinds of concurrent programming errors including data races and atomicity violations. A method is atomic if every execution of the concurrent program is equivalent to an execution in which the atomic method is executed without being interleaved with other concurrently executed methods. Atomicity is a common correctness requirement in concurrent programs; atomicity violations may indicate incorrect synchronization. This paper presents Extended Parameterized Atomic Java (EPAJ), a type system for specifying and verifying atomicity in Java programs. EPAJ combines Flanagan and Qadeer's atomicity types [11] with a new and significantly more expressive type system for analyzing data races, called Extended Parameterized Race-Free Java (EPRFJ), allowing a more accurate analysis of atomicity. The paper also presents a type discovery algorithm to automatically obtain EPRFJ types, and a static interprocedural type inference algorithm that, given EPRFJ types, infers atomicity types. These algorithms can be incorporated into testing and debugging tools, benefiting users who know nothing about type systems. We report our experience with a prototype implementation.
- M. Abadi, C. Flanagan, and S. Freund. Types for safe locking: Static race detection for Java. ACM Transactions on Programming Languages and Systems, to appear. Google Scholar
Digital Library
- R. Agarwal, A. Sasturkar, and S. D. Stoller. Type discovery for parameterized race-free Java. Technical Report DAR-04-16, Computer Science Department, SUNY at Stony Brook, Sept. 2004. Available at http://www.cs.sunysb.edu/~stoller/type-discovery/ .Google Scholar
- R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation, volume 2937 of Lecture Notes in Computer Science, pages 149--160. Springer-Verlag, Jan. 2004.Google ScholarCross Ref
- C. Boyapati and M. C. Rinard. A parameterized type system for race-free Java programs. In Proc. 16th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), volume 36(11) of SIGPLAN Notices, pages 56--69. ACM Press, 2001. Google ScholarDigital Library
- J.-D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 258--269. ACM Press, 2002. Google ScholarDigital Library
- O. Edelstein, E. Farchi, E. Goldin, Y. Nir, G. Ratsaby, and S. Ur. Framework for testing multi-threaded Java programs. Concurrency and Computation: Practice and Experience, 15(3-5):485--499, 2003.Google ScholarCross Ref
- C. Flanagan and S. Freund. Type-based race detection for Java. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 219--232. ACM Press, 2000. Google ScholarDigital Library
- C. Flanagan and S. Freund. Type inference against races. In Proc. 11th International Static Analysis Symposium (SAS), volume 3148 of Lecture Notes in Computer Science. Springer-Verlag, Aug. 2004.Google ScholarCross Ref
- C. Flanagan, S. Freund, and M. Lifshin. Type inference for atomicity. In Proc. ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI). ACM Press, 2005. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In Proc. 31st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Jan. 2004. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 338--349. ACM Press, 2003. Google ScholarDigital Library
- A. Greenhouse and W. L. Scherlis. Assuring and evolving concurrent programs: annotations and policy. In Proc. 24th international Conference on Software Engineering (ICSE), pages 453--463. ACM Press, May 2002. Google ScholarDigital Library
- A. Sasturkar, R. Agarwal, and S. D. Stoller. Typing rules for Extended Parameterized Atomic Java. Technical Report DAR-05-21, Computer Science Department, SUNY at Stony Brook, Sept. 2004. Available at http://www.cs.sunysb.edu/~amits/papers/atomicity-inference/.Google Scholar
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM Transactions on Computer Systems, 15(4):391--411, Nov. 1997. Google ScholarDigital Library
- A. Tarski. A lattice theoretical fixed point theorem and its applications. Pacific J. of Math, 5:285--309, 1955.Google ScholarCross Ref
- C. von Praun and T. R. Gross. Object race detection. In Proc. 16th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), volume 36(11) of SIGPLAN Notices, pages 70--82. ACM Press, Oct. 2001. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Proc. Third Workshop on Runtime Verification (RV), volume 89(2) of Electronic Notes in Theoretical Computer Science. Elsevier, July 2003. Available at http://www.cs.sunysb.edu/stoller.Google Scholar
- L. Wang and S. D. Stoller. Runtime analysis of atomicity for multi-threaded programs. Technical Report DAR-04-2, SUNY at Stony Brook, Computer Science Dept., July 2004. Available at http://www.cs.sunysb.edu/~liqiang/atomicity.html.Google Scholar
Index Terms
- Automated type-based analysis of data races and atomicity
Recommendations
Types for atomicity: Static checking and inference for Java
Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads. Atomic ...
Optimized run-time race detection and atomicity checking using partial discovered types
ASE '05: Proceedings of the 20th IEEE/ACM International Conference on Automated Software EngineeringConcurrent programs are notorious for containing errors that are difficult to reproduce and diagnose. Two common kinds of concurrency errors are data races and atomicity violations (informally, atomicity means that executing methods concurrently is ...
A type and effect system for atomicity
Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions between threads. Previous work addressed this problem by devising tools for detecting race conditions, a situation ...
Comments