Abstract
Read and write dependences of program variables are essential to determine whether and how a loop or a whole program can be parallelized. State-of-the-art tools for parallelization use approaches that over- as well as under-approximate to compute dependences and they lack a formal foundation. In this paper, we give formal semantics of read and write data dependences and present a program logic that is able to reason about dependences soundly and with full precision. The approach has been implemented in the deductive verification tool KeY for the target language Java.
This work was funded by the Hessian LOEWE initiative within the Software-Factory 4.0 project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In the HPC community the term dependence (pl. dependences) is used rather than dependency / dependencies. We follow their convention.
- 2.
This is easily justified formally by using \(\{ac_1\}\{ac_2\}\) instead of \(\{ac_1, ac_2\}\) and the original rule \({\mathsf {readAcOnNoRAW}}\), but would result in a longer, more technical proof.
References
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification – The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6
Albert, E., Bubel, R., Genaim, S., Hähnle, R., Díez, G.R.: A formal verification framework for static analysis–as well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. Softw. Syst. Model. 15(4), 987–1012 (2016)
Allen, F.E., Burke, M.G., Cytron, R., Ferrante, J., Hsieh, W.C.: A framework for determining useful parallelism. In: Lenfant, J. (ed.) Proceedings of the 2nd International Conference on Supercomputing, pp. 207–215. ACM (1988)
Amme, W., Braun, P., Thomasset, F., Zehendner, E.: Data dependence analysis of assembly code. Int. J. Parallel Program. 28(5), 431–467 (2000)
Banerjee, U.: An introduction to a formal theory of dependence analysis. J. Supercomput. 2(2), 133–149 (1988)
Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org
Cytron, R., Ferrante, J.: What’s in a name? -or- the value of renaming for parallelism detection and storage allocation. In: International Conference on Parallel Processing, pp. 19–27. Pennsylvania State University Press (1987)
Feautrier, P.: Dataflow analysis of array and scalar references. Int. J. Parallel Program. 20(1), 23–53 (1991)
Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319–349 (1987)
Garcia, S., Jeon, D., Louie, C.M., Taylor, M.B.: Kremlin: rethinking and rebooting gprof for the multicore age. In: Hall, M.W., Padua, D.A. (eds.) 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 458–469. ACM (2011)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259
Huda, Z.U., Atre, R., Jannesari, A., Wolf, F.: Automatic parallel pattern detection in the algorithm structure design space. In: 30th IEEE International Parallel and Distributed Processing Symposium, pp. 43–52. IEEE Computer Society (2016)
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976). https://doi.org/10.1145/360248.360252
Li, Z., Jannesari, A., Wolf, F.: An efficient data-dependence profiler for sequential and parallel programs. In: IEEE International Parallel and Distributed Processing Symposium, pp. 484–493. IEEE Computer Society (2015)
Liu, W., et al.: POSH: a TLS compiler that exploits program structure. In: Torrellas, J., Chatterjee, S. (eds.) ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP, pp. 158–167. ACM (2006)
Maydan, D., Amarsinghe, S., Lam, M.: Data dependence and data-flow analysis of arrays. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1992. LNCS, vol. 757, pp. 434–448. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57502-2_63
von Praun, C., Bordawekar, R., Cascaval, C.: Modeling optimistic concurrency using quantitative dependence analysis. In: Chatterjee, S., Scott, M.L. (eds.) 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP, pp. 185–196. ACM (2008)
Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Martin, J.L. (ed.) Proceedings Supercomputing 1991, pp. 4–13. ACM (1991)
Pugh, W., Wonnacott, D.: An exact method for analysis of value-based array data dependences. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1993. LNCS, vol. 768, pp. 546–566. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-57659-2_31
Pugh, W., Wonnacott, D.: Static analysis of upper and lower bounds on dependences and parallelism. ACM Trans. Program. Lang. Syst. 16(4), 1248–1278 (1994)
Sánchez, D., Yen, L., Hill, M.D., Sankaralingam, K.: Implementing signatures for transactional memory. In: 40th Annual IEEE/ACM International Symposium on Microarchitecture, pp. 123–133. IEEE Computer Society (2007)
Snelting, G., et al.: Checking probabilistic noninterference using JOANA. it - Inf. Technol. 56(6), 280–287 (2014)
Wasser, N., Bubel, R., Hähnle, R.: Abstract interpretation. In: Ahrendt et al. [1], chap. 6, pp. 167–189
Wu, P., Kejariwal, A., Caşcaval, C.: Compiler-driven dependence profiling to guide program parallelization. In: Amaral, J.N. (ed.) LCPC 2008. LNCS, vol. 5335, pp. 232–248. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89740-8_16
Yuki, T., Pouchet, L.N.: Polybench/c 4.1 (2015). http://web.cse.ohio-state.edu/~pouchet.2/software/polybench/
Zhang, X., Navabi, A., Jagannathan, S.: Alchemist: a transparent dependence distance profiling infrastructure. In: The Seventh International Symposium on Code Generation and Optimization, pp. 47–58. IEEE Computer Society (2009)
Acknowledgment
We thank Prof. Felix Wolf, Mohammad Norouzi, and Arya Mazaheri for providing us with DiscoPoP and for helpful discussions about data dependence analysis.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Bubel, R., Hähnle, R., Heydari Tabar, A. (2019). A Program Logic for Dependence Analysis. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-34968-4_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-34967-7
Online ISBN: 978-3-030-34968-4
eBook Packages: Computer ScienceComputer Science (R0)