This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Exploiting Purity for Atomicity
April 2005 (vol. 31 no. 4)
pp. 275-291
ASCII Text
x 
 
Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, "Exploiting Purity for Atomicity," IEEE Transactions on Software Engineering, vol. 31, no. 4, pp. 275-291, April, 2005.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2005.47,
author = {Cormac Flanagan and Stephen N. Freund and Shaz Qadeer},
title = {Exploiting Purity for Atomicity},
journal ={IEEE Transactions on Software Engineering},
volume = {31},
number = {4},
issn = {0098-5589},
year = {2005},
pages = {275-291},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2005.47},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Exploiting Purity for Atomicity
IS - 4
SN - 0098-5589
SP275
EP291
EPD - 275-291
A1 - Cormac Flanagan,
A1 - Stephen N. Freund,
A1 - Shaz Qadeer,
PY - 2005
KW - Index Terms- Atomicity
KW - purity
KW - reduction
KW - concurrent programs.
VL - 31
JA - IEEE Transactions on Software Engineering
ER -
 
Multithreaded programs often exhibit erroneous behavior because of unintended interactions between concurrent threads. This paper focuses on the noninterference property of atomicity. A procedure is atomic if, for every execution, there is an equivalent serial execution in which the actions of the atomic procedure are not interleaved with actions of other threads. This key property makes atomic procedures amenable to sequential reasoning techniques, which significantly facilitates subsequent validation activities such as code inspection and testing. Several existing tools verify atomicity by using commutativity of actions to show that every execution reduces to a corresponding serial execution. However, experiments with these tools have highlighted a number of interesting procedures that, while intuitively atomic, are not reducible. In this paper, we exploit the notion of pure code blocks to verify the atomicity of such irreducible procedures. If a pure block terminates normally, then its evaluation does not change the program state and, hence, these evaluation steps can be removed from the program trace before reduction. We develop a static typed-based analysis for atomicity based on this insight, and we illustrate this analysis on a number of interesting examples that could not be verified using earlier tools based purely on reduction.

[1] C. Flanagan and M. Abadi, “Types for Safe Locking” Proc. European Symp. Programming, pp. 91-108, 1999.
[2] C. Flanagan and S.N. Freund, “Type-Based Race Detection for Java” Proc. ACM Conf. Programming Language Design and Implementation, pp. 219-232, 2000.
[3] C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata, “Extended Static Checking for Java,” Proc. ACM Conf. Programming Language Design and Implementation, pp. 234-245, 2002.
[4] S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T.E. Anderson, “Eraser: A Dynamic Data Race Detector for Multi-Threaded Programs,” ACM Trans. Computer Systems, vol. 15, no. 4, pp. 391-411, 1997.
[5] C. Flanagan and S.N. Freund, “Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs,” Proc. ACM Symp. Principles of Programming Languages, pp. 256-267, 2004.
[6] S.N. Freund and S. Qadeer, “Checking Concise Specifications for Multithreaded Software,” J. Object Technology, vol. 3, no. 6, pp. 81-101, 2004.
[7] C. Flanagan and S. Qadeer, “A Type and Effect System for Atomicity,” Proc. ACM Conf. Programming Language Design and Implementation, pp. 338-349, 2003.
[8] C. Flanagan and S. Qadeer, “Types for Atomicity,” Proc. ACM Workshop Types in Language Design and Implementation, pp. 1-12, 2003.
[9] L. Wang and S.D. Stoller, “Run-Time Analysis for Atomicity,” Proc. Workshop Runtime Verification, 2003.
[10] J. Hatcliff, Robby, and M.B. Dwyer, “Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking,” Proc. Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 175-190, 2004.
[11] R.J. Lipton, “Reduction: A Method of Proving Properties of Parallel Programs,” Comm. ACM, vol. 18, no. 12, pp. 717-721, 1975.
[12] D. Peled, “Combining Partial Order Reductions with On-the-Fly Model Checking,” Proc. Conf. Computer Aided Verification, pp. 377-390, 1994.
[13] C. Flanagan, “Verifying Commit-Atomicity Using Model-Checking,” Proc. 11th Int'l SPIN Workshop Model Checking of Software, pp. 252-266, 2004.
[14] C. Boyapati and M. Rinard, “A Parameterized Type System for Race-Free Java Programs,” Proc. ACM Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 56-69, 2001.
[15] D. Grossman, “Type-Safe Multithreading in Cyclone,” Proc. ACM Workshop Types in Language Design and Implementation, pp. 13-25, 2003.
[16] N. Sterling, “WARLOCK— A Static Data Race Analysis Tool,” Proc. USENIX Technical Conf., pp. 97-106, 1993.
[17] F. Nielson, H.R. Nielson, and C. Hank, Principles of Program Analysis. Springer, 1999.
[18] D.C. Schmidt and T.H. Harrison, “Double-Checked Locking— A Optimization Pattern for Efficiently Initializing and Accessing Thread-Safe Objects,” Pattern Languages of Program Design 3, R. Martin et al., eds., 1997.
[19] J.-D. Choi, M. Gupta, M.J. Serrano, V.C. Sreedhar, and S.P. Midkiff, “Escape Analysis for Java,” Proc. ACM Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 1-19, 1999.
[20] B. Blanchet, “Escape Analysis for Object-Oriented Languages. Application to Java,” Proc. ACM Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 20-34, 1999.
[21] T.W. Doeppner Jr., “Parallel Program Correctness through Refinement,” Proc. ACM Symp. Principles of Programming Languages, pp. 155-169, 1977.
[22] R.-J. Back, “A Method for Refining Atomicity in Parallel Algorithms,” Proc. Conf. Parallel Architectures and Languages Europe, pp. 199-216, 1989.
[23] L. Lamport and F.B. Schneider, “Pretending Atomicity,” Research Report 44, DEC Systems Research Center, 1989.
[24] E. Cohen and L. Lamport, “Reduction in TLA,” Proc. Int'l Conf. Concurrency Theory, pp. 317-331, 1998.
[25] J. Misra, A Discipline of Multiprogramming: Programming Theory for Distributed Applications. Springer- Verlag, 2001.
[26] D. Bruening, “Systematic Testing of Multithreaded Java Programs,” master's thesis, Massachusetts Inst. of Tech nology, 1999.
[27] S.D. Stoller, “Model-Checking Multi-Threaded Distributed Java Programs,” Proc. Workshop Model Checking and Software Verification, pp. 224-244, 2000.
[28] C. Flanagan and S. Qadeer, “Transactions for Software Model Checking,” Proc. Workshop Software Model Checking, 2003.
[29] S. Qadeer, S.K. Rajamani, and J. Rehof, “Summarizing Procedures in Concurrent Programs,” Proc. ACM Symp. Principles of Programming Languages, pp. 245-255, 2004.
[30] P. Godefroid, “Using Partial Orders to Improve Automatic Verification Methods,” Proc. IEEE Conf. Computer Aided Verification, pp. 176-185, 1991.
[31] R.E. Rodriguez, M.B. Dwyer, and J. Hatcliff, “Checking Strong Specifications Using an Extensible Software Model Checking Framework,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 404-420, 2004.
[32] C. Papadimitriou, The Theory of Database Concurrency Control. 1986.
[33] M.P. Herlihy and J.M. Wing, “Linearizability: A Correctness Condition for Concurrent Objects,” ACM Trans. Programming Languages and Systems, vol. 12, no. 3, pp. 463-492, 1990.
[34] C.A.R. Hoare, “Towards a Theory of Parallel Programming,” Operating Systems Techniques, pp. 61-71, 1972.
[35] D.B. Lomet, “Process Structuring, Synchronization, and Recovery Using Atomic Actions,” Language Design for Reliable Software, pp. 128-137, 1977.
[36] B. Liskov, D. Curtis, P. Johnson, and R. Scheifler, “Implementation of Argus,” Proc. Symp. Operating Systems Principles, pp. 111-122, 1987.
[37] J.L. Eppinger, L.B. Mummert, and A.Z. Spector, Camelot and Avalon: A Distributed Transaction Facility. Morgan Kaufmann, 1991.
[38] M.P. Atkinson, K.J. Chisholm, and W.P. Cockshott, “PS-Algol: An Algol with a Persistent Heap,” ACM SIGPLAN Notices, vol. 17, no. 7, pp. 24-31, 1981.
[39] M.P. Atkinson and D. Morrison, “Procedures as Persistent Data Objects,” ACM Trans. Programming Languages and Systems, vol. 7, no. 4, pp. 539-559, 1985.
[40] T.L. Harris and K. Fraser, “Language Support for Lightweight Transactions,” Proc. ACM Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 388-402, 2003.
[41] A. Welc, S. Jagannathan, and A.L. Hosking, “Transactional Monitors for Concurrent Objects,” Proc. 18th European Conf. Object-Oriented Programming, pp. 519-542, 2004.
[42] X. Deng, M. Dwyer, J. Hatcliff, and M. Mizuno, “Invariant-Based Specification, Synthesis, and Verification of Synchronization in Concurrent Programs,” Proc. Int'l Conf. Software Eng., pp. 442-452, 2002.
[43] C. Flanagan, S.N. Freund, and S. Qadeer, “Exploiting Purity for Atomicity,” Technical Note 04-05, Williams College, 2004.

Index Terms:
Index Terms- Atomicity, purity, reduction, concurrent programs.
Citation:
Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, "Exploiting Purity for Atomicity," IEEE Transactions on Software Engineering, vol. 31, no. 4, pp. 275-291, April 2005, doi:10.1109/TSE.2005.47
Usage of this product signifies your acceptance of the Terms of Use.