Liqiang Wang
Scott D. Stoller
ABSTRACT
Atomicity is an important correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multi-threaded programs, executions of procedures (or methods) can be regarded as transactions. Correctness in the presence of concurrency often requires atomicity of these transactions. Tools that automatically detect atomicity violations can uncover subtle errors that are hard to find with traditional debugging and testing techniques.This paper presents new algorithms for runtime (dynamic) detection of violations of conflict-atomicity and view-atomicity, which are analogous to conflict-serializability and view-serializability in database systems. In these algorithms, the recorded events are formed into a graph with edges representing the synchronization within each transaction and possible interactions between transactions. We give conditions on the graph that imply conflict-atomicity and view-atomicity. Experiments show that these new algorithms are more efficient in most experiments and are more accurate than previous algorithms with comparable asymptotic complexity.
- R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. In Proc. 20th IEEE/ACM International Conference on Automated Software Engineering (ASE). ACM Press, Nov. 2005. Google Scholar
Digital Library
- R. Agarwal, L. Wang, and S. D. Stoller. Detecting potential deadlocks with static analysis and runtime monitoring. In Proceedings of the Parallel and Distributed Systems: Testing and Debugging (PADTAD) Track of the 2005 IBM Verification Conference. Springer-Verlag, Nov. 2005.Google Scholar
- P. A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency control and recovery in database systems. Addison Wesley, 1987. Google ScholarDigital Library
- C. Flanagan. Verifying commit-atomicity using model-checking. In Proc. 11th Int'l. SPIN Workshop on Model Checking of Software, volume 2989 of LNCS, pages 252--266. Springer-Verlag, 2004.Google ScholarCross Ref
- C. Flanagan and S. N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In Proc. of ACM Symposium on Principles of Programming Languages (POPL), pages 256--267. ACM Press, 2004. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Type inference against races. In Static Analysis Symposium (SAS), volume 3148 of LNCS. Springer-Verlag, Aug. 2004.Google ScholarCross Ref
- C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. IEEE Transactions on Software Engineering, 31(4), Apr. 2005. 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). ACM Press, 2003. Google ScholarDigital Library
- J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), volume 2937 of LNCS. Springer-Verlag, Jan. 2004.Google ScholarCross Ref
- K. Havelund. Using runtime analysis to guide model checking of Java programs. In Proc. 7th Int'l. SPIN Workshop on Model Checking of Software, volume 1885 of LNCS, pages 245--264. Springer-Verlag, Aug. 2000. Google ScholarDigital Library
- M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463--492, July 1990. Google ScholarDigital Library
- Java Grande Forum. Java Grande Multi-threaded Benchmark Suite. version 1.0. Available from http://www.javagrande.org/.Google Scholar
- Jigsaw, version 2.2.4. Available from http://www.w3c.org.Google Scholar
- Decision Management Systems GmbH, Kopi compiler. Available from http://www.dms.at/kopi/.Google Scholar
- R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975. Google ScholarDigital Library
- C. H. Papadimitriou. The serializability of concurrent database updates. Journal of the ACM, 26(4):631--653, Oct. 1979. Google ScholarDigital Library
- A. Sasturkar, R. Agarwal, L. Wang, and S. D. Stoller. Automated type-based analysis of data races and atomicity. In Proc. ACM SIGPLAN 2005 Symposium on Principles and Practice of Parallel Programming (PPoPP). ACM Press, June 2005. Google ScholarDigital Library
- V. Vefeiadis, M. Herlihy, T. Hoare, and M. Shapiro. Proving correctness of highly-concurrent linearizable objects. In Proc. ACM SIGPLAN 2006 Symposium on Principles and Practice of Parallel Programming (PPoPP). ACM Press, 2006. Google ScholarDigital Library
- 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
- C. von Praun and T. R. Gross. Static detection of atomicity violations in object-oriented programs. In Journal of Object Technology, vol.3, no. 6, June 2004.Google Scholar
- L. Wang and S. D. Stoller. Run-time analysis for atomicity. In Third Workshop on Runtime Verification (RV03), volume 89(2) of Electronic Notes in Theoretical Computer Science. Elsevier, 2003.Google Scholar
- L. Wang and S. D. Stoller. Runtime analysis of atomicity for multi-threaded programs. Technical Report DAR-04-14, SUNY at Stony Brook, Computer Science Dept., July 2004. (revised May 2005). To appear in IEEE Transactions on Software Engineering. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. Technical Report DAR-05-26, SUNY at Stony Brook, Computer Science Dept., Sept. 2005.Google Scholar
- L. Wang and S. D. Stoller. Static analysis for programs with non-blocking synchronization. In Proc. ACM SIGPLAN 2005 Symposium on Principles and Practice of Parallel Programming (PPoPP). ACM Press, June 2005. Google ScholarDigital Library
Index Terms
- Accurate and efficient runtime detection of atomicity errors in concurrent programs
Recommendations
Runtime Analysis of Atomicity for Multithreaded Programs
Atomicity is a correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multithreaded programs, ...
Atomicity via source-to-source translation
MSPC '06: Proceedings of the 2006 workshop on Memory system performance and correctnessWe present an implementation and evaluation of atomicity (also known as software transactions) for a dialect of Java. Our implementation is fundamentally different from prior work in three respects: (1) It is entirely a source-to-source translation, ...
Dynamic detection of atomic-set-serializability violations
ICSE '08: Proceedings of the 30th international conference on Software engineeringPreviously we presented atomic sets, memory locations that share some consistency property, and units of work, code fragments that preserve consistency of atomic sets on which they are declared. We also proposed atomic-set serializability as a ...
Comments