|
 ABSTRACT
Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected interactions between concurrent threads. Much previous work has focused on detecting race conditions, but the absence of race conditions does not by itself prevent undesired thread interactions. We focus on the more fundamental non-interference property of atomicity; a method is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies (formal and informal) correctness arguments.This paper presents a dynamic analysis for detecting atomicity violations. This analysis combines ideas from both Lipton's theory of reduction and earlier dynamic race detectors. Experience with a prototype checker for multithreaded Java code demonstrates that this approach is effective for detecting errors due to unintended interactions between threads. In particular, our atomicity checker detects errors that would be missed by standard race detectors, and it produces fewer false alarms on benign races that do not cause atomicity violations. Our experimental results also indicate that the majority of methods in our benchmarks are atomic, supporting our hypothesis that atomicity is a standard methodology in multithreaded programming.
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
|
C. Artho, K. Havelund, and A. Biere. High-level data races. In The First International Workshop on Verification and Validation of Enterprise Information Systems, 2003.
|
 |
2
|
|
| |
3
|
|
| |
4
|
|
| |
5
|
David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
|
| |
6
|
A. D. Birrell. An introduction to programming with threads. Research Report~35, Digital Equipment Corporation Systems Research Center, 1989.
|
| |
7
|
Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
|
| |
8
|
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
|
| |
9
|
M. Burrows and K. R. M. Leino. Finding stale-value errors in concurrent programs. Technical Note 2002-004, Compaq Systems Research Center, 2002.
|
| |
10
|
|
| |
11
|
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
|
| |
12
|
|
| |
13
|
|
| |
14
|
Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Masaaki Mizuno, Invariant-based specification, synthesis, and verification of synchronization in concurrent programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
[doi> 10.1145/581339.581394]
|
| |
15
|
|
| |
16
|
|
| |
17
|
|
| |
18
|
|
| |
19
|
|
| |
20
|
|
| |
21
|
|
| |
22
|
|
| |
23
|
Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
|
| |
24
|
|
| |
25
|
|
| |
26
|
S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. In Workshop on Formal Techniques for Java-like Languages, 2003.
|
| |
27
|
|
| |
28
|
|
| |
29
|
Tim Harris , Keir Fraser, Language support for lightweight transactions, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
|
| |
30
|
J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In Proceedings of the International Conference on Verification, Model Checking and Abstract Interpretation, 2004.
|
| |
31
|
|
| |
32
|
|
| |
33
|
Java Grande Forum. Java Grande benchmark suite. Available from http://www.javagrande.org/, 2003.
|
| |
34
|
|
| |
35
|
|
| |
36
|
|
| |
37
|
|
| |
38
|
|
| |
39
|
B. Liskov , D. Curtis , P. Johnson , R. Scheifer, Implementation of Argus, Proceedings of the eleventh ACM Symposium on Operating systems principles, p.111-122, November 08-11, 1987, Austin, Texas, United States
|
| |
40
|
|
| |
41
|
|
| |
42
|
|
| |
43
|
|
| |
44
|
Polyspace technologies, 2003. Available at http://www.polyspace.com.
|
| |
45
|
|
| |
46
|
|
| |
47
|
|
| |
48
|
Standard Performance Evaluation Corporation. SPEC benchmarks. Available from http://www.spec.org/, 2003.
|
| |
49
|
N. Sterling. Warlock: A static data race analysis tool. In Proceedings of the USENIX Winter Technical Conference, pages 97--106, 1993.
|
| |
50
|
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
|
| |
51
|
|
| |
52
|
C. von Praun and T. Gross. Static detection of atomicity violations in object-oriented programs. In Workshop on Formal Techniques for Java-like Programs, 2003.
|
| |
53
|
L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Proceedings of the Workshop on Runtime Verification, volume 89(2) of Electronic Notes in Computer Science. Elsevier, 2003.
|
| |
54
|
World Wide Web Consortium. Jigsaw. Available from http://www.w3c.org, 2001.
|
CITED BY 54
|
|
|
|
|
|
|
|
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
|
|
|
Amit Sasturkar , Rahul Agarwal , Liqiang Wang , Scott D. Stoller, Automated type-based analysis of data races and atomicity, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Rahul Agarwal , Scott D. Stoller, Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables, Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA
|
|
|
Yosi Ben-Asher , Yaniv Eytani , Eitan Farchi , Shmuel Ur, Producing scheduling that causes concurrent programs to fail, Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Bohuslav Krena , Zdenek Letko , Rachel Tzoref , Shmuel Ur , Tomáš Vojnar, Healing data races on-the-fly, Proceedings of the 2007 ACM workshop on Parallel and distributed systems: testing and debugging, July 09-09, 2007, London, United Kingdom
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Robert Geva , Yang Ni , Adam Welc, Towards transactional memory semantics for C++, Proceedings of the twenty-first annual symposium on Parallelism in algorithms and architectures, August 11-13, 2009, Calgary, AB, Canada
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.2