Context-sensitive synchronization-sensitive analysis is undecidable

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Context-sensitive synchronization-sensitive analysis is undecidable

Full text

Pdf (202 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 22 , Issue 2 (March 2000) table of contents

Pages: 416 - 430

Year of Publication: 2000

ISSN:0164-0925

Author

G. Ramalingam

IBM T.J. Watson Research Center, Yorktown Heights, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 21, Downloads (12 Months): 125, Citation Count: 29

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/349214.349241 What is a DOI?

ABSTRACT

Static program analysis is concerned with the computation of approximations of the runtime behavior of programs. Precise information about a program's runtime behavior is, in general, uncomputable for various different reasons, and each reason may necessitate making certain approximations in the information computed. This article illustrates one source of difficulty in static analysis of concurrent programs. Specifically, the article shows that an analysis that is simultaneously both context-sensitive and synchronization-sensitive (that is, a context-sensitive analysis that precisely takes into account the constraints on execution order imposed by the synchronization statements in the program) is impossible even for the simplest of analysis problems.

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	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	2	Evelyn Duesterwald , Mary Lou Soffa, Concurrency analysis in the presence of procedures using a data-flow framework, Proceedings of the symposium on Testing, analysis, and verification, p.36-48, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120811]
	3	Javier Esparza , Andreas Podelski, Efficient algorithms for pre* and post* on interprocedural parallel flow graphs, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325697]
	4	Dirk Grunwald , Harini Srinivasan, Efficient Computation of Precedence Information in Parallel Programs, Proceedings of the 6th International Workshop on Languages and Compilers for Parallel Computing, p.602-616, August 12-14, 1993
	5	John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	6	Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
	7	Stephen P. Masticola , Barbara G. Ryder, Non-concurrency analysis, Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.129-138, May 19-22, 1993, San Diego, California, United States
	8	Stephen P. Masticola, Static detection of deadlocks in polynomial time, Rutgers University, New Brunswick, NJ, 1993
	9	Gleb Naumovich , George S. Avrunin, A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.24-34, November 01-05, 1998, Lake Buena Vista, Florida, United States
	10	G. Naumovich , G. Avrunin , L. Clarke, An Efficient Algorithm for Computing MHP Information for Concurrent Java Programs, University of Massachusetts, Amherst, MA, 1998
	11	John H. Reif, Data flow analysis of communicating processes, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.257-268, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567777]
	12	Thomas Reps, Undecidability of context-sensitive data-independence analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.162-186, Jan. 2000 [doi>10.1145/345099.345137]
	13	Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
	14	Mooly Sagiv , Thomas Reps , Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, Theoretical Computer Science, v.167 n.1-2, p.131-170, Oct. 30, 1996
	15	SHARIR, ~/{. AND PNEULI, t. 1981. Two approaches to interprocedurM data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice Hall, Englewood Cliffs, N J, 189-233.
	16	TAYLOR, R. N. 1983. Complexity of analyzing the synchronization structure of concurrent programs. Acta Inforrnatica 19, 57-84.

CITED BY 29

	Markus Müller-Olm , Helmut Seidl, On optimal slicing of parallel programs, Proceedings of the thirty-third annual ACM symposium on Theory of computing, p.647-656, July 2001, Hersonissos, Greece
	Jong-Deok Choi , Andreas Zeller, Isolating failure-inducing thread schedules, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	Jens Krinke, Context-sensitive slicing of concurrent programs, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003
	Ahmed Bouajjani , Javier Esparza , Tayssir Touili, A generic approach to the static analysis of concurrent programs with procedures, ACM SIGPLAN Notices, v.38 n.1, p.62-73, January 2003
	Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof, Summarizing procedures in concurrent programs, ACM SIGPLAN Notices, v.39 n.1, p.245-255, January 2004
	Markus Müller-Olm, Precise interprocedural dependence analysis of parallel programs, Theoretical Computer Science, v.311 n.1-3, p.325-388, 23 January 2004
	Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM SIGPLAN Notices, v.39 n.4, April 2004
	Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004
	Javier Esparza, Grammars as processes, Formal and natural computing, Springer-Verlag New York, Inc., New York, NY, 2002
	Baowen Xu , Ju Qian , Xiaofang Zhang , Zhongqiang Wu , Lin Chen, A brief survey of program slicing, ACM SIGSOFT Software Engineering Notes, v.30 n.2, March 2005
	Herb Sutter , James Larus, Software and the concurrency revolution, Queue, v.3 n.7, September 2005
	Arthur Charlesworth, The undecidability of associativity and commutativity analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.5, p.554-565, September 2002
	Mangala Gowri Nanda , S. Ramesh, Interprocedural slicing of multithreaded programs with applications to Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1088-1144, November 2006
	Ranjit Jhala , Rupak Majumdar, Interprocedural analysis of asynchronous programs, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Vineet Kahlon , Aarti Gupta, On the analysis of interacting pushdown systems, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Narjes Ben Rajeb , Brahim Nasraoui , Riadh Robbana , Tayssir Touili, Verifying Multithreaded Recursive Programs with Integer Variables, Electronic Notes in Theoretical Computer Science (ENTCS), 239, p.143-154, July, 2009
	Byron Cook , Daniel Kroening , Natasha Sharygina, Verification of Boolean programs with unbounded thread creation, Theoretical Computer Science, v.388 n.1-3, p.227-242, December, 2007
	Ravi Chugh , Jan W. Voung , Ranjit Jhala , Sorin Lerner, Dataflow analysis for concurrent programs using datarace detection, ACM SIGPLAN Notices, v.43 n.6, June 2008
	David Binkley, Source Code Analysis: A Road Map, 2007 Future of Software Engineering, p.104-119, May 23-25, 2007
	Dilian Gurov , Marieke Huisman , Christoph Sprenger, Compositional verification of sequential programs with procedures, Information and Computation, v.206 n.7, p.840-868, July, 2008
	Jun Chen , Steve MacDonald, Towards a better collaboration of static and dynamic analyses for testing concurrent programs, Proceedings of the 6th workshop on Parallel and distributed systems: testing, analysis, and debugging, p.1-9, July 20-21, 2008, Seattle, Washington
	Jun Chen , Steve MacDonald, Testing concurrent programs using value schedules, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Laura Bozzelli , Salvatore La Torre , Adriano Peron, Verification of well-formed communicating recursive state machines, Theoretical Computer Science, v.403 n.2-3, p.382-405, August, 2008
	Fernando Rosa-Velardo , David de Frutos-Escrig, Name Creation vs. Replication in Petri Net Systems, Fundamenta Informaticae, v.88 n.3, p.329-356, December 2008
	Pierre Ganty , Rupak Majumdar , Andrey Rybalchenko, Verifying liveness for asynchronous programs, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Dennis Giffhorn , Christian Hammer, Precise slicing of concurrent programs, Automated Software Engineering, v.16 n.2, p.197-234, June 2009
	Mihaela Sighireanu , Tayssir Touili, Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism, Electronic Notes in Theoretical Computer Science (ENTCS), 239, p.43-56, July, 2009
	Akash Lal , Thomas Reps, Reducing concurrent analysis under a context bound to sequential analysis, Formal Methods in System Design, v.35 n.1, p.73-97, August 2009