Abstract
We define a novel formulation of dataflow analysis for concurrent programs, where the flow of facts is along the causal dependencies of events. We capture the control flow of concurrent programs using a Petri net (called the control net), develop algorithms based on partially-ordered unfoldings, and report experimental results for solving causal dataflow analysis problems. For the subclass of distributive problems, we prove that complexity of checking data flow is linear in the number of facts and in the unfolding of the control net.
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
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: principles, techniques, and tools. Addison-Wesley Longman, Amsterdam (1986)
Chamillard, A.T., Clarke, L.A.: Improving the accuracy of petri net-based analysis of concurrent programs. In: ISSTA, pp. 24–38 (1996), doi:10.1145/229000.226299
Cytron, R., et al.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991), doi:10.1145/115372.115320
Dwyer, M., et al.: Flow analysis for verifying properties of concurrent software systems (2004)
Dwyer, M.B., Clarke, L.A.: A compact petri net representation and its implications for analysis. IEEE Trans. Softw. Eng. 22(11), 794–811 (1996), doi:10.1109/32.553699
Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20, 285–310 (2002)
Farzan, A., Madhusudan, P.: Causal atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 315–328. Springer, Heidelberg (2006)
Farzan, A., Madhusudan, P.: Causal dataflow analysis for concurrent programs. Technical Report UIUCDCS-R-2007-2806, CS Department, UIUC (2007)
Grahlmann, B.: The PEP tool. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 440–443. Springer, Heidelberg (1997)
Hecht, M.: Flow Analysis of Computer Programs. Elsevier, Amsterdam (1977)
Kahlon, V., Ivancic, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 505–518. Springer, Heidelberg (2005)
Knoop, J., Steffen, B.: Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. TOPLAS 18(3), 268–299 (1996), citeseer.ist.psu.edu/knoop94parallelism.html
Lee, J., Midkiff, S.P., Padua, D.A.: Concurrent static single assignment form and constant propagation for explicitly parallel programs. In: Huang, C.-H., Sadayappan, P., Sehr, D. (eds.) LCPC 1997. LNCS, vol. 1366, pp. 114–130. Springer, Heidelberg (1998)
Lee, J., Padua, D.A., Midkiff, S.P.: Basic compiler algorithms for parallel programs. In: PPoPP, pp. 1–12 (1999), citeseer.ist.psu.edu/lee99basic.html
Masticola, S.P., Ryder, B.G.: Non-concurrency analysis. In: PPOPP, pp. 129–138 (1993), doi:10.1145/155332.155346
McMillan, K.: A technique of state space search based on unfolding. Formal Methods in System Design 6(1), 45–65 (1995)
Muchnick, S.S.: Advanced Compiler Design and Imlementation. Morgan Kaufmann, San Francisco (1997)
Naumovich, G., Avrunin, G.S.: A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. In: SIGSOFT/FSE-6, Lake Buena Vista, Florida, United States, pp. 24–34 (1998), doi:10.1145/288195.288213
Nielson, F., Nielson, H.: Type and effect systems. In: Correct System Design, pp. 114–136 (1999)
Reps, T., et al.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1-2), 206–263 (2005)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp. 49–61 (1995), doi:10.1145/199448.199462
Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: PPoPP, pp. 12–23. ACM Press, New York (2001), doi:10.1145/379539.379553
Stoltz, E., Wolfe, M.: Sparse data-flow analysis for dag parallel programs (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Farzan, A., Madhusudan, P. (2007). Causal Dataflow Analysis for Concurrent Programs. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)