Abstract
We present a fixpoint-based algorithm for context-sensitive interprocedural kill/gen-analysis of programs with thread creation. Our algorithm is precise up to abstraction of synchronization common in this line of research; it can handle forward as well as backward problems. We exploit a structural property of kill/gen-problems that allows us to analyze the influence of environment actions independently from the local transfer of data flow information. While this idea has been used for programs with parbegin/parend blocks before in work of Knoop/Steffen/Vollmer and Seidl/Steffen, considerable refinement and modification is needed to extend it to thread creation, in particular for backward problems. Our algorithm computes annotations for all program points in time depending linearly on the program size, thus being faster than a recently proposed automata based algorithm by Bouajjani et. al..
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bouajjani, A., Müller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL 1977, Los Angeles, California, pp. 238–252. ACM Press, New York (1977)
Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) ETAPS 1999 and FOSSACS 1999. LNCS, vol. 1578, pp. 14–30. Springer, Heidelberg (1999)
Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: Proc. of POPL 2000, pp. 1–11. Springer, Heidelberg (2000)
Knoop, J., Steffen, B., Vollmer, J.: Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. TOPLAS 18(3), 268–299 (1996)
Lammich, P.: Fixpunkt-basierte optimale Analyse von Programmen mit Thread-Erzeugung. Master’s thesis, University of Dortmund (May 2006)
Lammich, P., Müller-Olm, M.: Precise fixpoint-based analysis of programs with thread-creation. Version with appendix. Available from http://cs.uni-muenster.de/u/mmo/pubs/
Lammich, P., Müller-Olm, M.: Precise fixed point based analysis of programs with thread-creation. In: Proc. of MEMICS 2006, pp. 91–98. Faculty of Information Technology, Brno University of Technology (2006)
Müller-Olm, M.: Precise interprocedural dependence analysis of parallel programs. Theor. Comput. Sci. 311(1-3), 325–388 (2004)
Müller-Olm, M., Seidl, H.: On optimal slicing of parallel programs. In: Proc. of STOC 2001, pp. 647–656. ACM Press, New York, NY, USA (2001)
Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. TOPLAS 22(2), 416–430 (2000)
Seidl, H., Steffen, B.: Constraint-Based Inter-Procedural Analysis of Parallel Programs. Nordic Journal of Computing (NJC) 7(4), 375–400 (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lammich, P., Müller-Olm, M. (2007). Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)