Liqiang Wang
Scott D. Stoller
ABSTRACT
In concurrent programming, non-blocking synchronization is very efficient but difficult to design correctly. This paper presents a static analysis to show that code blocks are atomic, i.e., that every execution of the program is equivalent to one in which those code blocks execute without interruption by other threads. Our analysis determines commutativity of operations based primarily on how synchronization primitives (including locks, load-linked, store-conditional, and compare-and-swap) are used. A reduction theorem states that certain patterns of commutativity imply atomicity. Atomicity is itself an important correctness requirement for many concurrent programs. Furthermore, an atomic code block can be treated as a single transition during subsequent analysis of the program; this can greatly improve the efficiency of the subsequent analysis. We demonstrate the effectiveness of our approach on several concurrent non-blocking programs.
- 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). ACM Press, 2004. Google Scholar
Digital Library
- C. Flanagan, S. N. Freund, and S. Qadeer. Exploiting purity for atomicity. In Proc. ACM International Symposium on Software Testing and Analysis (ISSTA), pages 221--231. ACM Press, 2004. An extended version appeared as Technical Report 04-02, Williams College, 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). ACM Press, 2003. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Types for atomicity. In Proc. ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI), pages 1--12. ACM Press, 2003. Google ScholarDigital Library
- H. Gao and W. H. Hesselink. A formal reduction for lock-free parallel algorithms. In Proceedings of the 16th International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science, pages 44--56, 2004.Google Scholar
- M. P. Herlihy. Wait-free synchronization. ACM Transactions on Programming Languages and Systems, 13(1):124--149, January 1991. Google ScholarDigital Library
- M. P. Herlihy. A methodology for implementing highly concurrent data objects. ACM Transactions on Programming Languages and Systems, 15(5):745--770, Nov. 1993. 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
- G. J. Holzmann. The SPIN Model Checker. Addison-Wesley, 2003.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
- M. M. Michael. Private communication, 2004.Google Scholar
- M. M. Michael. Scalable lock-free dynamic memory allocation. In Conference on Programming Language Design and Implementation (PLDI). ACM Press, June 2004. Google ScholarDigital Library
- M. M. Michael and M. L. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In the 15th Annual ACM Symposium on Principles of Distributed Computing (PODC '96), pages 267--275. ACM Press, 1996. Google ScholarDigital Library
- D. Peled. Ten years of partial order reduction. In A. J. Hu and M. Y. Vardi, editors, Proc. 10th Int'l. Conference on Computer-Aided Verification (CAV), volume 1427 of Lecture Notes in Computer Science, pages 17--28. Springer-Verlag, 1998. Google ScholarDigital Library
- S. Qadeer, S. K. Rajamani, and J. Rehof. Summarizing procedures in concurrent programs. In Proc. 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 245--255. ACM Press, 2004. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Static analysis of atomicity for programs with non-blocking synchronization. Technical Report DAR-04-17, SUNY at Stony Brook, Computer Science Dept., Oct. 2004 (revised Jan. 2005). Available at http://www.cs.sunysb.edu/~liqiang/nonblocking.html.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
- E. Yahav and M. Sagiv. Automatically verifying concurrent queue algorithms. In Proc. Workshop on Software Model Checking (SoftMC'03), volume 89(3) of Electronic Notes in Theoretical Computer Science. Elsevier, 2003.Google Scholar
Index Terms
- Static analysis of atomicity for programs with non-blocking synchronization
Recommendations
Looking for efficient implementations of concurrent objects
PaCT'11: Proceedings of the 11th international conference on Parallel computing technologiesAs introduced by Taubenfeld, a contention-sensitive implementation of a concurrent object is an implementation such that the overhead introduced by locking is eliminated in the common cases, i.e., when there is no contention or when the operations ...
On the implementation of concurrent objects
Dependable and Historic ComputingThe implementation of objects shared by concurrent processes, with provable safety and liveness guarantees, is a fundamental issue of concurrent programming in shared memory systems. It is now largely accepted that linearizability (or atomicity) is an ...
Specifying and checking semantic atomicity for multithreaded programs
ASPLOS '11In practice, it is quite difficult to write correct multithreaded programs due to the potential for unintended and nondeterministic interference between parallel threads. A fundamental correctness property for such programs is atomicity---a block of ...
Comments