|
 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.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
 |
1
|
|
| |
2
|
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/ .
|
| |
3
|
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.
|
| |
4
|
Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
|
| |
5
|
Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
|
| |
6
|
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.
|
| |
7
|
|
| |
8
|
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.
|
| |
9
|
Cormac Flanagan , Stephen N. Freund , Marina Lifshin, Type inference for atomicity, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.47-58, January 10-10, 2005, Long Beach, California, USA
[doi> 10.1145/1040294.1040299]
|
| |
10
|
|
| |
11
|
|
| |
12
|
|
| |
13
|
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/.
|
| |
14
|
|
| |
15
|
A. Tarski. A lattice theoretical fixed point theorem and its applications. Pacific J. of Math, 5:285--309, 1955.
|
| |
16
|
Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
|
| |
17
|
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.
|
| |
18
|
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.
|
CITED BY 20
|
|
|
|
|
|
|
|
Rahul Agarwal , Amit Sasturkar , Liqiang Wang , Scott D. Stoller, Optimized run-time race detection and atomicity checking using partial discovered types, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Zdeněk Letko , Tomáš Vojnar , Bohuslav Křena, AtomRace: data race and atomicity violation detector and healer, Proceedings of the 6th workshop on Parallel and distributed systems: testing, analysis, and debugging, p.1-10, July 20-21, 2008, Seattle, Washington
|
|
|
|
|
|
|
|
|
|
|
|
Chen Tian , Vijay Nagarajan , Rajiv Gupta , Sriraman Tallam, Dynamic recognition of synchronization operations for improved data race detection, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
|
|
|
|
|
|
|
|
|
Shan Lu , Soyeon Park , Chongfeng Hu , Xiao Ma , Weihang Jiang , Zhenmin Li , Raluca A. Popa , Yuanyuan Zhou, MUVI: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs, ACM SIGOPS Operating Systems Review, v.41 n.6, December 2007
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.1